Vladimir Lifschitz

KR Conference 2023 Conference Paper

Omega-Completeness of the Logic of Here-and-There and Strong Equivalence of Logic Programs

• Jorge Fandinno
• Vladimir Lifschitz

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.

JELIA Conference 2023 Conference Paper

On Heuer's Procedure for Verifying Strong Equivalence

• Jorge Fandinno
• Vladimir Lifschitz

Abstract In answer set programming, two groups of rules are considered strongly equivalent if replacing one group by the other within any program does not affect the set of stable models. Jan Heuer has designed and implemented a system that verifies strong equivalence of programs in the ASP language mini- gringo. The design is based on the syntactic transformation \(\tau ^*\) that converts mini- gringo programs into first-order formulas. Heuer’s assertion about \(\tau ^*\) that was supposed to justify this procedure turned out to be incorrect, and in this paper we propose an alternative justification for his algorithm. We show also that if \(\tau ^*\) is replaced by the simpler and more natural translation \(\nu \) then the algorithm will still produce correct results.

JELIA Conference 2021 Conference Paper

Transforming Gringo Rules into Formulas in a Natural Way

• Vladimir Lifschitz

Abstract Research on the input language of the ASP grounder gringo uses a translation that converts rules in that language into first-order formulas. That translation often transforms short rules into formulas that are syntactically complex. In this note we identify a class of rules that can be transformed into formulas in a simpler, more natural way. The new translation contributes to our understanding of the relationship between the language of gringo and first-order languages.

FLAP Journal 2017 Journal Article

In Memoriam: Grigori E. Mints, 1939-2014.

• A. Burdman Feferman
• Vladimir Lifschitz

AIJ Journal 2017 Journal Article

Infinitary equilibrium logic and strongly equivalent logic programs

• Amelia Harrison
• Vladimir Lifschitz
• David Pearce
• Agustín Valverde

Strong equivalence is an important concept in the theory of answer set programming. Informally speaking, two sets of rules are strongly equivalent if they have the same meaning in any context. Equilibrium logic was used to prove that sets of rules expressed as propositional formulas are strongly equivalent if and only if they are equivalent in the logic of here-and-there. We extend this line of work to formulas with infinitely long conjunctions and disjunctions, show that the infinitary logic of here-and-there characterizes strong equivalence of infinitary formulas, and give an axiomatization of that logic. This is useful because of the relationship between infinitary formulas and logic programs with local variables.

AAAI Conference 2015 Conference Paper

Pearl’s Causality in a Logical Setting

• Alexander Bochman
• Vladimir Lifschitz

We provide a logical representation of Pearl’s structural causal models in the framework of 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 a causal model), while the causal logic from Bochman (2004) is adequate for describing the behavior of causal models under interventions (forming submodels).

ICAPS Conference 2014 Conference Paper

Planning in Action Language BC while Learning Action Costs for Mobile Robots

• Piyush Khandelwal
• Fangkai Yang
• Matteo Leonetti
• Vladimir Lifschitz
• Peter Stone 0001

The action language BC provides an elegant way of formalizing dynamic domains which involve indirect effects of actions and recursively defined fluents. In complex robot task planning domains, it may be necessary for robots to plan with incomplete information, and reason about indirect or recursive action effects. In this paper, we demonstrate how BC can be used for robot task planning to solve these issues. Additionally, action costs are incorporated with planning to produce optimal plans, and we estimate these costs from experience making planning adaptive. This paper presents the first application of BC on a real robot in a realistic domain, which involves human-robot interaction for knowledge acquisition, optimal plan generation to minimize navigation time, and learning for adaptive planning.

KR Conference 2014 Conference Paper

The Semantics of Gringo and Infinitary Proposition Formulas

• Amelia Harrison
• Vladimir Lifschitz
• Fangkai Yang

IJCAI Conference 2013 Conference Paper

Action Language BC: Preliminary Report

• Joohyung Lee
• Vladimir Lifschitz
• Fangkai Yang

The action description languages B and C have significant common core. Nevertheless, some expressive possibilities of B are difficult or impossible to simulate in C, and the other way around. The main advantage of B is that it allows the user to give Prolog-style recursive definitions, which is important in applications. On the other hand, B solves the frame problem by incorporating the commonsense law of inertia in its semantics, which makes it difficult to talk about fluents whose behavior is described by defaults other than inertia. In C and in its extension C+, the inertia assumption is expressed by axioms that the user is free to include or not to include, and other defaults can be postulated as well. This paper defines a new action description language, called BC, that combines the attractive features of B and C+. Examples of formalizing commonsense domains discussed in the paper illustrate the expressive capabilities of BC and the use of answer set solvers for the automation of reasoning about actions described in this language.

KR Conference 2012 Conference Paper

Logic Programs with Intensional Functions

• Vladimir Lifschitz

Because programs with intensional functions are similar both to nonmonotonic causal theories and to traditional logic programs, they provide a new perspective on the relationship between these two knowledge representation languages. This is one of the reasons why they may be of interest. Another reason is that they allow us to describe effects of actions on non-Boolean fluents directly, in pretty much the same way as causal theories in the sense of (Lifschitz 1997). In traditional logic programming, non-Boolean fluents have to be encoded by Boolean fluents; to express, for instance, that the location of an object x changed between times t and t + 1 we have to write The stable model semantics treats a logic program as a mechanism for specifying its intensional predicates. In this paper we discuss a modification of that semantics in which functions, rather than predicates, are intensional. The idea of the new definition comes from nonmonotonic causal logic.

AIJ Journal 2011 Journal Article

Stable models and circumscription

• Paolo Ferraris
• Joohyung Lee
• Vladimir Lifschitz

The concept of a stable model provided a declarative semantics for Prolog programs with negation as failure and became a starting point for the development of answer set programming. In this paper we propose a new definition of that concept, which covers many constructs used in answer set programming and, unlike the original definition, refers neither to grounding nor to fixpoints. It is based on a syntactic transformation similar to parallel circumscription.

JELIA Conference 2010 Conference Paper

Translating First-Order Causal Theories into Answer Set Programming

• Vladimir Lifschitz
• Fangkai Yang

Abstract Nonmonotonic causal logic became a basis for the semantics of several expressive action languages. Norman McCain and Paolo Ferraris showed how to embed propositional causal theories into logic programming, and this work paved the way to the use of answer set solvers for answering queries about actions described in causal logic. In this paper we generalize these embeddings to first-order causal logic—a system that has been used to simplify the semantics of variables in action descriptions.

IJCAI Conference 2009 Conference Paper

• Paolo Ferraris
• Joohyung Lee
• Vladimir Lifschitz
• Ravi Palla

Splitting a logic program allows us to reduce the task of computing its stable models to similar tasks for smaller programs. This idea is extended here to the general theory of stable models that replaces traditional logic programs by arbitrary firstorder sentences and distinguishes between intensional and extensional predicates. We discuss two kinds of splitting: a set of intensional predicates can be split into subsets, and a formula can be split into its conjunctive terms.

AAAI Conference 2008 Conference Paper

What Is Answer Set Programming?

• Vladimir Lifschitz

Answer set programming (ASP) is a form of declarative programming oriented towards difficult search problems. As an outgrowth of research on the use of nonmonotonic reasoning in knowledge representation, it is particularly useful in knowledge-intensive applications. ASP programs consist of rules that look like Prolog rules, but the computational mechanisms used in ASP are different: they are based on the ideas that have led to the creation of fast satisfiability solvers for propositional logic.

IJCAI Conference 2007 Conference Paper

• Paolo Ferraris
• Joohyung Lee
• Vladimir Lifschitz

The definition of a stable model has provided a declarative semantics for Prolog programs with negation as failure and has led to the development of answer set programming. In this paper we propose a new definition of that concept, which covers many constructs used in answer set programming (including disjunctive rules, choice rules and conditional literals) and, unlike the original definition, refers neither to grounding nor to fixpoints. Rather, it is based on a syntactic transformation, which turns a logic program into a formula of second-order logic that is similar to the formula familiar from the definition of circumscription.

AAAI Conference 2007 Conference Paper

The Semantics of Variables in Action Descriptions

• Vladimir Lifschitz

Action description language C+ is more expressive than ADL in many ways; for instance, it addresses the ramification problem. On the other hand, ADL is based on first-order logic, while C+ is only propositional; expressions with variables, which are frequently used when action domains are described in C+, are merely schemas describing finite sets of causal laws that are formed according to the same pattern. In this paper we propose a new approach to the semantics of action descriptions with variables that combines attractive features of ADL and C+.

AAAI Conference 2006 Conference Paper

A Modular Action Description Language

• Vladimir Lifschitz

“Toy worlds” involving actions, such as the blocks world and the Missionaries and Cannibals puzzle, are often used by researchers in the areas of commonsense reasoning and planning to illustrate and test their ideas. We would like to create a database of general-purpose knowledge about actions that encodes common features of many action domains of this kind, in the same way as abstract algebra and topology represent common features of specific number systems. This paper is a report on the first stage of this project—the design of an action description language in which this database will be written. The new language is an extension of the action language C+. Its main distinctive feature is the possibility of referring to other action descriptions in the definition of a new action domain.

KR Conference 2006 Conference Paper

Actions as Special Cases

• Selim Erdogan
• Vladimir Lifschitz

This paper is motivated by the idea of interaction between two directions of research in knowledge representation: the design of action description languages and the development of libraries of reusable, general-purpose knowledge components. Writing an action description that characterizes actions in terms of their effects, as common today, can be compared to writing a program that does not use standard subroutines. We conjecture that a library of standard descriptions for a number of "basic" actions can facilitate writing, understanding and modifying action descriptions. In this paper, we take some steps towards determining how such a library, written in the action language C+, can be used. When using an instance of a library action description, we relate the library constants to the domain-specific constants by providing definitions. Therefore, a theory of explicit definitions in C+ is developed. To illustrate the use of the library, we show how the action PushBox in the Monkey and Bananas domain can be described as a special case of the "library action" Move.

AIJ Journal 2004 Journal Article

Nonmonotonic causal theories

• Enrico Giunchiglia
• Joohyung Lee
• Vladimir Lifschitz
• Norman McCain
• Hudson Turner

The nonmonotonic causal logic defined in this paper can be used to represent properties of actions, including actions with conditional and indirect effects, nondeterministic actions, and concurrently executed actions. It has been applied to several challenge problems in the theory of commonsense knowledge. We study the relationship between this formalism and other work on nonmonotonic reasoning and knowledge representation, and discuss its implementation, called the Causal Calculator.

AIJ Journal 2004 Journal Article

Representing the Zoo World and the Traffic World in the language of the Causal Calculator

• Varol Akman
• Selim T. Erdoğan
• Joohyung Lee
• Vladimir Lifschitz
• Hudson Turner

The work described in this report is motivated by the desire to test the expressive possibilities of action language C +. The Causal Calculator (CCalc) is a system that answers queries about action domains described in a fragment of that language. The Zoo World and the Traffic World have been proposed by Erik Sandewall in his Logic Modelling Workshop—an environment for communicating axiomatizations of action domains of nontrivial size. The Zoo World consists of several cages and the exterior, gates between them, and animals of several species, including humans. Actions in this domain include moving within and between cages, opening and closing gates, and mounting and riding animals. The Traffic World includes vehicles moving continuously between road crossings subject to a number of restrictions, such as speed limits and keeping a fixed safety distance away from other vehicles on the road. We show how to represent the two domains in the input language of CCalc, and how to use CCalc to test these representations.

AIJ Journal 2002 Journal Article

Answer set programming and plan generation

• Vladimir Lifschitz

The idea of answer set programming is to represent a given computational problem by a logic program whose answer sets correspond to solutions, and then use an answer set solver, such as smodels or dlv, to find an answer set for this program. Applications of this method to planning are related to the line of research on the frame problem that started with the invention of formal nonmonotonic reasoning in 1980.

NMR Workshop 2002 Conference Paper

Why Sam doesn't know calculus

• Vladimir Lifschitz

Solutions to the frame problem available today can be applied to a larger problem that motivated research on nonmonotonic logic in the first place — to formalizing commonsense knowledge and reasoning. In this work, the need for defaults and nonmonotonic conclusions is a small but essential part of the issues involved. Consider, for instance, the following problem from the Common Sense Problem Page (http:/ /wwwformal.Stanford.EDU/leora/cs/). Sam got straight C’s in high school math and has not thought for a moment about math in the 20 years since. Infer that Sam is not the person to ask about a calculus problem. (Contributed by Ernie Davis.) Once we inferred that Sam didn’t know calculus when he graduated from high school, how can we move on to the conclusion that Sam doesn’t know calculus today? The argument is that Sam has not performed any actions that would cause him to learn calculus. This argument is nonmonotonic — it is based on the commonsense law of inertia. We will discuss a representation of this example in a nonmonotonic causal logic and the use of an implementation of that logic, called the Causal Calculator, to justify the required conclusion. This is joint work with the Austin Chapter of Texas Action Group (http://www.cs.utexas.edu/users/tag/).

AIJ Journal 2000 Journal Article

M. Shanahan, Solving the Frame Problem☆☆MIT Press, Cambridge, MA, 1997. 410 pp. $55.00 (cloth). ISBN 0-262-19384-1. http://mitpress.mit.edu/book-home.tcl?isbn = 0262193841.

• Vladimir Lifschitz

AIJ Journal 1997 Journal Article

On the logic of causal explanation

• Vladimir Lifschitz

The McCain-Turner semantics of causal rules is based on a fixpoint construction similar to the one found in the definition of default logic. In the special case when the heads of the rules are literals, it can be equivalently expressed by a translation from sets of rules into sets of propositional formulas. We define a translation from causal logic into classical logic that characterizes the semantics of arbitrary causal rules, without any restrictions on their syntactic form. This translation suggests a way to extend the McCain-Turner logic to nonpropositional causal theories.

AIJ Journal 1997 Journal Article

Representing action: indeterminacy and ramifications

• Enrico Giunchiglia
• G.Neelakantan Kartha
• Vladimir Lifschitz

We define and study a high-level language for describing actions, more expressive than the action language A introduced by Gelfond and Lifschitz. The new language, AR, allows us to describe actions with indirect effects (ramifications), nondeterministic actions, and actions that may be impossible to execute. It has symbols for nonpropositional fluents and for the fluents that are exempt from the commonsense law of inertia. Temporal projection problems specified using the language AR can be represented as nested abnormality theories based on the situation calculus.

AIJ Journal 1995 Journal Article

Nested abnormality theories

• Vladimir Lifschitz

We propose a new approach to the use of circumscription for representing knowledge. Nested abnormality theories are similar to simple abnormality theories introduced by McCarthy, except that their axioms may have a nested structure, with each level corresponding to another application of the circumscription operator. The new style of applying circumscription sometimes leads to more economical and elegant formalizations. Mathematical properties of nested abnormality theories may be easier to investigate. These advantages are demonstrated by recasting several familiar applications of circumscription in the new format, including some examples of inheritance hierarchies, the domain closure assumption and causal minimization. Nested abnormality theories provide also a convenient representation for the explanation closure approach to the frame problem developed by Schubert.

TARK Conference 1994 Conference Paper

Autoepistemic Logic and Introspective Circumscription

• Michael Gelfond
• Vladimir Lifschitz
• Halina Przymusinska
• Grigori Schwarz

We investigate the relationship between two epistemic nonmonotonic formalisms: autoepistemic logic and introspective circumscription. Finitely axiomatized autoepistemic theories are shownto be equivalent to the propositional case of introspective circumscription. This theorem is applied to the problem ofrelating the usual "minimizing" circumscription to autoepistemic logic.

AIJ Journal 1994 Journal Article

Minimal belief and negation as failure

• Vladimir Lifschitz

Fangzhen Lin and Yoav Shoham defined a propositional nonmonotonic logic which uses two independent modal operators. One of them represents minimal knowledge, the other is related to the ideas of justification (as understood in default logic) and of negation as failure. We describe a simplified version of that system, show how quantifiers can be included in it, and study its relation to circumscription and default logic, to logic programming, and to the theory of epistemic queries developed by Hector Levesque and Ray Reiter.

AAAI Conference 1993 Conference Paper

Restricted Monotonicity

• Vladimir Lifschitz

Vladimir Lifschitz* Department of Computer Sciences and Department of Philosophy University of Texas at Austin Austin, TX 78712 Examples ation. When additional assumptions are made, the class of domains that are being described becomes smaller, so that the class of conclusions that are true in all the domains becomes larger. As a result, a satisfactory solution to a parametric knowledge representation problem on the basis of some nonmonotonic formali’ sm can be expected to have a certain formal property, that we call restricted monotonicity. We argue that it is important to recognize parametric knowledge representation problems and to verify restricted monotonicity fir their proposed solutions.

AIJ Journal 1990 Journal Article

Frames in the space of situations

• Vladimir Lifschitz

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.

NMR Workshop 1989 Conference Paper

Benchmark Problems for Formal Non-Monotonic Reasoning, Version 2. 00

• Vladimir Lifschitz

NMR Workshop 1989 Conference Paper

Compiling Circumscriptive Theories into Logic Programs

• Michael Gelfond
• Vladimir Lifschitz

Abstract We study the possibility of reducing some special cases of circumscription to logic programming. The description of a given circumscriptive theory T can be sometimes transformed into a logic program II, so that, by running II, we can determine whether a given ground literal is provable in T. The method is applicable, in particular, to some formalizations of tree-structured inheritance systems with exceptions.

AIJ Journal 1989 Journal Article

Miracles in formal theories of action

• Vladimir Lifschitz
• Arkady Rabinov

Most work on reasoning about action is based on the implicit assumption that there are no events happening in the world concurrently with the actions that are being carried out. We discuss the possibility of relaxing this assumption and treating it as a default principle—if it is inconsistent with the given facts, then we will admit the possibility of unknown events, “miracles, ” that, along with the given actions, contribute to the properties of the new situation. The formalism proposed by one of the authors in the paper, Formal Theories of Action, does not treat “miracles” properly. We discuss a modification of that approach which corrects this problem.

IJCAI Conference 1989 Conference Paper

Things That Change by Themselves

• Vladimir Lifschitz
• Arkady Rabinov

AAAI Conference 1987 Conference Paper

Circumscriptive Theories: A Logic-Based Framework for Knowledge Representation, Preliminary Report

• Vladimir Lifschitz

The use of circumscription for formalizing commonsense knowledge and reasoning requires that a circumscription policy be selected for each particular application: we should specify which predicates are circumscribed, which predicates and functions are allowed to vary, what priorities between the circumscribed predicates are established, etc. The circumscription policy is usually described either informally or using suitable metamathematical notation. In this paper we propose a simple and general formalism which permits describing circumscription policies by axioms, included in the knowledge base along with the axioms describing the objects of reasoning. This method allows us to formalize some important forms of metalevel reasoning in the circumscriptive theory itself.

IJCAI Conference 1987 Conference Paper

Formal Theories of Action (Preliminary Report)

• Vladimir Lifschitz

AIJ Journal 1986 Journal Article

On the satisfiability of circumscription

• Vladimir Lifschitz

Etherington, Mercer and Reiter showed, on the basis of ideas of Bossu and Siegel, that circumscription cannot lead to inconsistency for universal formulas. We extend this result in three directions: to formulas of a more general syntactic form, to circumscription with some predicate symbols allowed to vary, and to prioritized circumscription.

AAAI Conference 1986 Conference Paper

Pointwise Circumscription: Preliminary Report

• Vladimir Lifschitz

Circumscription is the minimization of predicates subject to restrictions expressed by predicate formulas. We propose a modified notion of circumscription so that, instead of being a single minimality condition, it becomes an "infinite conjunction" of "local" minimality conditions; each of these conditions expresses the impossibility of changing the value of a predicate from true to false at one point. We argue that this "pointwise" circumscription is conceptually simpler than the traditional "global" approach and, at the same time, leads to generalizations with the additional flexibility needed in applications to the theory of commonsense reasoning.

AIJ Journal 1985 Journal Article

Closed-world databases and circumscription

• Vladimir Lifschitz

We compare two forms of non-monotonic reasoning: closed-world evaluation of queries in databases and circumscription. For closed E-saturated databases we show that the closed-world assumption, if consistent, is equivalent to circumscribing all predicates in the database.

IJCAI Conference 1985 Conference Paper

Computing Circumscription

• Vladimir Lifschitz

NMR Workshop 1984 Conference Paper

Some Results on Circumscription

• Vladimir Lifschitz