Optimal models of disjunctive logic programs: semantics, complexity, and computation

Almost all semantics for logic programs with negation identify a set, SEM(P), of models of program P, as the intended semantics of P, and any model M in this class is considered a possible meaning of P with regard to the semantics the user has in mind. Thus, for example, in the case of stable models [M. Gelfond et al., (1988)], choice models [D. Sacca et al., (1990)], answer sets [M. Gelfond et al., (1991)], etc., different possible models correspond to different ways of "completing" the incomplete information in the logic program. However, different end-users may have different ideas on which of these different models in SEM(P) is a reasonable one from their point of view. For instance, given SEM(P), user U/sub 1/ may prefer model M/sub 1//spl isin/SEM(P) to model M/sub 2//spl isin/SEM(P) based on some evaluation criterion that she has. We develop a logic program semantics based on optimal models. This semantics does not add yet another semantics to the logic programming arena - it takes as input an existing semantics SEM(P) and a user-specified objective function Obj, and yields a new semantics Opt(P)_/spl sube/ SEM(P) that realizes the objective function within the framework of preferred models identified already by SEM(P). Thus, the user who may or may not know anything about logic programming has considerable flexibility in making the system reflect her own objectives by building "on top" of existing semantics known to the system. In addition to the declarative semantics, we provide a complete complexity analysis and algorithms to compute optimal models under varied conditions when SEM(P) is the stable model semantics, the minimal models semantics, and the all-models semantics.     

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.     

Locally Determined Logic Programs and Recursive Stable Models

In general, the set of stable models of a recursive logic program can be quite complex. For example, it follows from results of Marek, Nerode, and Remmel [Ann. Pure and Appl. Logic (1992)] that there exists finite predicate logic programs and recursive propositional logic programs which have stable models but no hyperarithmetic stable models. In this paper, we shall define several conditions which ensure that recursive logic program P has a stable model which is of low complexity, e.g., a recursive stable model, a polynomial time stable model, or a stable model which lies in a low level of the polynomial time hierarchy.     

Complexity and undecidability results for logic programming

This paper surveys complexity, degree of uncomputability, and expressive power results for logic programming. Some major decision problem complexity results and other results for logic programming are also covered. It also proves several new results filling in previous gaps in the literature. The paper considers seven logic programming semantics: the van Emden-Kowalski semantics for definite (Horn) logic programs; the perfect model semantics for stratified and for locally stratified logic programs; and the two- and three-valued program completion semantics, the well-founded semantics, and the stable semantics, all for normal logic programs, under skeptical inference. The main results concern expressibility and query complexity/uncomputability in five contexts: for propositional logic programs, for first order logic programs with infinite Herbrand universes on their Herbrand universes (a closed domain assumption), for first order logic programs with infinite Herbrand universes on those universes extended with infinitely many new elements (an open domain assumption), and for logic programs without function or constant symbols evaluated over varying extensional databases (DATALOG-type results, data complexity results only) under both closed and open domain assumptions. Several of the open domain assumption results are new to this paper. Other results surveyed are (1) results about the family of all stable models of a program and (2) decision questions about when a logic program has nice properties with respect to a semantics (e.g., a unique stable model). One decision result, for well-founded semantics, is new to this paper.Work supported in part by NSF grant IRI-8905166.     

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     

The expressiveness of locally stratified programs

This paper completes an investigation of the logical expressibility of finite, locally stratified, general logic programs. We show that every hyperarithmetic set can be defined by a suitably chosen locally stratified logic program (as a set of values of a predicate over its perfect model). This is an optimal result, since the perfect model of a locally stratified program is itself an implicitly definable hyperarithmetic set (under a recursive coding of the Herbrand base); hence, to obtain all hyperarithmetic sets requires something new, in this case selecting one predicate from the model. We find that the expressive power of programs does not increase when one considers the programs which have a unique stable model or a total well-founded model. This shows that all these classes of structures (perfect models of logically stratified logic programs, well-founded models which turn out to be total, and stable models of programs possessing a unique stable model) are all closely connected with Kleene's hyperarithmetical hierarchy. Thus, for general logic programming, negation with respect to two-valued logic is related to the hyperarithmetic hierarchy in the same way as Horn logic is to the class of recursively enumerable sets. In particular, a set is definable in the well-founded semantics by a programP whose well-founded partial model is total iff it is hyperarithmetic.Research partially supported by the U.S. Army Research Office through the Mathematical Sciences Institute of Cornell University.Research partially supported by NSF Grant IRI-9012902 and partially supported by the U.S. Army Research Office through the Mathematical Sciences Institute of Cornell University.Research partially supported by NSF Grant IRI-8905166 and partially supported by the U.S. Army Research Office through the Mathematical Sciences Institute of Cornell University.     

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.     

Linux进程语义安全性检测的稳定模型

现有进程检测方法,检测的目标是系统调用的序列的排列关联,忽略了语义中潜在的异常。稳定模型是逻辑程序的语义模型,可以用以发现并修改逻辑程序的异常问题。该文以系统调用为基本检测点,采用逻辑程序描述进程的基本语义逻辑,用稳定模型表达进程的检测语义。系统定义进程的一系列安全语义规则,在进程执行中,计算安全语义规则与进程逻辑之间的稳定模型,得到安全语义的可计算性结论。论文最后,给出了一个Linux系统中的进程语义安全性检测的基本框架。     

Computation of stable models and its integration with logical queryprocessing

The well-founded semantics and the stable model semantics capture intuitions of the skeptical and credulous semantics in nonmonotonic reasoning, respectively. They represent the two dominant proposals for the declarative semantics of deductive databases and logic programs. However, neither semantics seems to be suitable for all applications. We have developed an efficient implementation of goal-oriented effective query evaluation under the well-founded semantics. It produces a residual program for subgoals that are relevant to a query, which contains facts for true instances and clauses with body literals for undefined instances. We present a simple method of stable model computation that can be applied to the residual program of a query to derive answers with respect to stable models. The method incorporates both forward and backward chaining to propagate the assumed truth values of ground atoms, and derives multiple stable models through backtracking. Users are able to request that only stable models satisfying certain conditions be computed. A prototype has been developed that provides integrated query evaluation under the well-founded semantics, the stable models, and ordinary Prolog execution. We describe the user interface of the prototype and present some experimental results     

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.     

Possibilistic uncertainty handling for answer set programming

In this work, we introduce a new framework able to deal with a reasoning that is at the same time non monotonic and uncertain. In order to take into account a certainty level associated to each piece of knowledge, we use possibility theory to extend the non monotonic semantics of stable models for logic programs with default negation. By means of a possibility distribution we define a clear semantics of such programs by introducing what is a possibilistic stable model. We also propose a syntactic process based on a fix-point operator to compute these particular models representing the deductions of the program and their certainty. Then, we show how this introduction of a certainty level on each rule of a program can be used in order to restore its consistency in case of the program has no model at all. Furthermore, we explain how we can compute possibilistic stable models by using available softwares for Answer Set Programming and we describe the main lines of the system that we have developed to achieve this goal.     

Stable inference as intuitionistic validity

The paper characterises the nonmonotonic inference relation associated with the stable model semantics for logic programs as follows: a formula is entailed by a program in the stable model semantics if and only if it belongs to every intuitionistically complete and consistent extension of the program formed by adding only negated atoms. In place of intuitionistic logic, any proper intermediate logic can be used.     

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.     

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

     

Set based logic programming

In a previous paper (Blair et al. 2001), the authors showed that the mechanism underlying Logic Programming can be extended to handle the situation where the atoms are interpreted as subsets of a given space X. The view of a logic program as a one-step consequence operator along with the concepts of supported and stable model can be transferred to such situations. In this paper, we show that we can further extend this paradigm by creating a new one-step consequence operator by composing the old one-step consequence operator with a monotonic idempotent operator (miop) in the space of all subsets of X, 2 ^X . We call this extension set based logic programming. We show that such a set based formalism for logic programming naturally supports a variety of options. For example, if the underlying space has a topology, one can insist that the new one-step consequence operator always produces a closed set or always produces an open set. The flexibility inherent in the semantics of set based logic programs is due to both the range of natural choices available for specifying the semantics of negation, as well as the role of monotonic idempotent operators (miops) as parameters in the semantics. This leads to a natural type of polymorphism for logic programming, i.e. the same logic program can produce a variety of outcomes depending on the miop associated with the semantics. We develop a general framework for set based programming involving miops. Among the applications, we obtain integer-based representations of real continuous functions as stable models of a set based logic program.      

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.     

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.     

Stable and extension class theory for logic programs and default logics

The stable model semantics (cf. Gelfond and Lifschitz [1]) for logic programs suffers from the problem that programs may not always have stable models. Likewise, default theories suffer from the problem that they do not always have extensions. In such cases, both these formalisms for non-monotonic reasoning have an inadequate semantics. In this paper, we propose a novel idea-that of extension classes for default logics, and of stable classes for logic programs. It is shown that the extension class and stable class semantics extend the extension and stable model semantics respectively. This allows us to reason about inconsistent default theories, and about logic programs with inconsistent completions. Our work extends the results of Marek and Truszczynski [2] relating logic programming and default logics.