141.
A Generalization of the Lifting Lemma for Logic Programming
- Payet, Etienne; Mesnard, Fred
In this
paper, we first generalize a version of the lifting lemma, by extending the
relation "is more general than" so that it takes into account only some
arguments of the atoms.
142.
Using First-Order Logic to Reason about Policies
- Halpern, Joseph Y.; Weissman, Vicky
We show that a fragment of (multi-sorted) first-order logic can be
used to represent and reason about policies.
143.
The intuitionistic fragment of computability logic at the propositional
level
- Japaridze, Giorgi
Intuitionistic
implication is understood as algorithmic reduction in the weakest possible --
and hence most natural -- sense, disjunction and conjunction as
deterministic-choice combinations of problems (disjunction = machine's choice,
conjunction = environment's choice), and "absurd" as a computational problem of
universal strength.
144.
Efficient First-Order Temporal Logic for Infinite-State Systems
- Dixon, Clare; Fisher, Michael; Konev, Boris; Lisitsa, Alexei
In this paper we consider the specification and verification of
infinite-state systems using temporal logic.
145.
Well-Founded Argumentation Semantics for Extended Logic Programming
- Schweimeier, Ralf; Schroeder, Michael
This paper defines an argumentation semantics for extended logic programming
and shows its equivalence to the well-founded semantics with explicit negation.
146.
Applications of Intuitionistic Logic in Answer Set Programming
- Osorio, Mauricio; Navarro, Juan Antonio; Arrazola, Jose
We present some applications of intermediate logics in the field of Answer
Set Programming (ASP).
147.
On Structuring Proof Search for First Order Linear Logic
- Bruscoli, Paola; Guglielmi, Alessio
Full first order linear logic can be presented as an abstract logic
programming language in Miller's system Forum, which yields a sensible
operational interpretation in the 'proof search as computation' paradigm.
148.
Logic Column 12: Logical Verification and Equational Verification
- Pucella, Riccardo
This article examines two approaches to verification, one based on using a
logic for expressing properties of a system, and one based on showing the
system equivalent to a simpler system that obviously has whatever property is
of interest.
149.
A feasible algorithm for typing in Elementary Affine Logic
- Baillot, Patrick; Terui, Kazushige
We give a new type inference algorithm for typing lambda-terms in Elementary
Affine Logic (EAL), which is motivated by applications to complexity and
optimal reduction.
150.
Sound search in a denotational semantics for first order logic
- Vermeulen, C. F. M.
In this paper we adapt the definitions and results from Apt and Vermeulen on
`First order logic as a constraint programming language' (in: Proceedings of
LPAR2001, Baaz and Voronkov (eds.), Springer LNAI 2514) to include important
ideas about search and choice into the system.
151.
Uma investigação acerca das regras para a negação e o absurdo em dedução natural
- Wagner de Campos Sanz
O objetivo desta tese é o de propor uma elucidação da negação e do absurdo no âmbito dos sistemas de dedução natural para as lógicas intuicionista e clássica.
152.
Reasoning with Individuals for the Description Logic SHIQ
- Horrock, Ian; Sattler, Ulrike; Tobies, Stephan
While there has been a great deal of work on the development of reasoning
algorithms for expressive description logics, in most cases only Tbox reasoning
is considered.
153.
Detecção de movimento de objetos em tempo real utilizando dispositivos de lógica programável complexa
- Danilo Carlos Rossetto Minhoni
Um sistema que realiza a detecção de movimento procura, numa seqüência de imagens, sinais que confirmem a existência de movimentação no ambiente monitorado.
154.
Minimum Model Semantics for Logic Programs with Negation-as-Failure
- Rondogiannis, Panos; Wadge, William W.
We give a purely model-theoretic characterization of the semantics of logic
programs with negation-as-failure allowed in clause bodies.
155.
Well-founded and Stable Semantics of Logic Programs with Aggregates
- Pelov, Nikolay; Denecker, Marc; Bruynooghe, Maurice
In this paper, we present a framework for the semantics and the computation
of aggregates in the context of logic programming.
156.
A Hierarchical Analysis of Propositional Temporal Logic Based on
Intervals
- Moszkowski, Ben
We present a hierarchical framework for analysing propositional linear-time
temporal logic (PTL) to obtain standard results such as a small model property,
decision procedures and axiomatic completeness.
157.
The Complexity of Model Checking Higher-Order Fixpoint Logic
- Axelsson, Roland; Lange, Martin; Somla, Rafa?
This makes it a highly expressive
temporal logic that is capable of expressing various interesting correctness
properties of programs that are not expressible in the modal mu-calculus.
158.
A Comparison of Logic Programming Approaches for Representation and
Solving of Constraint Satisfaction Problems
- Pelov, Nikolay; De Mot, Emmanuel; Bruynooghe, Maurice
Many logic programming based approaches can be used to describe and solve
combinatorial search problems.
159.
Using Modes to Ensure Subject Reduction for Typed Logic Programs with
Subtyping
- Smaus, Jan-Georg; Fages, Francois; Deransart, Pierre
the execution model: if a program is
"well-typed", then all derivations starting in a "well-typed" goal are again
"well-typed".
160.
Some applications of logic to feasibility in higher types
- Ignjatovic, Aleksandar; Sharma, Arun
In this paper we demonstrate that the class of basic feasible functionals has
recursion theoretic properties which naturally generalize the corresponding
properties of the class of feasible functions.
