Static semantics for normal and disjunctive logic programs

In this paper, we propose a newsemantic framework for disjunctive logic programming by introducingstatic expansions of disjunctive programs. The class of static expansions extends both the classes of stable, well-founded and stationary models of normal programs and the class of minimal models of positive disjunctive programs. Any static expansion of a programP provides the corresponding semantics forP consisting of the set of all sentences logically implied by the expansion. We show that among all static expansions of a disjunctive programP there is always theleast static expansion, which we call thestatic completion ¯P ofP. The static completion¯P can be defined as the least fixed point of a naturalminimal model operator and can be constructed by means of a simpleiterative procedure. The semantics defined by the static completion¯P is called thestatic semantics ofP. It coincides with the set of sentences that are true inall static expansions ofP. For normal programs, it coincides with the well-founded semantics. The class of static expansions represents a semantic framework which differs significantly from the other semantics proposed recently for disjunctive programs and databases. It is also defined for a much broader class of programs.Dedicated to Jack MinkerPartially supported by the National Science Foundation grant # IRI-9313061.     

On the computational cost of disjunctive logic programming: Propositional case

This paper addresses complexity issues for important problems arising with disjunctive logic programming. In particular, the complexity of deciding whether a disjunctive logic program is consistent is investigated for a variety of well-known semantics, as well as the complexity of deciding whether a propositional formula is satisfied by all models according to a given semantics. We concentrate on finite propositional disjunctive programs with as well as without integrity constraints, i.e., clauses with empty heads; the problems are located in appropriate slots of the polynomial hierarchy. In particular, we show that the consistency check is ₂ ^p -complete for the disjunctive stable model semantics (in the total as well as partial version), the iterated closed world assumption, and the perfect model semantics, and we show that the inference problem for these semantics is ₂ ^p -complete; analogous results are derived for the answer sets semantics of extended disjunctive logic programs. Besides, we generalize previously derived complexity results for the generalized closed world assumption and other more sophisticated variants of the closed world assumption. Furthermore, we use the close ties between the logic programming framework and other nonmonotonic formalisms to provide new complexity results for disjunctive default theories and disjunctive autoepistemic literal theories.Parts of the results in this paper appeared in form of an abstract in the Proceedings of the Twelfth ACM SIGACT SIGMOD-SIGART Symposium on Principles of Database Systems (PODS-93), pp. 158–167. Other parts appeared in shortened form in the Proceedings of the International Logic Programming Symposium, Vancouver, October 1993 (ILPS-93), pp. 266–278. MIT Press.     

Disjunctive Stable Models: Unfounded Sets, Fixpoint Semantics, and Computation

Disjunctive logic programs have become a powerful tool in knowledge representation and commonsense reasoning. This paper focuses on stable model semantics, currently the most widely acknowledged semantics for disjunctive logic programs. After presenting a new notion of unfounded sets for disjunctive logic programs, we provide two declarative characterizations of stable models in terms of unfounded sets. One shows that the set of stable models coincides with the family of unfounded-free models (i.e., a model is stable iff it contains no unfounded atoms). The other proves that stable models can be defined equivalently by a property of their false literals, as a model is stable iff the set of its false literals coincides with its greatest unfounded set. We then generalize the well-founded operator to disjunctive logic programs, give a fixpoint semantics for disjunctive stable models and present an algorithm for computing the stable models of function-free programs. The algorithm's soundness and completeness are proved and some complexity issues are discussed.     

A logical framework for querying and repairing inconsistent databases

In this paper, we address the problem of managing inconsistent databases, i.e., databases violating integrity constraints. We propose a general logic framework for computing repairs and consistent answers over inconsistent databases. A repair for a possibly inconsistent database is a minimal set of insert and delete operations which makes the database consistent, whereas a consistent answer is a set of tuples derived from the database, satisfying all integrity constraints. In our framework, different types of rules defining general integrity constraints, repair constraints (i.e., rules defining conditions on the insertion or deletion of atoms), and prioritized constraints (i.e., rules defining priorities among updates and repairs) are considered. We propose a technique based on the rewriting of constraints into (prioritized) extended disjunctive rules with two different forms of negation (negation as failure and classical negation). The disjunctive program can be used for two different purposes: to compute "repairs" for the database and produce consistent answers, i.e., a maximal set of atoms which do not violate the constraints. We show that our technique is sound, complete (each preferred stable model defines a repair and each repair is derived from a preferred stable model), and more general than techniques previously proposed.     

Extremal problems in logic programming and stable model computation

We study the following problem: given a class of logic programs ¢, determine the maximum number of stable models of a program from ©. We establish the maximum for the class of all logic programs with at most n clauses, and for the class of all logic programs of size at most n. We also characterize the programs for which the maxima are attained. We obtained similar results for the class of all disjunctive logic programs with at most n clauses, each of length at most m, and for the class of all disjunctive logic programs of size at most n. Our results on logic programs have direct implication for the design of algorithms to compute stable models. Several such algorithms, similar in spirit to the Davis-Putnam procedure, are described in the paper. Our results imply that there is an algorithm that finds all stable models of a program with n clauses after considering the search space of size O(3^n/3) in the worst case. Our results also provide some insights into the question of representability of families of sets as families of stable models of logic programs.     

Well-founded and stationary models of logic programs

We investigate the class ofstationary or partial stable models of normal logic programs. This important class of models includes all (total)stable models, and, moreover, thewell-founded model is always its smallest member. Stationary models have several natural fixed-point definitions and can be equivalently obtained as expansions or extensions of suitable autoepistemic or default theories. By taking a particular subclass of this class of models one can obtain different semantics of logic programs, including the stable semantics and the well-founded semantics. Stationary models can be also naturally extended to the class of all disjunctive logic programs. These features of stationary models designate them as an important class of models with applications reaching far beyond the realm of logic programming.Partially supported by the National Science Foundation grant #IRI-9313061.     

Logic Programs,Compatibility and Forward Chaining Construction

Logic programming under the stable model semantics is proposed as a non-monotonic language for knowledge representation and reasoning in artificial intelligence. In this paper, we explore and extend the notion of compatibility and the Λ operator, which were first proposed by Zhang to characterize default theories. First, we present a new characterization of stable models of a logic program and show that an extended notion of compatibility can characterize stable submodels. We further propose the notion of weak auto-compatibility which characterizes the Normal Forward Chaining Construction proposed by Marek, Nerode and Remmel. Previously, this construction was only known to construct the stable models of FC-normal logic programs, which turn out to be a proper subclass of weakly auto-compatible logic programs. We investigate the properties and complexity issues for weakly auto-compatible logic programs and compare them with some subclasses of logic programs.     

An alternative approach to the semantics of disjunctive logic programs and deductive databases

In this paper, we study a new semantics of logic programming and deductive databases. Thepossible model semantics is introduced as a declarative semantics of disjunctive logic programs. The possible model semantics is an alternative theoretical framework to the classical minimal model semantics and provides a flexible inference mechanism for inferring negation in disjunctive logic programs. We also present a proof procedure for the possible model semantics and show that the possible model semantics has an advantage from the computational complexity point of view.This is a revised and extended version of the paper [36] which was presented at the Tenth International Conference on Logic Programming, Budapest, 21–25 June 1993.     

Propositional semantics for disjunctive logic programs

In this paper we study the properties of the class of head-cycle-free extended disjunctive logic programs (HEDLPs), which includes, as a special case, all nondisjunctive extended logic programs. We show that any propositional HEDLP can be mapped in polynomial time into a propositional theory such that each model of the latter corresponds to an answer set, as defined by stable model semantics, of the former. Using this mapping, we show that many queries over HEDLPs can be determined by solving propositional satisfiability problems. Our mapping has several important implications: It establishes the NP-completeness of this class of disjunctive logic programs; it allows existing algorithms and tractable subsets for the satisfiability problem to be used in logic programming; it facilitates evaluation of the expressive power of disjunctive logic programs; and it leads to the discovery of useful similarities between stable model semantics and Clark's predicate completion.     

Comparison of Semantics of Disjunctive Logic Programs Based on Model-Equivalent Reduction

In this paper, it is shown that stable model semantics, perfect model semantics, and partial stable model semantics of disjunctive logic programs have the same expressive power with respect to the polynomial-time model-equivalent reduction. That is, taking perfect model semantics and stable model semantic as an example, any logic program P can be transformed in polynomial time to another logic program P＇ such that perfect models （resp. stable models） of P i-i correspond to stable models （resp. perfect models） of P＇, and the correspondence can be computed also in polynomial time. However, the minimal model semantics has weaker expressiveness than other mentioned semantics, otherwise, the polynomial hierarchy would collapse to NP.     

Stable semantics for disjunctive programs

We introduce the stable model semantics fordisjunctive logic programs and deductive databases, which generalizes the stable model semantics, defined earlier for normal (i.e., non-disjunctive) programs. Depending on whether only total (2-valued) or all partial (3-valued) models are used we obtain thedisjunctive stable semantics or thepartial disjunctive stable semantics, respectively. The proposed semantics are shown to have the following properties:

? For normal programs, the disjunctive (respectively, partial disjunctive) stable semantics coincides with thestable (respectively,partial stable) semantics.

? For normal programs, the partial disjunctive stable semantics also coincides with thewell-founded semantics.

? For locally stratified disjunctive programs both (total and partial) disjunctive stable semantics coincide with theperfect model semantics.

? The partial disjunctive stable semantics can be generalized to the class ofall disjunctive logic programs.

? Both (total and partial) disjunctive stable semantics can be naturally extended to a broader class of disjunctive programs that permit the use ofclassical negation.

? After translation of the programP into a suitable autoepistemic theory \( \hat P \) the disjunctive (respectively, partial disjunctive) stable semantics ofP coincides with the autoepistemic (respectively, 3-valued autoepistemic) semantics of \( \hat P \) .

     

Classical negation in logic programs and disjunctive databases

An important limitation of traditional logic programming as a knowledge representation tool, in comparison with classical logic, is that logic programming does not allow us to deal directly with incomplete information. In order to overcome this limitation, we extend the class of general logic programs by including classical negation, in addition to negation-as-failure. The semantics of such extended programs is based on the method of stable models. The concept of a disjunctive database can be extended in a similar way. We show that some facts of commonsense knowledge can be represented by logic programs and disjunctive databases more easily when classical negation is available. Computationally, classical negation can be eliminated from extended programs by a simple preprocessor. Extended programs are identical to a special case of default theories in the sense of Reiter.     

The Least Fixpoint Transformation for Disjunctive Logic Programs

The paradigm of disjunctive logic programming(DLP)enhances greatly the expressive power of normal logic programming(NLP)and many(declarative)semantics have been defined for DLP to cope with various problems of knowledge representation in artificial intelligence.However,the expressive ability of the semantics and the soundness of program transformations for DLP have been rarely explored.This paper defines an immediate consequence operatro T^GP for each disjunctive program and shows that T^GP has the least and computable fixpoint Lft(P),Lft is,in fact,a program transformation for DLP,which transforms all disjunctive programs into negative programs.It is shown that Lft preserves many key semantics,including the disjunctive stable models,well-founded model,disjunctive argunent semantics DAS,three-valued models,ect.Thic means that every disjunctive program P has a unique canonical form Lft(P)with respect to these semantics.As a result,the work in this paper provides a unifying framework for studying the expressive ability of various semantics for DLP On the other hand,the computing of the above semantics for negative programs is ust a trivial task,therefore,Lft(P)is also an optimization method for DLP.Another application of Lft is to derive some interesting semantic results for DLP.     

On the partial semantics for disjunctive deductive databases

Partial stable models for deductive databases, i.e., normal function-free logic programs (also called datalog programs), have two equivalent definitions: one based on 3-valued logics and another based on the notion of unfounded set. The notion of partial stable model has been extended to disjunctive deductive databases using 3-valued logics. In this paper, a characterization of partial stable models for disjunctive datalog programs is given using a suitable extension of the notion of unfounded set. Two interesting sub-classes of partial stable models, M-stable (Maximal-stable) (also called regular models, preferred extension,and maximal stable classes) and L-stable (Least undefined-stable) models, are then extended from normal to disjunctive datalog programs. On the one hand, L-stable models are shown to be the natural relaxation of the notion of total stable model; on the other hand the less strict M-stable models, endowed with a nice modularity property, may be appealing from the programming and computational point of view. M-stable and L-stable models are also compared with the regular models for disjunctive datalog programs recently proposed in the literature.     

First-order logic characterization of program properties

A program is first-order reducible (FO-reducible) w.r.t. a set IC of integrity constraints if there exists a first-order theory T such that the set of models for T is exactly the set of intended models for the program w.r.t. all possible EDBs. In this case, we say that P is FO-reducible to T w.r.t. IC. For FO-reducible programs, it is possible to characterize, using first-order logic implications, properties of programs that are related to all possible EDBs as in the database context. These properties include, among others, containment of programs, independence of updates w.r.t. queries and integrity constraints, and characterization and implication of integrity constraints in programs, all of which have no known proof procedures. Therefore, many important problems formalized in a nonstandard logic can be dealt with by using the rich reservoir of first-order theorem-proving tools, provided that the program is FO-reducible. The following classes of programs are shown to be FO-reducible: (1) a stratified acyclic program P is FO-reducible to comp(P)∪IC w.r.t. IC for any set IC of constraints; (2) a general chained program P is FO-reducible to comp(P')∪IC w.r.t. certain acyclicity constraints IC; and (3) a bounded program P is FO-reducible to comp(P')∪IC w.r.t. any set IC of constraints, where P' is a nonrecursive program equivalent to P. Some heuristics for constructing FO-reducible programs are described     

Semantic Forcing in Disjunctive Logic Programs

We propose a semantics for disjunctive logic programs, based on the single notion of forcing. We show that the semantics properly extends, in a natural way, previous approaches. A fixpoint characterization is also provided. We also take a closer look at the relationship between disjunctive logic programs and disjunctive-free logic programs. We present certain criteria under which a disjunctive program is semantically equivalent with its disjunctive-free (shifted) version.     

Active Integrity Constraints for Database Consistency Maintenance

This paper introduces active integrity constraints (AICs), an extension of integrity constraints for consistent database maintenance. An active integrity constraint is a special constraint whose body contains a conjunction of literals which must be false and whose head contains a disjunction of update actions representing actions (insertions and deletions of tuples) to be performed if the constraint is not satisfied (that is its body is true). The AICs work in a domino-like manner as the satisfaction of one AIC may trigger the violation and therefore the activation of another one. The paper also introduces founded repairs, which are minimal sets of update actions that make the database consistent, and are specified and “supported” by active integrity constraints. The paper presents: 1) a formal declarative semantics allowing the computation of founded repairs and 2) a characterization of this semantics obtained by rewriting active integrity constraints into disjunctive logic rules, so that founded repairs can be derived from the answer sets of the derived logic program. Finally, the paper studies the computational complexity of computing founded repairs.     

Translating Multi-Agent Autoepistemic Logic into Logic Program

In order to develop a proof procedure of multi-agent autoepistemic Logic (MAEL), a natural framework to formalize belief and reasoning including inheritance, persistence, and causality, we introduce a method that translates a MAEL theory into a logic program with integrity constraints. It is proved that there exists one-to-one correspondence between extensions of a MAEL theory and stable models of a logic program translated from it. Our approach has the following advantages: (1) We can obtain all extensions of a MAEL theory if we compute all stable models of the translated logic program. (2) We can fully use efficient techniques or systems for computing stable models of a logic program. We also investigate the properties of reasoning in MAEL through this translation. The fact that the extension computing problem can be reduced to the stable model computing problem implies that there are close relationships between MAEL and other formalizations of nonmonotonic reasoning.     

Stable models and difference logic

The paper studies the relationship between logic programs with the stable model semantics and difference logic recently considered in the Satisfiability Modulo Theories framework. Characterizations of stable models in terms of level rankings are developed building on simple linear integer constraints allowed in difference logic. Based on the characterizations translations are devised which map normal programs to difference logic formulas capturing stable models of a program as satisfying valuations of the resulting formula. The translations make it possible to use a solver for difference logic to compute stable models of logic programs.