描述逻辑程序系统的设计与实现

Eiter等人为语义网提出的回答集程序和描述逻辑相结合的描述逻辑程序,获得了本体上的非单调表达和推理能力。王以松等人证明了描述逻辑程序的完备化和环公式可以精确刻画描述逻辑程序的回答集。在此基础上,进一步证明了若完备化公式的模型不是回答集则一定存在终止环公式反例,它们是多项式时间可计算的。设计并实现了借助SAT求解器MiniSAT以及描述逻辑推理机RacerPro计算描述逻辑强回答集的原型DLP_SAT。实验结果表明,该原型能有效地计算一些熟知的描述逻辑程序的强回答集。     

Nested expressions in logic programs

We extend the answer set semantics to a class of logic programs with nested expressions permitted in the bodies and heads of rules. These expressions are formed from literals using negation as failure, conjunction (,) and disjunction (;) that can be nested arbitrarily. Conditional expressions are introduced as abbreviations. The study of equivalent transformations of programs with nested expressions shows that any such program is equivalent to a set of disjunctive rules, possibly with negation as failure in the heads. The generalized answer set semantics is related to the Lloyd–Topor generalization of Clark’s completion and to the logic of minimal belief and negation as failure. This revised version was published online in June 2006 with corrections to the Cover Date.     

Weight constraint programs with evaluable functions

In the current practice of Answer Set Programming (ASP), evaluable functions are represented as special kinds of relations. This often makes the resulting program unnecessarily large when instantiated over a large domain. The extra constraints needed to enforce the relation as a function also make the logic program less transparent. In this paper, we consider adding evaluable functions to answer set logic programs. The class of logic programs that we consider here is that of weight constraint programs, which are widely used in ASP. We propose an answer set semantics to these extended weight constraint programs and define loop completion to characterize the semantics. Computationally, we provide a translation from loop completions of these programs to instances of the Constraint Satisfaction Problem (CSP) and use the off-the-shelf CSP solvers to compute the answer sets of these programs. A main advantage of this approach is that global constraints implemented in such CSP solvers become available to ASP. The approach also provides a new encoding for CSP problems in the style of weight constraint programs. We have implemented a prototype system based on these results, and our experiments show that this prototype system competes well with the state-of-the-art ASP solvers. In addition, we illustrate the utilities of global constraints in the ASP context.     

Complexity of computing with extended propositional logic programs

In this paper we introduce the notion of anF-program, whereF is a collection of formulas. We then study the complexity of computing withF-programs.F-programs can be regarded as a generalization of standard logic programs. Clauses (or rules) ofF-programs are built of formulas fromF. In particular, formulas other than atoms are allowed as building blocks ofF-program rules. Typical examples ofF are the set of all atoms (in which case the class of ordinary logic programs is obtained), the set of all literals (in this case, we get the class of logic programs with classical negation [9]), the set of all Horn clauses, the set of all clauses, the set of all clauses with at most two literals, the set of all clauses with at least three literals, etc. The notions of minimal and stable models [16, 1, 7] of a logic program have natural generalizations to the case ofF-programs. The resulting notions are called in this paperminimal andstable answer sets. We study the complexity of reasoning involving these notions. In particular, we establish the complexity of determining the existence of a stable answer set, and the complexity of determining the membership of a formula in some (or all) stable answer sets. We study the complexity of the existence of minimal answer sets, and that of determining the membership of a formula in all minimal answer sets. We also list several open problems.This work was partially supported by National Science Foundation under grant IRI-9012902.This work was partially supported by National Science Foundation under grant CCR-9110721.     

Semantic forgetting in answer set programming

The notion of forgetting, also known as variable elimination, has been investigated extensively in the context of classical logic, but less so in (nonmonotonic) logic programming and nonmonotonic reasoning. The few approaches that exist are based on syntactic modifications of a program at hand. In this paper, we establish a declarative theory of forgetting for disjunctive logic programs under answer set semantics that is fully based on semantic grounds. The suitability of this theory is justified by a number of desirable properties. In particular, one of our results shows that our notion of forgetting can be entirely captured by classical forgetting. We present several algorithms for computing a representation of the result of forgetting, and provide a characterization of the computational complexity of reasoning from a logic program under forgetting. As applications of our approach, we present a fairly general framework for resolving conflicts in inconsistent knowledge bases that are represented by disjunctive logic programs, and we show how the semantics of inheritance logic programs and update logic programs from the literature can be characterized through forgetting. The basic idea of the conflict resolution framework is to weaken the preferences of each agent by forgetting certain knowledge that causes inconsistency. In particular, we show how to use the notion of forgetting to provide an elegant solution for preference elicitation in disjunctive logic programming.     

Logical considerations on default semantics

We consider a reinterpretation of the rules of default logic. We make Reiter’s default rules into a constructive method of building models, not theories. To allow reasoning in first‐order systems, we equip standard first‐order logic with a (new) Kleene 3‐valued partial model semantics. Then, using our methodology, we add defaults to this semantic system. The result is that our logic is an ordinary monotonic one, but its semantics is now nonmonotonic. Reiter’s extensions now appear in the semantics, not in the syntax. As an application, we show that this semantics gives a partial solution to the conceptual problems with open defaults pointed out by Lifschitz [V. Lifschitz, On open defaults, in: Proceedings of the Symposium on Computational Logics (1990)], and Baader and Hollunder [F. Baader and B. Hollunder, Embedding defaults into terminological knowledge representation formalisms, in: Proceedings of Third Annual Conference on Knowledge Representation (Morgan‐Kaufmann, 1992)]. The solution is not complete, chiefly because in making the defaults model‐theoretic, we can only add conjunctive information to our models. This is in contrast to default theories, where extensions can contain disjunctive formulas, and therefore disjunctive information. Our proposal to treat the problem of open defaults uses a semantic notion of nonmonotonic entailment for our logic, related to the idea of “only knowing”. Our notion is “only having information” given by a formula. We discuss the differences between this and “minimal‐knowledge” ideas. Finally, we consider the Kraus–Lehmann–Magidor [S. Kraus, D. Lehmann and M. Magidor, Nonmonotonic reasoning, preferential models, and cumulative logics, Artificial Intelligence 44 (1990) 167–207] axioms for preferential consequence relations. We find that our consequence relation satisfies the most basic of the laws, and the Or law, but it does not satisfy the law of Cut, nor the law of Cautious Monotony. We give intuitive examples using our system, on the other hand, which on the surface seem to violate these two laws. We make some comparisons, using our examples, to probabilistic interpretations for which these laws are true, and we compare our models to the cumulative models of Kraus, Lehmann, and Magidor. We also show sufficient conditions for the laws to hold. These involve limiting the use of disjunction in our formulas in one way or another. We show how to make use of the theory of complete partially ordered sets, or domain theory. We can augment any Scott domain with a default set. We state a version of Reiter’s extension operator on arbitrary domains as well. This version makes clear the basic order‐theoretic nature of Reiter’s definitions. A three‐variable function is involved. Finding extensions corresponds to taking fixed points twice, with respect to two of these variables. In the special case of precondition‐free defaults, a general relation on Scott domains induced from the set of defaults is shown to characterize extensions. We show how a general notion of domain theory, the logic induced from the Scott topology on a domain, guides us to a correct notion of “affirmable sentence” in a specific case such as our first‐order systems. We also prove our consequence laws in such a way that they hold not only in first‐order systems, but in any logic derived from the Scott topology on an arbitrary domain. This revised version was published online in June 2006 with corrections to the Cover Date.     

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 generalization of the Lin-Zhao theorem

The theorem on loop formulas due to Fangzhen Lin and Yuting Zhao shows how to turn a logic program into a propositional formula that describes the program’s stable models. In this paper we simplify and generalize the statement of this theorem. The simplification is achieved by modifying the definition of a loop in such a way that a program is turned into the corresponding propositional formula by adding loop formulas directly to the conjunction of its rules, without the intermediate step of forming the program’s completion. The generalization makes the idea of a loop formula applicable to stable models in the sense of a very general definition that covers disjunctive programs, programs with nested expressions, and more.     

Logic programs with exceptions

We extend logic programming to deal with default reasoning by allowing the explicit representation of exceptions in addition to general rules. To formalise this extension, we modify the answer set semantics of Gelfond and Lifschitz, which allows both classical negation and negation as failure. We also propose a transformation which eliminates exceptions by using negation by failure. The transformed program can be implemented by standard logic programming methods, such as SLDNF. The explicit representation of rules and exceptions has the virtue of greater naturalness of expression. The transformed program, however, is easier to implement.     

Semantics and complexity of recursive aggregates in answer set programming

The addition of aggregates has been one of the most relevant enhancements to the language of answer set programming (ASP). They strengthen the modelling power of ASP in terms of natural and concise problem representations. Previous semantic definitions typically agree in the case of non-recursive aggregates, but the picture is less clear for aggregates involved in recursion. Some proposals explicitly avoid recursive aggregates, most others differ, and many of them do not satisfy desirable criteria, such as minimality or coincidence with answer sets in the aggregate-free case.In this paper we define a semantics for programs with arbitrary aggregates (including monotone, antimonotone, and nonmonotone aggregates) in the full ASP language allowing also for disjunction in the head (disjunctive logic programming — DLP). This semantics is a genuine generalization of the answer set semantics for DLP, it is defined by a natural variant of the Gelfond–Lifschitz transformation, and treats aggregate and non-aggregate literals in a uniform way. This novel transformation is interesting per se also in the aggregate-free case, since it is simpler than the original transformation and does not need to differentiate between positive and negative literals. We prove that our semantics guarantees the minimality (and therefore the incomparability) of answer sets, and we demonstrate that it coincides with the standard answer set semantics on aggregate-free programs.Moreover, we carry out an in-depth study of the computational complexity of the language. The analysis pays particular attention to the impact of syntactical restrictions on programs in the form of limited use of aggregates, disjunction, and negation. While the addition of aggregates does not affect the complexity of the full DLP language, it turns out that their presence does increase the complexity of normal (i.e., non-disjunctive) ASP programs up to the second level of the polynomial hierarchy. However, we show that there are large classes of aggregates the addition of which does not cause any complexity gap even for normal programs, including the fragment allowing for arbitrary monotone, arbitrary antimonotone, and stratified (i.e., non-recursive) nonmonotone aggregates. The analysis provides some useful indications on the possibility to implement aggregates in existing reasoning engines.     

Strong equivalence of logic programs under the infinite-valued semantics

We consider the notion of strong equivalence [V. Lifschitz, D. Pearce, A. Valverde, Strongly equivalent logic programs, ACM Transactions on Computational Logic 2 (4) (2001) 526-541] of normal propositional logic programs under the infinite-valued semantics [P. Rondogiannis, W.W. Wadge, Minimum model semantics for logic programs with negation-as-failure, ACM Transactions on Computational Logic 6 (2) (2005) 441-467] (which is a purely model-theoretic semantics that is compatible with the well-founded one). We demonstrate that two such programs are strongly equivalent under the infinite-valued semantics if and only if they are logically equivalent in the corresponding infinite-valued logic. In particular, we show that strong equivalence of normal propositional logic programs is decidable, and more specifically coNP-complete. Our results have a direct implication for the well-founded semantics since, as we demonstrate, if two programs are strongly equivalent under the infinite-valued semantics, then they are also strongly equivalent under the well-founded semantics.     

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.     

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.     

概率逻辑程序

1 引言最近几十年来,不确定性的管理在知识描述和推理中扮演着越来越重要的角色。为了处理不确定知识,人们提出了各种不同的形式化和方法论,其中大部分是直接或间接地基于概率论的。     

What is failure? An approach to constructive negation

A standard approach to negation in logic programming is negation as failure. Its major drawback is that it cannot produce answer substitutions to negated queries. Approaches to overcoming this limitation are termed constructive negation. This work proposes an approach based on construction offailed trees for some instances of a negated query. For this purpose a generalization of the standard notion of a failed tree is needed. We show that a straightforward generalization leads to unsoundness and present a correct one.The method is applicable to arbitrary normal programs. If finitely failed trees are concerned then its semantics is given by Clark completion in 3-valued logic (and our approach is a proper extension of SLDNF-resolution). If infinite failed trees are allowed then we obtain a method for the well-founded semantics. In both cases soundness and completeness are proved.     

On the Computation of the Disjunctive Well-Founded Semantics

A characterization of the disjunctive well-founded semantics (DWFS) is given in terms of the Gelfond–Lifschitz transformation. This characterization is used to develop a top-down method of testing DWFS membership, employing a hyperresolution-like operator and quasi-cyclic trees to handle minimal model processing. A flexible bottom-up method of computing the DWFS is also given that admits the use of a powerful reduction operator. For finite propositional databases, all of our methods run in polynomial space.     

On finite-state approximants for probabilistic computation tree logic

We generalize the familiar semantics for probabilistic computation tree logic from finite-state to infinite-state labelled Markov chains such that formulas are interpreted as measurable sets. Then we show how to synthesize finite-state abstractions which are sound for full probabilistic computation tree logic and in which measures are approximated by monotone set functions. This synthesis of sound finite-state approximants also applies to finite-state systems and is a probabilistic analogue of predicate abstraction. Sufficient and always realizable conditions are identified for obtaining optimal such abstractions for probabilistic propositional modal logic.     

Extending Answer Sets for Logic Programming Agents

We present systems of logic programming agents (LPAS) to model the interactions between decision-makers while evolving to a conclusion. Such a system consists of a number of agents connected by means of unidirectional communication channels. Agents communicate with each other by passing answer sets obtained by updating the information received from connected agents with their own private information. We introduce a credulous answer set semantics for logic programming agents. As an application, we show how extensive games with perfect information can be conveniently represented as logic programming agent systems, where each agent embodies the reasoning of a game player, such that the equilibria of the game correspond with the semantics agreed upon by the agents in the LPAS.     

行为时序逻辑与自反线性时序逻辑的关系

为了能够将哲学逻辑中的公理系统运用到行为时序逻辑的研究中。对行为时序逻辑公式的语义进行形式化定义．从语义和语法两方面研究行为时序逻辑公理系统和具有自反性质的线性时序逻辑公理系统之间的联系．提出并证明行为时序逻辑公式转换为自反线性时序逻辑公式的定理。按照集合论和模型论的思想,定义行为时序逻辑中项和行为时序逻辑原子公式的概念。定义Lesilie Lamport所提出的行为时序逻辑公式的语义。证明自反线性时序逻辑公理系统适用于行为时序逻辑公理系统．以此为基础证明行为时序逻辑的简单规则、基本规则和附加规则。