161.
Lógica dinámica con operadores ambiguos
- Artigas Prous, Josep
El almacenaje de Cooper es una técnica que ha sido desarrollada para tratar la ambigüedad semántica causada por el alcance de los cuantificadores. La Ambiguous Predicate Logic (APL) de van Eijck and Jaspars (1996) es una lógica ambigua que utiliza un método inspirado en esta técnica para formular representaciones subespecificadas. En esta comunicación proponemos equipar las teorías dinámicas de la semántica del lenguaje natural, en concreto la Dynamic Predicate Logic (DPL) de Groenendijk and Stokhof (1991), con el método de subespecificación de la APL. El resultado es una lógica dinámica subespecificada y propia.
162.
Lógica dinámica con operadores ambiguos
- Artigas Prous, Josep
El almacenaje de Cooper es una técnica que ha sido desarrollada para tratar la ambigüedad semántica causada por el alcance de los cuantificadores. La Ambiguous Predicate Logic (APL) de van Eijck and Jaspars (1996) es una lógica ambigua que utiliza un método inspirado en esta técnica para formular representaciones subespecificadas. En esta comunicación proponemos equipar las teorías dinámicas de la semántica del lenguaje natural, en concreto la Dynamic Predicate Logic (DPL) de Groenendijk and Stokhof (1991), con el método de subespecificación de la APL. El resultado es una lógica dinámica subespecificada y propia.
163.
A TECHNIQUE FOR DOING LAZY EVALUATION IN LOGIC SANJAI NARAIN
- J. Logic Programming
D We develop a natural technique for defining functions in logic, i.e. PROLOG, which directly yields lazy evaluation. Its use does not require any change to the PROLOG interpreter. Function definitions run as PROLOG programs and so run very efficiently. It is possible to combine lazy evaluation with nondeterminism and simulate coroutining. It is also possible to handle infinite data structures and implement networks of communicating processes. We analyze this technique and develop a precise definition of lazy evaluation for lists. For further efficiency we show how to preprocess programs and ensure, using logical variables, that values of expressions once...
164.
Probabilistic Interval Temporal Logic
- Dimitar P. Guelev; Dimitar P. Guelev
This paper presents an interval-based probabilistic temporal logic, that we call probabilistic interval logic. The new logic is an extension of Interval Temporal Logic (cf. e.g. [Dut95]), and can be viewed as a generalisation of Probabilistic Duration Calculus [LRSZ92, DZ94]. We propose a proof system for the new logic and demonstrate its completeness. We also present a complete axiomatisation of Chapman-Kolmogorov's property of sequential composition of probabilistic processes relative to a class of models of probabilistic interval logic that includes the significant class of real time based models. By giving a complete deductive system to the new logic we make...
165.
Representation Theory for Default Logic
- Wiktor Marek Jan
Default logic can be regarded as a mechanism to represent families of belief sets of a reasoning agent. As such, it is inherently second-order. In this paper, we study the problem of representability of a family of theories as the set of extensions of a default theory. We give a complete solution to the problem of representability by means of default theories with finite set of defaults, and by means of normal default theories. We obtain partial results on representability by arbitrary (infinite, nonnormal) default theories. We construct examples of denumerable families of non-including theories that are not representable. We...
166.
Representation Theory for Default Logic
- V. Wiktor Marek; Jan Treur; Miroslaw Truszczynski
Default logic can be regarded as a mechanism to represent families of belief sets of a reasoning agent. As such, it is inherently second-order. In this paper, we study the problem of representability of a family of theories as the set of extensions of a default theory. We give a complete solution to the problem of representability by means of default theories with finite set of defaults, and by means of normal default theories. We obtain partial results on representability by arbitrary (infinite, nonnormal) default theories. We construct examples of denumerable families of non-including theories that are not representable. We...
167.
A Model of Information Retrieval based on a Terminological Logic
- Terminological Logic,Carlo Meghint,Fabrizio Sebastiani,Umberto Straccia,Costantino Thanos
IAccording to the logical model of Information Retrieval (IR), the task of IR can be described as the extraction....
168.
The (Lazy) Functional Side of Logic Programming
- Sandro Etalle; Jon Mountjoy
The possibility of translating logic programs into functional ones has long been a subject of investigation. Common to the many approaches is that the original logic program, in order to be translated, needs to be well-moded and this has led to the common understanding that these programs can be considered to be the "functional part" of logic programs. As a consequence of this it has become widely accepted that "complex" logical variables, the possibility of a dynamic selection rule, and general properties of non-well-moded programs are exclusive features of logic programs. This is not quite true, as some of these...
169.
Nonmonotonic Reasoning Based on Incomplete Logic
- Tuan-Fang Fan Peng; I-peng Lin; Churn-jung Liau
. What characterizes human reasoning is the ability of dealing with incomplete information. Incomplete logic is developed for modeling incomplete knowledge. The most distinctive feature of incomplete logic is its semantics. This is an alternative presentation of partial semantics. In this paper, we will introduce the general notion of incomplete logic(ICL), compare it with partial logic, and give the resolution method for it. We will also show how ICL can be applied to nonmonotonic reasoning. We define nonmonotonic derivation as monotonic derivation in ICL from the database and some consistent assumptions. The mechanism of ICL makes it easy to assert...
170.
Concurrent Logic Programming as Uniform Linear Proofs
- Paolo Volpe
We describe a formalism based on the proof theory of linear logic, whose aim is to specify concurrent computations and whose language restriction (as compared to other linear logic languages) provides a simpler operational model that can lead to a more practical language core. The fragment is proved to be an abstract logic programming language, that is any sequent can be derived by uniform proofs. The resulting class of computations can be viewed in terms of multiset rewriting and is reminiscent of the computations arising in the Chemical Abstract Machine and in the Gamma model. The fragment makes it possible...
171.
Multi-Dimensional Logic Programming: Theoretical Foundations
- Mehmet A. Orgun; Weichang Du
This paper introduces an extension of logic programming based on multi-dimensional logics, called MLP. In a multi-dimensional logic the values of elements vary depending on more than one dimension, such as time and space. The resulting logic programming language is suitable for modelling objects which involve implicit and/or explicit temporal and spatial dependencies. The execution of programs of the language is based on a resolution-type proof procedure called MSLD-resolution (for Multi-dimensional SLD-resolution). MSLDresolution is based on the axioms and rules of inference of the underlying multi-dimensional logic. The paper also establishes the declarative semantics of multi-dimensional logic programs, based on...
172.
Introduction to mathematical logic - A problem solving course
- Miller, Arnold W.
This is a set of 288 questions written for a Moore-style course in
Mathematical Logic. I have used these (or some variation) four times in a
beginning graduate course. Topics covered are:
propositional logic
axioms of ZFC
wellorderings and equivalents of AC
ordinal and cardinal arithmetic
first order logic, and the compactness theorem
Lowenheim-Skolem theorems
Turing machines, Church's Thesis
completeness theorem and first incompleteness theorem
undecidable theories
second incompleteness theorem
173.
Topological Completeness for Higher-Order Logic
- Awodey, Steve; Butz, Carsten
Using recent results in topos theory, two systems of
higher-order logic are shown to be complete with respect to sheaf
models over topological spaces---so-called ``topological semantics''.
The first is classical higher-order logic, with relational
quantification of finitely high type; the second system is a
predicative fragment thereof with quantification over functions
between types, but not over arbitrary relations. The second theorem
applies to intuitionistic as well as classical logic.
174.
Translating Fork Specifications into Logic Programs
- Baum, Gabriel Alfredo; Aguirre, Nazareno Matías; Arroyo, Marcelo
In this work a compiler from fork specifications into logic programs is presented. The technique implemented by the compiler consists of transforming a set of fork equations (with some restrictions) into normal logic programs in such a way that the semantics of the fork equations is preserved.
After translating a fork specification, it can be executed by consulting the generated logic program. The fork compiler, a tool for the
translation, is also introduced.
175.
Resource-oriented Programming Based on Linear Logic
- Valerie Novitzká; Daniel Mihályi
Abstract: In our research we consider programming as logical reasoning over types. Linear logic with its resource-oriented features yields a proper means for our approach because it enables to consider about resources as in real life: after their use they are exhausted. Computation then can be regarded as proof search. In our paper we present how space and time can be introduced into this logic and we discuss several programming languages based on linear logic.
176.
Differential logic for reasoning about hybrid systems
- André Platzer
Abstract. We propose a first-order dynamic logic for reasoning about hybrid systems. As a uniform model for discrete and continuous evolutions in hybrid systems, we introduce hybrid programs with differential actions. Our logic can be used to specify and verify correctness statements about hybrid programs, which are suitable for symbolic processing by calculus rules. Using first-order variables, our logic supports systems with symbolic parameters. With dynamic modalities, it is prepared to handle multiple system components.
177.
Linear Logic Programming with an Ordered Context
- Jeff Polakow
We begin with a review of ordered linear logic (OLL), a refinement of intuitionistic linear logic with an inherent notion of order. We then develop a logic programming interpretation for OLL in two steps: (1) we give a system of ordered uniform derivations which is sound and complete with respect to OLL, and (2) we present a model of resource consumption which removes non-determinism from ordered resource allocation during search for uniform derivations. We also illustrate the expressive power of the resulting ordered linear logic programming language with several example programs.
178.
Logic Finite Automata
. In this paper we generalize the concept of a finite state automaton,
essentially by replacing terminal and nonterminal symbols by first order
terms and identity checking by unification. We arrive at the concept of a logic
finite automaton. Ignoring a conceptual distinction in the treatment of input,
logic finite automata may also be regarded as logic grammars with a rightlinear
skeleton. The concept is then discussed from these two perspectives.
We first consider logic finite automata over an input alphabet of constants,
regarding logic finite automata as classical automata. Among other results the
four classes from the Chomsky-Hierarchy are characterized by means of syntactic
restrictions on logic finite...
179.
Taming First-Order Logic
- Szabolcs Mikulas
In this paper we define computationally well-behaved versions of classical first-order logic and prove that the validity problem is decidable 1 . Keywords: first-order logic, decidability, relativization, mosaic, polyadic and counting quantifiers. 1 Taming In [5], we developed a strategy for taming logics. The idea of taming can be described as follows. Let us assume that we have a well-investigated logic with some undesirable metalogical properties. An example is the incompleteness and undecidability of the finite variable fragment of classical first-order logic, FOL, with at least three variables, cf. [4] 4.1.3 and 4.2.18 for the equivalent algebraic results. Taming a...
180.
Reinventing Logic Modeling: A Stakeholder-Driven Group Approach
- Green, Erinn Leary
A logic model visually represents the inputs, activities, outputs and outcomes of a program and proposes the causal links among these entities. The importance of including logic modeling in the evaluation of a program is well established (Weiss 1998; Rossi, Freeman & Lipsey 1999). Many evaluators have called for more stakeholder involvement in logic modeling (Weiss 1997, 1998; Patton 1989; Rossi, Freeman & Lipsey 1999), while others have called for new methods to craft logic models (Bickman 1987, 1989; McLaughlin & Jordan, 1999). This study developed and tested a technique that guides program stakeholders through the creation of a logic...
