Disjunctive LP+integrity constraints= stable model semantics

We show that stable models of logic programs may be viewed as minimal models of programs that satisfy certain additional constraints. To do so, we transform the normal programs into disjunctive logic programs and sets of integrity constraints. We show that the stable models of the normal program coincide with the minimal models of the disjunctive program thatsatisfy the integrity constraints. As a consequence, the stable model semantics can be characterized using theextended generalized closed world assumption for disjunctive logic programs. Using this result, we develop a bottomup algorithm for function-free logic programs to find all stable models of a normal program by computing the perfect models of a disjunctive stratified logic program and checking them for consistency with the integrity constraints. The integrity constraints provide a rationale as to why some normal logic programs have no stable models.     

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 \) .

     

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.     

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.     

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.     

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.     

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.     

Autoepistemic logics as a unifying framework for the semantics of logic programs

In this paper, it is shown that a three-valued autoepistemic logic provides an elegant unifying framework for some of the major semantics of normal and disjunctive logic programs and logic programs with classical negation, namely, the stable semantics, the well-founded semantics, supported models, Fitting's semantics, Kunen's semantics, the stationary semantics, and answer sets. For the first time, so many semantics are embedded into one logic. The framework extends previous results—by Gelfond, Lifschitz, Marek, Subrahmanian, and Truszczynski —on the relationships between logic programming and Moore's autoepistemic logic. The framework suggests several new semantics for negation-as-failure. In particular, we will introduce the epistemic semantics for disjunctive logic programs. In order to motivate the epistemic semantics, an interesting class of applications called ignorance tests will be formalized; it will be proved that ignorance tests can be defined by means of the epistemic semantics, but not by means of the old semantics for disjunctive programs. The autoepistemic framework provides a formal foundation for an environment that integrates different forms of negation. The role of classical negation and various forms of negation-by-failure in logic programming will be briefly discussed.     

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.     

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.     

Partial equilibrium logic

Partial equilibrium logic (PEL) is a new nonmonotonic reasoning formalism closely aligned with logic programming under well-founded and partial stable model semantics. In particular it provides a logical foundation for these semantics as well as an extension of the basic syntax of logic programs. In this paper we describe PEL, study some of its logical properties and examine its behaviour on disjunctive and nested logic programs. In addition we consider computational features of PEL and study different approaches to its computation.     

On computing logic programs

In this paper we present and compare some classical problem-solving methods for computing the stable models of logic programs with negation. Using a graph theoretic representation of logic programs and their stable models, we discuss and compare linear programming, propositional satisfiability, constraint satisfaction, and graph methods.     

Iterative belief revision in extended logic programming

Extended logic programming augments conventional logic programming with both default and explicit negation. Several semantics for extended logic programs have been proposed that extend the well-founded semantics for logic programs with default negation (called normal programs). We show that two of these extended semantics are intractable; both Dung's grounded argumentation semantics and the well-founded semantics of Alferes et al. are NP-hard. Nevertheless, we also show that these two semantics have a common core, a more restricted form of the grounded semantics, which is tractable and can be computed iteratively in quadratic time. Moreover, this semantics is a representative of a rich class of tractable semantics based on a notion of iterative belief revision.     

A Fixpoint Semantics for Stratified Databases

Przmusinski extended the notion of stratified logic programs,developed by Apt,Blair and Walker,and by van Gelder,to stratified databases that allow both negative premises and disjunctive consequents.However,he did not provide a fixpoint theory for such class of databases.On the other hand,although a fixpoint semantics has been developed by Minker and Rajasekar for non-Horn logic programs,it is tantamount to traditional minimal model semantics which is not sufficient to capture the intended meaning of negation in the premises of clauses in stratified databases.In this paper,a fixpoint approach to stratified databases is developed,which corresponds with the perfect model semantics.Moreover,algorithms are proposed for computing the set of perfect models of a stratified database.     

基于自动推理技术的智能规划方法

对几种智能规划方法中利用的逻辑演绎与推理技术予以分析,分别介绍利用命题逻辑的基于可满足性的规划方法与规划系统,利用模态逻辑与析取推理的Conformant规划方法与规划系统,利用非单调逻辑的规划方法和利用模糊描述逻辑的Flexible规划方法,并结合国际规划竞赛和相关论文等的实验结论说明上述方法的有效性和可行性.最后,提出目前基于自动推理技术的智能规划方法所面临的挑战、可能的处理方法以及与之相关的研究热点与趋势.     

Planning as satisfiability: parallel plans and algorithms for plan search

We address two aspects of constructing plans efficiently by means of satisfiability testing: efficient encoding of the problem of existence of plans of a given number t of time points in the propositional logic and strategies for finding plans, given these formulae for different values of t.For the first problem we consider three semantics for plans with parallel operator application in order to make the search for plans more efficient. The standard semantics requires that parallel operators are independent and can therefore be executed in any order. We consider a more relaxed definition of parallel plans which was first proposed by Dimopoulos et al., as well as a normal form for parallel plans that requires every operator to be executed as early as possible. We formalize the semantics of parallel plans emerging in this setting and present translations of these semantics into the propositional logic. The sizes of the translations are asymptotically optimal. Each of the semantics is constructed in such a way that there is a plan following the semantics exactly when there is a sequential plan, and moreover, the existence of a parallel plan implies the existence of a sequential plan with as many operators as in the parallel one.For the second problem we consider strategies based on testing the satisfiability of several formulae representing plans of n time steps for several values of n concurrently by several processes. We show that big efficiency gains can be obtained in comparison to the standard strategy of sequentially testing the satisfiability of formulae for an increasing number of time steps.