http://biblioteca.universia.net/vernivel.do?start=380&nivel=11 Mostrando recursos 381 - 400 de 88,632 es http://biblioteca.universia.net/img/logotipo.jpg http://biblioteca.universia.net/ http://biblioteca.universia.net/ficha.do?id=48925807 Esta dissertação apresenta uma integração entre a programação funcional e a programação em lógica, obtida pela definição e implementação da Linguagem LispLog. Nesta nova linguagem, o resultado de uma resolução pode ser utilizado como argumento de uma função (pelo operador metalisp) e o resultado da avaliação de uma função pode ser ligado a uma variável lógica (pelo operador avalia). A construção desta linguagem foi realizada a partir da simulação, em microcomputador similar ao IBM-PC, de uma ... DANTE CORBUCCI FILHO http://biblioteca.universia.net/ficha.do?id=47139528 This paper studies the notion of “freshness ” that often occurs in the meta-theory of computer science languages involving various kinds of names. Nominal Equational Logic is an extension of ordinary equational logic with assertions about the freshness of names. It is shown to be both sound and complete for the support interpretation of freshness and equality provided by the Gabbay-Pitts nominal sets model of names, binding and α-conversion. Ranald A. Clouston; Andrew M. Pitts http://biblioteca.universia.net/ficha.do?id=46673705 According to a well known conception, programs in a declarative programming language can be viewed as theories in some suitable logic, while computations can be viewed as deductions. In our opinion, there is yet no general assent on the logic to be viewed as the foundation of higher order, lazy functional logic languages. In this paper, we argue that a specific rewriting logic can play this role, and we justify the adequacy of our proposal by means of proof-theoretical and model-theoretical r... J. Carlos Gonzalez-moreno; M. Teresa Hortala-gonzalez; Mario Rodríguez-Artalejo http://biblioteca.universia.net/ficha.do?id=42088461 We are improving equality reasoning in automatic theorem-provers, and congruence classes provide an e#cient storage mechanism for terms, as well as the congruence closure decision procedure. We describe the technical steps involved in integrating logic variables with congruence classes, and present an algorithm that can be proved to find all matches between classes (modulo certain equalities). An application of this algorithm makes possible a percolation algorithm for undirected rewriting in ... http://biblioteca.universia.net/ficha.do?id=42089446 We are improving equality reasoning in automatic theorem-provers, and congruence classes provide an ecient storage mechanism for terms, as well as the congruence closure decision procedure. We describe the technical steps involved in integrating logic variables with congruence classes, and present an algorithm that can be proved to nd all matches between classes (modulo certain equalities). An application of this algorithm makes possible a percolation algorithm for undirected rewriting in min... http://biblioteca.universia.net/ficha.do?id=42124602 this paper we describe TLA from a logical perspective# our description of TLA has three aspects: 1' As a logic, TLA has a precise syntax and semantics. We define these in the next section. Our intent is not to develop a new TLA, but rather to explain and to refine Lamport's definition of TLA [1' 2. Like HOL [1' ] and other logics, TLA can serve for representing reactive systems in several styles. In particular, a specification may describe concurrent steps as interleaved or simultaneous# comm... http://biblioteca.universia.net/ficha.do?id=41490284 Contents 1 Introduction : : : : : : : : : : : : : : : : : : : : : : : : : : : : 2 2 The expressive power of second order Logic : : : : : : : : : : : 3 2.1 The language of second order logic : : : : : : : : : : : : : 3 2.2 Expressing size : : : : : : : : : : : : : : : : : : : : : : : : 4 2.3 Defining data types : : : : : : : : : : : : : : : : : : : : : 6 2.4 Describing processes : : : : : : : : : : : : : : : : : : : : : 8 2.5 Expressing convergence using second order validity : : : : : : : : :... Daniel Leivant http://biblioteca.universia.net/ficha.do?id=41737483 Contents 1 Introduction : : : : : : : : : : : : : : : : : : : : : : : : : : : : 2 2 The expressive power of second order Logic : : : : : : : : : : : 3 2.1 The language of second order logic : : : : : : : : : : : : : 3 2.2 Expressing size : : : : : : : : : : : : : : : : : : : : : : : : 4 2.3 Defining data types : : : : : : : : : : : : : : : : : : : : : 6 2.4 Describing processes : : : : : : : : : : : : : : : : : : : : : 8 2.5 Expressing convergence using second order validity : : : : : : : : :... Daniel Leivant http://biblioteca.universia.net/ficha.do?id=41954373 This paper presents a new approach to logic synthesis of digital synchronous circuits. We present a model for synchronous circuits that supports logic transformations aimed at optimizing the circuit performance. Previous synthesis approaches attacked this problem by separating the combinational logic from the registers and by applying circuit transformations to the combinational component only. We show in this paper instead how to optimize concurrently the circuit equations and the register p... Giovanni De Micheli http://biblioteca.universia.net/ficha.do?id=42018355 We show how to interoperate, semantically and inferentially, between the leading Semantic Web approaches to rules (RuleML Logic Programs) and ontologies (OWL/DAML+OIL Description Logic) via analyzing their expressive intersection. To do so, we define a new intermediate knowledge representation (KR) contained within this intersection: Description Logic Programs (DLP), and the closely related Description Horn Logic (DHL) which is an expressive fragment of first-order logic (FOL). DLP provides a... Benjamin N. Grosof,Ian Horrocks,Raphael Volz,Stefan Decker http://biblioteca.universia.net/ficha.do?id=42134783 We present a process logic for the p-calculus with the linear/affine type discipline [6, 7, 31, 32, 33, 59, 60]. Built on the preceding studies on logics for programs and processes, simple systems of assertions are developed, capturing the classes of behaviours ranging from purely functional interactions to those with destructive update, local state and genericity. A central feature of the logic is representation of the behaviour of an environment as the dual of that of a process in an assert... Queen Mary London http://biblioteca.universia.net/ficha.do?id=36515125 A presente pesquisa pretende analisar o período do pensamento filosófico de B. Russell e L. Wittgenstein entre os anos de 1905 e 1914 descrevendo o desenvolvimento da filosofia do atomismo lógico presente no Tractatus logico-philosophicus de Wittgenstein. Para tanto, será observada a crítica deste à teoria do juízo desenvolvida por Russell, a qual seria fundamento para a teoria do conhecimento que o último elaborava. Reconhecemos, com base nas críticas, que Russell sofria uma forte influência... Vanice Ribeiro da Silva http://biblioteca.universia.net/ficha.do?id=46150571 Abstract. We generalise dynamic logic to a logic for differential-algebraic programs, i.e., discrete programs augmented with first-order differentialalgebraic formulas as continuous evolution constraints in addition to first-order discrete jump formulas. These programs characterise interacting discrete and continuous dynamics of hybrid systems elegantly and uniformly. For our logic, we introduce a calculus over real arithmetic with discrete induction and a new differential induction with whic... André Platzer http://biblioteca.universia.net/ficha.do?id=46372656 We give an algebraic version of first order logic without equality in which the class of representable algebras forms a finitely based equational class. Further, the representables are defined in terms of set algebras, and all operations of the latter are permutation invariant. The algebraic form of this result is Theorem 1 (a concrete version of which is given by Theorems 1.8 and 3.2), while its logical form is Corollary 4.2. For first order logic with equality we give a result weaker than ... Ildikó Sain http://biblioteca.universia.net/ficha.do?id=46430141 We present a new fixed-point theorem akin to the Banach contraction mapping theorem, but in the context of a novel notion of generalized metric space, and show how it can be applied to analyse the denotational semantics of certain logic programs. The theorem is obtained by generalizing a theorem of Priess-Crampe and Ribenboim, which grew out of applications within valuation theory, but is also inspired by a theorem of S.G. Matthews which grew out of applications to conventional programming la... Pascal Hitzler And; Pascal Hitzler; Anthony K. Seda http://biblioteca.universia.net/ficha.do?id=46448499 Linear logic (LL) is the logical foundation of some type-theoretic languages and also of environments for specification and theorem proving. In this paper, we analyse the relationships between the proof net notion of LL and the connection notion used for efficient proof-search in different logics. Aiming at using proof nets as a tool for automated deduction in linear logic, we define a connection-based characterization of provability in Multiplicative Linear Logic (MLL). We show that an algor... D. Galmiche http://biblioteca.universia.net/ficha.do?id=46505068 In this paper we study constructions leading to the formation of belief sets by agents. We focus on the situation when possible belief sets are built incrementally in stages. We call an infinite sequence of theories that represents such a process a reasoning trace. A set of reasoning traces describing all possible reasoning scenarios for the agent is called a reasoning frame. Default logic by Reiter is not powerful enough to represent reasoning frames. In the paper we introduce a generalizati... Joeri Engelfriet; V. Wiktor Marek; Jan Treur; Miroslaw Truszczy'nski http://biblioteca.universia.net/ficha.do?id=46560212 We present a new fixed-point theorem akin to the Banach contraction mapping theorem, but in the context of a novel notion of generalized metric space, and show how it can be applied to analyse the denotational semantics of certain logic programs. The theorem is obtained by generalizing a theorem of Priess-Crampe and Ribenboim, which grew out of applications within valuation theory, but is also inspired by a theorem of S.G. Matthews which grew out of applications to conventional programming la... Pascal Hitzler; Anthony K. Seda http://biblioteca.universia.net/ficha.do?id=46606412 This article presents the description logic ALCRP(D) with concrete domains and a roleforming predicate operator as its prominent aspects. We demonstrate the feasibility of ALCRP(D) for reasoning about spatial objects and their qualitative spatial relationships and provide an appropriate concrete domain for spatial objects. The general significance of ALCRP(D) is demonstrated by adding temporal reasoning to spatial and terminological reasoning using a combined concrete domain. The theory... Volker Haarslev; Carsten Lutz; Ralf Möller http://biblioteca.universia.net/ficha.do?id=46896374 We show several properties of the abstract interpretation settings regarding relationships between precision of semantic operators and abstract domains composition. Then, we apply these results to the framework for logic programs introduced in [3], extended with the new class of operational observables. We prove that the classes of perfect, denotational and operational observables are complete lattices and we discuss some problems that arise studying them. Finally, we show how to use function... Gianluca Amato; Giorgio Levi