We present a new approach to reasoning with default logicthat aims at Reiter's original approach, whenever there is no source for incoherence. We accomplish this by shifting the emphasis from the application of i...
详细信息
ISBN:
(纸本)3540667490
We present a new approach to reasoning with default logicthat aims at Reiter's original approach, whenever there is no source for incoherence. We accomplish this by shifting the emphasis from the application of individual default rules to that of the joint application of a default rule together with rules supporting this application. this allows for reasoning in an incremental yet compositional fashion, without giving up the expressiveness needed for knowledge representation. Technically, our approach differs from others in that it guarantees the existence of extensions without requiring semi-monotonicity.
the coupling of description logicreasoning systems with other reasoning formalisms (possibly over the Web) is becoming an important research issue and calls for advanced methods and algorithms. Recently, several noti...
详细信息
ISBN:
(纸本)3540252363
the coupling of description logicreasoning systems with other reasoning formalisms (possibly over the Web) is becoming an important research issue and calls for advanced methods and algorithms. Recently, several notions of description logic programs have been introduced, combining rule-based semantics with description logics. Among them are nonmonotonic description logic programs (or dl-programs for short) which combine nonmonotoniclogic programs with description logics under a generalized version of the answer-set and the well-founded semantics, respectively, which are the predominant semantics for nonmonotoniclogic programs. In this paper, we consider some technical issues regarding an efficient implementation for both semantics, which has been realized in a working prototype exploiting the two state-of-art tools DLV and RACER. A major issue in this respect is efficient interfacing between the two reasoning systems at hand, for which we devised special methods. Such methods may fruitfully be used for the implementation of systems of similar nature. Reported experimentation activities with our prototype show that the methods we have developed are effective and are a key for highly optimized nonmonotonic dl-program engines.
LPEQ and DLPEQ, two translators for automated equivalence testing of logic programs are discussed. the translators LPEQ and DLPEQ have been implemented in the C programming language under the Linux operating system. B...
详细信息
ISBN:
(纸本)354020721X
LPEQ and DLPEQ, two translators for automated equivalence testing of logic programs are discussed. the translators LPEQ and DLPEQ have been implemented in the C programming language under the Linux operating system. Both translators take two logic programs and command line options as their input and produce a translation for equivalence testing as their output. the input files are assumed to be in an internal format, as produced by the front-end LPARSE of the SMODELS system.
We extend the language of here-and-there logic by two kinds of atomic programs allowing to minimally update the truth value of a propositional variable here or there, if possible. these atomic programs are combined by...
详细信息
ISBN:
(纸本)9783642405648
We extend the language of here-and-there logic by two kinds of atomic programs allowing to minimally update the truth value of a propositional variable here or there, if possible. these atomic programs are combined by the usual dynamic logic program connectives. We investigate the mathematical properties of the resulting extension of equilibrium logic: we prove that the problem of logical consequence in equilibrium models is EXPTIME complete by relating equilibrium logic to dynamic logic of propositional assignments.
reasoning on Constraint Handling Rules (CHR) programs and their executional behaviour is often ad-hoc and outside of a formal system. this is a pity, because CHR subsumes a wide range of important automated reasoning ...
详细信息
ISBN:
(纸本)9783540721994
reasoning on Constraint Handling Rules (CHR) programs and their executional behaviour is often ad-hoc and outside of a formal system. this is a pity, because CHR subsumes a wide range of important automated reasoning services. Mapping CHR to Transaction logic (TR) combines CHR rule specification, CHR rule application, and reasoning on CHR programs and CHR derivations inside one formal system which is executable. this new TR semantics obviates the need for disjoint declarative and operational semantics.
this paper applies the logic-based formalism of Answer Set programming (ASP) to the modelling of competition, inhibition and cycles in biochemical networks. In particular, it introduces a generic framework that unifie...
详细信息
ISBN:
(纸本)9781479943258
this paper applies the logic-based formalism of Answer Set programming (ASP) to the modelling of competition, inhibition and cycles in biochemical networks. In particular, it introduces a generic framework that unifies the competitive and inhibitory mechanisms proposed in the literature along withtheir complementary approaches to reasoning about loops. We show how the nonmonotonic effects of competition and inhibition can be naturally encoded in the formalism of ASP and that the different ways of handling loops correspond to the computation of stable and supported models. We also show that inhibitory models are currently more general than competitive models and we argue that that both interpretations of loops are justified in some applications.
A recently proposed module system for answer set programming is generalized for the input language of the SMODELS system. To show that the stable model semantics is compositional and modular equivalence is a congruenc...
详细信息
ISBN:
(纸本)9783540721994
A recently proposed module system for answer set programming is generalized for the input language of the SMODELS system. To show that the stable model semantics is compositional and modular equivalence is a congruence for composition of SMODELS program modules, a general translation-based scheme for introducing syntactic extensions of the module system is presented. A characterization of the compositionality of the semantics is used as an alternative condition for module composition, which allows compositions of modules even in certain cases with positive recursion between the modules to be composed.
In this paper we introduce a logicprogramming based framework which allows the representation of conditional non-monotonic temporal beliefs and goals in a declarative way. We endow it with stable model like semantics...
详细信息
ISBN:
(纸本)9783642405648
In this paper we introduce a logicprogramming based framework which allows the representation of conditional non-monotonic temporal beliefs and goals in a declarative way. We endow it with stable model like semantics that allows us to deal with conflicting goals and generate possible alternatives. We show that our framework satisfies some usual properties on goals and that it allows imposing alternative constraints on the interaction between beliefs and goals. We prove the decidability of the usual reasoning tasks and show how they can be implemented using an ASP solver and an LTL reasoner in a modular way, thus taking advantage of existing LTL reasoners and ASP solvers.
Reiter's default logic formalizes nonmonotonicreasoning using default assumptions. the semantics of a given instance of default logic is based on a fixpoint equation defining an extension. three different reasoni...
详细信息
ISBN:
(纸本)9783540721994
Reiter's default logic formalizes nonmonotonicreasoning using default assumptions. the semantics of a given instance of default logic is based on a fixpoint equation defining an extension. three different reasoning problems arise in the context of default logic, namely the existence of an extension, the presence of a given formula in an extension, and the occurrence of a formula in all extensions. Since the end of 1980s, several complexity results have been published concerning these default reasoning problems for different syntactic classes of formulas. We derive in this paper a complete classification of default logicreasoning problems by means of universal algebra tools using Post's clone lattice. In particular we prove a trichotomy theorem for the existence of an extension, classifying this problem to be either polynomial, NP-complete, or Sigma P-2-complete, depending on the set of underlying Boolean connectives. We also prove similar trichotomy theorems for the two other algorithmic problems in connection with default logicreasoning.
It has been known for a long time that intuitionistically equivalent formulas have the same stable models. We extend this theorem to propositional formulas with infinitely long conjunctions and disjunctions and show h...
详细信息
ISBN:
(纸本)9783642405648
It has been known for a long time that intuitionistically equivalent formulas have the same stable models. We extend this theorem to propositional formulas with infinitely long conjunctions and disjunctions and show how to apply this generalization to proving properties of aggregates in answer set programming.
暂无评论