This paper describes the process of translating rules that may contain arithmetic operations into the language of first-order logic. It identifies a normal form for which this transformation can be performed in a particularly simple and natural way. Other rules can be converted to this normal form by steps that preserve their meaning under the stable model semantics.

Abstract ANTHEM 2.0 is a tool to aid in the verification of logic programs written in an expressive fragment of CLINGO ’s input language named MINI-GRINGO, which includes arithmetic operations and simple choice rules but not aggregates. It can translate logic programs into formula representations in the logic of here-and-there and analyze properties of logic programs such as tightness. Most importantly, ANTHEM 2.0 can support program verification by invoking first-order theorem provers to confirm that a program adheres to a first-order specification or to establish strong and external equivalence of programs. This paper serves as an overview of the system’s capabilities. We demonstrate how to use ANTHEM 2.0 effectively and interpret its results.

Abstract In answer set programming, two groups of rules are considered strongly equivalent if they have the same meaning in any context. Strong equivalence of two programs can be sometimes established by deriving rules of each program from rules of the other in an appropriate deductive system. This paper shows how to extend this method of proving strong equivalence to programs containing the counting aggregate.

Abstract Program completion is a translation from the language of logic programs into the language of first-order theories. Its original definition has been extended to programs that include integer arithmetic, accept input, and distinguish between output predicates and auxiliary predicates. For tight programs, that generalization of completion is known to match the stable model semantics, which is the basis of answer set programming. We show that the tightness condition in this theorem can be replaced by a less restrictive “local tightness” requirement. From this fact we conclude that the proof assistant anthem-p2p can be used to verify equivalence between locally tight programs.

Theory of strongly equivalent transformations is an essential part of the methodology of representing knowledge in answer set programming. Strong equivalence of two programs can be sometimes characterized as the possibility of deriving the rules of each program from the rules of the other in some deductive system. This paper describes a system with this property for the language mini-GRINGO. The key to the proof is an ω-completeness theorem for the many-sorted logic of here-and-there.

Abstract Refactoring is modifying a program without changing its external behavior. In this paper, we make the concept of external behavior precise for a simple answer set programming language. Then we describe a proof assistant for the task of verifying that refactoring a program in that language is performed correctly.

Abstract Theory of stable models is the mathematical basis of answer set programming. Several results in that theory refer to the concept of the positive dependency graph of a logic program. We describe a modification of that concept and show that the new understanding of positive dependency makes it possible to strengthen some of these results.

Abstract This paper describes a generalization of Clark’s completion that is applicable to logic programs containing arithmetic operations and produces syntactically simple, natural looking formulas. If a set of first-order axioms is equivalent to the completion of a program, then we may be able to find standard models of these axioms by running an answer set solver. As an example, we apply this “reverse completion” procedure to the Sum and Product Puzzle.

Abstract In answer set programming, two groups of rules are considered strongly equivalent if they have the same meaning in any context. In some cases, strong equivalence of programs in the input language of the grounder gringo can be established by deriving rules of each program from rules of the other. The possibility of such proofs has been demonstrated for a subset of that language that includes comparisons, arithmetic operations, and simple choice rules, but not aggregates. This method is extended here to a class of programs in which some uses of the #count aggregate are allowed.

Abstarct In the theory of answer set programming, two groups of rules are called strongly equivalent if, informally speaking, they have the same meaning in any context. The relationship between strong equivalence and the propositional logic of here-and-there allows us to establish strong equivalence by deriving rules of each group from rules of the other. In the process, rules are rewritten as propositional formulas. We extend this method of proving strong equivalence to an answer set programming language that includes operations on integers. The formula representing a rule in this language is a first-order formula that may contain comparison symbols among its predicate constants, and symbols for arithmetic operations among its function constants. The paper is under consideration for acceptance in TPLP.

Abstract This paper continues the line of research aimed at investigating the relationship between logic programs and first-order theories. We extend the definition of program completion to programs with input and output in a subset of the input language of the ASP grounder gringo, study the relationship between stable models and completion in this context, and describe preliminary experiments with the use of two software tools, anthem and vampire, for verifying the correctness of programs with input and output. Proofs of theorems are based on a lemma that relates the semantics of programs studied in this paper to stable models of first-order formulas.

Abstract The input language of the answer set solver clingo is based on the definition of a stable model proposed by Paolo Ferraris. The semantics of the ASP-Core language, developed by the ASP Standardization Working Group, uses the approach to stable models due to Wolfgang Faber, Nicola Leone, and Gerald Pfeifer. The two languages are based on different versions of the stable model semantics, and the ASP-Core document requires, “for the sake of an uncontroversial semantics,” that programs avoid the use of recursion through aggregates. In this paper we prove that the absence of recursion through aggregates does indeed guarantee the equivalence between the two versions of the stable model semantics, and show how that requirement can be relaxed without violating the equivalence property.

Abstract We argue that turning a logic program into a set of completed definitions can be sometimes thought of as the “reverse engineering” process of generating a set of conditions that could serve as a specification for it. Accordingly, it may be useful to define completion for a large class of Answer Set Programming (ASP) programs and to automate the process of generating and simplifying completion formulas. Examining the output produced by this kind of software may help programmers to see more clearly what their program does, and to what degree its behavior conforms with their expectations. As a step toward this goal, we propose here a definition of program completion for a large class of programs in the input language of the ASP grounder gringo, and study its properties.

Abstract This paper describes an approach to the methodology of answer set programming that can facilitate the design of encodings that are easy to understand and provably correct. Under this approach, after appending a rule or a small group of rules to the emerging program, we include a comment that states what has been “achieved” so far. This strategy allows us to set out our understanding of the design of the program by describing the roles of small parts of the program in a mathematically precise way.

Abstract The definition of stable models for propositional formulas with infinite conjunctions and disjunctions can be used to describe the semantics of answer set programming languages. In this note, we enhance that definition by introducing a distinction between intensional and extensional atoms. The symmetric splitting theorem for first-order formulas is then extended to infinitary formulas and used to reason about infinitary definitions.

Abstract 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.

We provide a logical representation of Pearl's structural causal models in the causal calculus of McCain and Turner (1997) and its first-order generalization by Lifschitz. It will be shown that, under this representation, the nonmonotonic semantics of the causal calculus describes precisely the solutions of the structural equations (the causal worlds of the causal model), while the causal logic from Bochman (2004) is adequate for describing the behavior of causal models under interventions (forming submodels).

Abstract This paper defines the syntax and semantics of the input language of the ASP grounder gringo . The definition covers several constructs that were not discussed in earlier work on the semantics of that language, including intervals, pools, division of integers, aggregates with non-numeric values, and lparse-style aggregate expressions. The definition is abstract in the sense that it disregards some details related to representing programs by strings of ASCII characters. It serves as a specification for gringo from Version 4.5 on.

Abstract 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.

Abstract 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.

Abstract Nonmonotonic causal logic, introduced by McCain and Turner (McCain, N. and Turner, H. 1997. Causal theories of action and change. In Proceedings of National Conference on Artificial Intelligence (AAAI), Stanford, CA, 460–465) became the 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 the first-order causal logic.

Abstract 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.

A theorem by Lin and Zhao shows how to turn any nondisjunctive logic program, understood in accordance with the answer set semantics, into an equivalent set of propositional formulas. The set of formulas generated by this process can be significantly larger than the original program. In this article we show (assuming P ⊈ NC 1 / poly , a conjecture from the theory of computational complexity that is widely believed to be true) that this is inevitable: any equivalent translation from logic programs to propositional formulas involves a significant increase in size.

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.

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 Niemelä 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.

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. François 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.

A logic program Π 1 is said to be equivalent to a logic program Π 2 in the sense of the answer set semantics if Π 1 and Π 2 have the same answer sets. We are interested in the following stronger condition: for every logic program, Π, Π 1 , ∪ Π has the same answer sets as Π 2 ∪ Π. The study of strong equivalence is important, because we learn from it how one can simplify a part of a logic program without looking at the rest of it. The main theorem shows that the verification of strong equivalence can be accomplished by cheching the equivalence of formulas in a monotonic logic, called the logic of here-and-there, which is intermediate between classical logic and intuitionistic logic.

Editorial Get access VLADIMIR LIFSCHITZ VLADIMIR LIFSCHITZ University of Texas Search for other works by this author on: Oxford Academic Google Scholar Journal of Logic and Computation, Volume 2, Issue 6, December 1992, Pages 671–673, https://doi.org/10.1093/logcom/2.6.671 Published: 01 December 1992

Some of the formalizations discussed in recent work on action and change use variables for propositional fluents. The authors do not specify whether these variables are meant to range over the set of all propositional fluents or over some part of this set. We show that this seemingly minor detail affects the acceptability of some postulates proposed in the literature. We argue that it is important to distinguish between assertions about arbitrary fluents and assertions about the fluents that belong to a “frame” in the space of situations.

Summary form only given. Research on applications of logic to artificial intelligence has led to the invention of a few useful consequence relations that are not monotonic. They are needed for default reasoning formalization, reasoning about action, introspective reasoning, and negation by failure. The author defines nonmonotonic consequence relations and discusses their importance.>

Let $I = (1, \cdots ,m),\, J = (1, \cdots ,n)$ and $\Delta = (D_i )_{i \in I} $ be a family of subsets $D_i $ of J. A class of algorithms which find a minimum number of $D_i $’s covering $D = \cup _{i \in I} D_i $ is studied. A measure $T(\Delta )$ of the computation time is shown to grow exponentially with the size of the problem in the worst case, namely $\max _\Delta T(\Delta ) > (4^{1/5} )^{\min (m,n')} > 1.319^{\min (m,n')} ,\, n' = |D|$. For $m = n'$ and a large subclass of algorithms, an estimate $\max _\Delta T(\Delta ) < (3/4^{1/3} )^m < (1.890)^m $ is established, so they always perform better than the obvious trivial procedure. Let, on the other hand, be chosen at random. Under condition in $\ln n/\ln m \to \gamma \in (0,\infty )$, it is proven that \[ P\left(m^{c_1 (\gamma )\ln m} \leqq T(\Delta ) \leqq m^{c_2 (\gamma )\ln m} \right) \to 1. \] Hence, asymptotically almost certainly, the computation time is of a considerably lower order than that in Hence, asymptotically almost certainly, the computation time is of a considerably lower order than that in the worst case, but it is still far from being polynomially bounded.

We distinguish between two kinds of mathematical assertions: objective and constructive. An objective assertion describes the universe of mathematical objects; a constructive one describes the (idealized) mathematician's ability to find mathematical objects with various properties. The familiar formalizations of classical mathematics are based on formal languages designed for expressing objective assertions only. The constructivist program stresses, on the contrary, the importance of constructive assertions; moreover, intuitionism claims that constructive activities of the mind constitute the very subject matter of mathematics, and thus questions the semantic status of objective assertions. The purpose of this paper is to show that classical mathematics can be extended to include constructive sentences, so that both objective and constructive properties can be discussed in the framework of the same theory. To achieve this goal, we introduce a new property of mathematical objects, calculability. The word “calculable” may be applied to objects of various types: natural numbers, integers, rational or real numbers, polynomials with rational or real coefficients, etc. In each case it has a different meaning, so that actually we define not one, but many new properties.