arXiv subjects

Vladimir Lifschitz

Publications and source records attributed to Vladimir Lifschitz.

28 records · Page 2Linked to original sources

arXiv2016

Proving Infinitary Formulas

The infinitary propositional logic of here-and-there is important for the theory of answer set programming in view of its relation to strongly equivalent transformations of logic programs. We know a formal system axiomatizing this logic exists, but a proof in that system may include infinitely many formulas. In this note we describe a relationship between the validity of infinitary formulas in the logic of here-and-there and the provability of formulas in some finite deductive systems. This relationship allows us to use finite proofs to justify the validity of infinitary formulas. This note is under consideration for publication in Theory and Practice of Logic Programming.

cs.LO↗

arXiv2014

On Equivalence of Infinitary Formulas under the Stable Model Semantics

Propositional formulas that are equivalent in intuitionistic logic, or in its extension known as the logic of here-and-there, have the same stable models. We extend this theorem to propositional formulas with infinitely long conjunctions and disjunctions and show how to apply this generalization to proving properties of aggregates in answer set programming. To appear in Theory and Practice of Logic Programming (TPLP).

cs.LO↗

arXiv2013

On the Semantics of Gringo

Input languages of answer set solvers are based on the mathematically simple concept of a stable model. But many useful constructs available in these languages, including local variables, conditional literals, and aggregates, cannot be easily explained in terms of stable models in the sense of the original definition of this concept and its straightforward generalizations. Manuals written by designers of answer set solvers usually explain such constructs using examples and informal comments that appeal to the user's intuition, without references to any precise semantics. We propose to approach the problem of defining the semantics of gringo programs by translating them into the language of infinitary propositional formulas. This semantics allows us to study equivalent transformations of gringo programs using natural deduction in infinitary propositional logic.

cs.AI↗

arXiv2013

Lloyd-Topor Completion and General Stable Models

We investigate the relationship between the generalization of program completion defined in 1984 by Lloyd and Topor and the generalization of the stable model semantics introduced recently by Ferraris et al. The main theorem can be used to characterize, in some cases, the general stable models of a logic program by a first-order formula. The proof uses Truszczynski's stable model semantics of infinitary propositional formulas.

cs.LO↗

arXiv2012

Relational Theories with Null Values and Non-Herbrand Stable Models

Generalized relational theories with null values in the sense of Reiter are first-order theories that provide a semantics for relational databases with incomplete information. In this paper we show that any such theory can be turned into an equivalent logic program, so that models of the theory can be generated using computational methods of answer set programming. As a step towards this goal, we develop a general method for calculating stable models under the domain closure assumption but without the unique name assumption.

cs.LO↗

arXiv2011

Representing First-Order Causal Theories by Logic Programs

Nonmonotonic causal logic, introduced by Norman McCain and Hudson Turner, became a basis for the semantics of several expressive action languages. McCain's embedding of definite propositional causal theories into logic programming paved the way to the use of answer set solvers for answering queries about actions described in such languages. In this paper we extend this embedding to nondefinite theories and to first-order causal logic.

cs.AI↗

arXiv2005

Temporal Phylogenetic Networks and Logic Programming

The concept of a temporal phylogenetic network is a mathematical model of evolution of a family of natural languages. It takes into account the fact that languages can trade their characteristics with each other when linguistic communities are in contact, and also that a contact is only possible when the languages are spoken at the same time. We show how computational methods of answer set programming and constraint logic programming can be used to generate plausible conjectures about contacts between prehistoric linguistic communities, and illustrate our approach by applying it to the evolutionary history of Indo-European languages. To appear in Theory and Practice of Logic Programming (TPLP).

cs.LO↗

arXiv2003

Weight Constraints as Nested Expressions

We compare two recent extensions of the answer set (stable model) semantics of logic programs. One of them, due to Lifschitz, Tang and Turner, allows the bodies and heads of rules to contain nested expressions. The other, due to Niemela and Simons, uses weight constraints. We show that there is a simple, modular translation from the language of weight constraints into the language of nested expressions that preserves the program's answer sets. Nested expressions can be eliminated from the result of this translation in favor of additional atoms. The translation makes it possible to compute answer sets for some programs with weight constraints using satisfiability solvers, and to prove the strong equivalence of programs with weight constraints using the logic of here-and there.

cs.AI↗

arXiv2003

Tight Logic Programs

This note is about the relationship between two theories of negation as failure -- one based on program completion, the other based on stable models, or answer sets. Francois Fages showed that if a logic program satisfies a certain syntactic condition, which is now called ``tightness,'' then its stable models can be characterized as the models of its completion. We extend the definition of tightness and Fages' theorem to programs with nested expressions in the bodies of rules, and study tight logic programs containing the definition of the transitive closure of a predicate.

cs.AI↗

arXiv2000

Fages' Theorem and Answer Set Programming

We generalize a theorem by Francois Fages that describes the relationship between the completion semantics and the answer set semantics for logic programs with negation as failure. The study of this relationship is important in connection with the emergence of answer set programming. Whenever the two semantics are equivalent, answer sets can be computed by a satisfiability solver, and the use of answer set solvers such as smodels and dlv is unnecessary. A logic programming representation of the blocks world due to Ilkka Niemelae is discussed as an example.

cs.AI↗