Strong equivalence is an important property for nonmonotonic formalisms, allowing safe local changes to a nonmonotonic theory. this paper considers strong equivalence for nonmonotonic causal theories of the kind intro...
详细信息
ISBN:
(纸本)354020721X
Strong equivalence is an important property for nonmonotonic formalisms, allowing safe local changes to a nonmonotonic theory. this paper considers strong equivalence for nonmonotonic causal theories of the kind introduced by McCain and Turner. Causal theories T-1 and T-2 are strongly equivalent if, for every causal theory T, T-1 boolean OR T and T-2 boolean OR T are equivalent (that is, have the same causal models). the paper introduces a convenient characterization of this property in terms of so-called SE-models, much as was done previously for answer set programs and default theories. A similar result is provided for the nonmonotonic modal logic UCL. the paper also introduces a reduction from the problem of deciding strong equivalence of two causal theories to the problem of deciding equivalence of two sets of propositional formulas.
the language of nonmonotonic causal theories, defined by Norman McCain and Hudson Turner, is an important formalism for representing properties of actions. For causal theories of a special kind, called definite, a sim...
详细信息
ISBN:
(纸本)354020721X
the language of nonmonotonic causal theories, defined by Norman McCain and Hudson Turner, is an important formalism for representing properties of actions. For causal theories of a special kind, called definite, a simple translation into the language of logic programs under the answer set semantics is available. In this paper we define a similar translation for causal theories of a more general form, called almost definite. Such theories can be used, for instance, to characterize the transitive closure of a binary relation. the new translation leads to an implementation of a subclass of almost definite causal theories that employs the answer set solver SMODELS as the search engine.
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.
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.
this paper studies computational issues related to the problem of reasoning about actions and change (RAC) by exploiting its link withthe Answer Set programming paradigm. It investigates how increasing the expressive...
详细信息
ISBN:
(纸本)9783540207214
this paper studies computational issues related to the problem of reasoning about actions and change (RAC) by exploiting its link withthe Answer Set programming paradigm. It investigates how increasing the expressiveness of a RAC formalism so that it can capture the three major problems of frame, ramification and qualification, affects its computational complexity, and how a solution to these problems can be implemented within Answer Set programming. Our study is carried out within the particular language Ε. It establishes a link between language Ε and Answer Set programming by presenting encodings of different versions of this language into logic programs under the answer set semantics. this provides a computational realization of solutions to problems related to reasoning about actions and change, that can make use of the recent development of effective systems for Answer Set programming.
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.
暂无评论