For a given semantics, two logic programs Pi(1) and Pi(2) can be said to be equivalent if they have the same intended models and strongly equivalent if for any program X, Pi(1) boolean OR X and Pi(2) boolean OR X are ...
详细信息
ISBN:
(纸本)354020721X
For a given semantics, two logic programs Pi(1) and Pi(2) can be said to be equivalent if they have the same intended models and strongly equivalent if for any program X, Pi(1) boolean OR X and Pi(2) boolean OR X are equivalent. Eiter and Fink have recently studied and characterised under answer set semantics a further, related property of uniform equivalence, where the extension X is required to be a set of atoms. We extend their main results to propositional theories in equilibrium logic and describe a tableaux proof system for checking the property of uniform equivalence. We also show that no new forms of equivalence are obtained by varying the logical form of expressions in the extension X. Finally, some examples are studied including special cases of nested and generalized rules.
We investigate rule dependency graphs and their colorings for characterizing the computation of answer sets of logic programs. We start from a characterization of answer sets in terms of totally colored dependency gra...
详细信息
ISBN:
(纸本)354020721X
We investigate rule dependency graphs and their colorings for characterizing the computation of answer sets of logic programs. We start from a characterization of answer sets in terms of totally colored dependency graphs. To a turn, we develop a series of operational characterizations of answer sets in terms of operators on partial colorings. In analogy to the notion of a derivation in proof theory, our operational characterizations are expressed as (non-deterministically formed) sequences of colorings, turning an uncolored graph into a totally colored one. this results in an operational framework in which different combinations of operators result in different formal properties. Among others, we identify the basic strategy employed by the noMoRe system and justify its algorithmic approach. Also, we distinguish Fitting's and well-founded semantics.
An extension of DLV by aggregates to simplify the encoding of the frequently occuring concepts is discussed. DLV is an efficient Answer Set programming (ASP) system which can implement the answer set semantics with va...
详细信息
ISBN:
(纸本)354020721X
An extension of DLV by aggregates to simplify the encoding of the frequently occuring concepts is discussed. DLV is an efficient Answer Set programming (ASP) system which can implement the answer set semantics with various language extensions. the semantics of programs without aggregates is provided in BLR00 as an extension of the classical answer set semantics given in GL91. the strong point of DLV is its robust and efficient implementation, which integrates algorithms and heuristics from the field of nonmonotic reasoning.
Ontologies have become an important methodology for representing knowledge, particularly for allowing agents to interchange knowledge over the world-wide-web. From an abstract point of view, an ontology can be seen as...
详细信息
ISBN:
(纸本)354020721X
Ontologies have become an important methodology for representing knowledge, particularly for allowing agents to interchange knowledge over the world-wide-web. From an abstract point of view, an ontology can be seen as a theory about a set of classes. the language underlying the ontology may or may not be decidable;if it is, it is often called a description logic, and the problem of determining whether one description logic formula implies (or subsumes) another is fundamental to deduction in ontologies. this paper models description logics as first-order theories, and employs model-theoretic techniques to determine properties of various description logics. these properties are used to design efficient engines to generate Answer Set Programs that perform deduction in ontologies. this approach contrasts to tableaux theorem proving techniques that are more commonly used. the resulting system serves as an experimental platform to explore the combination of logic-programming based techniques for non-monotonic reasoning and constraint handling with description-logic based deduction. Specifically, we use ASP to create a small but powerful theorem prover for the description logic ALCQI. While ALCQI is P-space complete, our deduction engine requires exponential space in the worst case. However experiments show that its time is roughly comparable to the one of the best tableaux-based engined, DLP [1], even though DLP is written for a simpler description logic, ALCN(1).
Well-known principles of induction include monotone induction and different sorts of non-monotone induction such as inflationary induction, induction over well-ordered sets and iterated induction. In this work, we def...
详细信息
ISBN:
(纸本)354020721X
Well-known principles of induction include monotone induction and different sorts of non-monotone induction such as inflationary induction, induction over well-ordered sets and iterated induction. In this work, we define a logic formalizing induction over well-ordered sets and monotone and iterated induction. Just as the principle of positive induction has been formalized in FO(LFP), and the principle of inflationary induction has been formalized in FO(IFP), this paper formalizes the principle of iterated induction in a new logic for Non-Monotone Inductive Definitions (NMID-logic). the semantics of the logic is strongly influenced by the well-founded semantics of logicprogramming. Our main result concerns the modularity properties of inductive definitions in NMID-logic. Specifically, we formulate conditions under which a simultaneous definition Delta of several relations is logically equivalent to a conjunction of smaller definitions Delta(1) boolean AND . . . boolean AND Delta(n) with disjoint sets of defined predicates. the difficulty of the result comes from the fact that predicates P-i and P-j defined in Delta(i) and Delta(j), respectively, may be mutually connected by simultaneous induction. Since logicprogramming and abductive logicprogramming under well-founded semantics are proper fragments of our logic, our modularity results are applicable there as well. As an example of application of our logic and theorems presented in this paper, we describe a temporal formalism, the inductive situation calculus, where causal dependencies axe naturally represented as rules of inductive definitions.
Many NP-complete problems can be encoded in the answer set semantics of logic programs in a very concise way, where the encoding reflects the typical "guess and check" nature of NP problems: the property is ...
详细信息
ISBN:
(纸本)354020721X
Many NP-complete problems can be encoded in the answer set semantics of logic programs in a very concise way, where the encoding reflects the typical "guess and check" nature of NP problems: the property is encoded in a way such that polynomial size certificates for it correspond to stable models of a program. However, the problem-solving capacity of full disjunctive logic programs (DLPs) is beyond NP at the second level of the polynomial hierarchy. While problems there also have a "guess and check" structure, an encoding in a DLP is often non-obvious, in particular if the "check" itself is co-NP-complete;usually, such problems are solved by interleaving separate "guess" and "check" programs, where the check is expressed by inconsistency of the check program. We present general transformations of head-cycle free (extended) logic programs into stratified disjunctive logic programs which enable one to integrate such "guess" and "check" programs automatically into a single disjunctive logic program. Our results complement recent results on meta-interpretation in ASP, and extend methods and techniques for a declarative "guess and check" problem solving paradigm through ASP.
Disjunctive logicprogramming (DLP) under the answer set semantics is an advanced formalism for knowledge representation and reasoning. It is generally considered more expressive than normal (disjunction-free) logic P...
详细信息
ISBN:
(纸本)354020721X
Disjunctive logicprogramming (DLP) under the answer set semantics is an advanced formalism for knowledge representation and reasoning. It is generally considered more expressive than normal (disjunction-free) logicprogramming, whose expressiveness is limited to properties decidable in NP. However, this higher expressiveness comes at a computational cost, and while there are several efficient systems for the normal case, we are only aware of few solid implementations for full DLP. In this paper we investigate novel techniques to couple two main modules (a model generator and a model checker) commonly found in DLP systems more tightly. Instead of using the checker only as a boolean oracle, in our approach, upon a failed check it also returns a so-called unfounded set. Intuitively, this set explains why a model candidate is not an answer set, and the generator employs this knowledge to backtrack until that set is no longer unfounded, which is vastly more efficient than employing full-fledged model checks to control backtracking. Furthermore, we invoke the checker not only for actual model candidates, but also on partial models during model generation to possibly prune the search space. We implemented these approaches in DLV, a state-of-the-art implementation of DLP according to recent comparisons, and carried out experiments;tests on hard benchmark instances show a significant speedup of a factor of two and above.
We present a declarative language, PP, for the specification of preferences between possible solutions (or trajectories) of a planning problem. this novel language allows users to elegantly express non-trivial, multi-...
详细信息
An inference engine obtained by integrating smodels with a finite-domain solver capable of executing smodels program with aggregates was described. the engine was meant to be used in conjunction with front-ends capabl...
详细信息
ISBN:
(纸本)9783540207214
An inference engine obtained by integrating smodels with a finite-domain solver capable of executing smodels program with aggregates was described. the engine was meant to be used in conjunction with front-ends capable of performing high-level constraint handling of sets and aggregates. the use of a general constraint solver allows to easily understand and customize the way aggregates are handled. It also allows to easily extend the system to include new form of aggregates by simply adding new type of constraints.
We present a logicprogramming based conditional planner that is capable of generating both conditional plans and conformant plans in the presence of sensing actions and incomplete information. We prove the correctnes...
详细信息
暂无评论