We present DLV-Complex, an extension of the DLV system that features the support for a powerful (possibly recursive) use of functions, list and set terms in the full ASP language with disjunction and negation. Any com...
详细信息
ISBN:
(纸本)9783642042379
We present DLV-Complex, an extension of the DLV system that features the support for a powerful (possibly recursive) use of functions, list and set terms in the full ASP language with disjunction and negation. Any computable function can be encoded in a rich and fully declarative KRR language, ensuring termination on all programs belonging to the recently introduced class of finitely-ground programs furthermore, termination can be "a priori" guaranteed on demand by means of a syntactic restriction check that ensures a finite-domain property. the system, which is already successfully used in many universities and reinstitutes, comes also equipped with a rich library of built-in functions and predicates for the manipulation of complex terms.
FLORA-2 is an advanced knowledge representation system that integrates F-logic, HiLog, and Transaction logic. In this paper we give an overview of the theoretical foundations of the system and of some of the aspects o...
详细信息
ISBN:
(纸本)3540285385
FLORA-2 is an advanced knowledge representation system that integrates F-logic, HiLog, and Transaction logic. In this paper we give an overview of the theoretical foundations of the system and of some of the aspects of nonmonotonicreasoning in FLORA-2. these include scoped default negation, behavioral inheritance, and nonmonotonicity that stems from database dynamics.
the logic FO(ID) uses ideas from the field of logicprogramming to extend first order logic with non-monotone inductive definitions. the goal of this paper is to extend Gentzen's sequeut calculus to obtain a deduc...
详细信息
ISBN:
(纸本)9783642042379
the logic FO(ID) uses ideas from the field of logicprogramming to extend first order logic with non-monotone inductive definitions. the goal of this paper is to extend Gentzen's sequeut calculus to obtain a deductive inference method for FO(ID). the main difficulty in building Such a proof system is the representation and inference of unfounded sets. It turns out that we can represent unfounded sets by least fixpoint expressions borrowed from stratified least fixpoint logic (SLFP), which is a logic with a least fixpoint operator and characterizes the expressibility of stratified logic programs. therefore, in this paper, we integrate least fixpoint expressions into FO(ID) and define the logic FO(ID,SLFP). We investigate a sequeut calculus for FO(ID,SLFP), which extends the sequent calculus for SLFP with inference rules for the inductive definitions of FO(ID). We show that this proof system is sound with respect to a slightly restricted fragment of FO(ID) and complete for a more restricted fragment of FO(ID).
Disjunctive logicprogramming (DLP) with stable model semantics is a powerful nonmonotonic formalism for knowledge representation and reasoning. reasoning with DLP is harder than with normal (boolean OR-free) logic pr...
详细信息
Disjunctive logicprogramming (DLP) with stable model semantics is a powerful nonmonotonic formalism for knowledge representation and reasoning. reasoning with DLP is harder than with normal (boolean OR-free) logic programs, because stable model checking-deciding whether a given model is a stable model of a propositional DLP program-is co-NP-complete, while it is polynomial for normal logic programs. this paper proposes a new transformation Gamma(M) (P), which reduces stable model checking to UNSAT-i.e., to deciding whether a given CNF formula is unsatisfiable. the stability of a model M of a program P thus can be verified by calling a Satisfiability Checker on the CNF formula Gamma(M) (P). the transformation is parsimonious (i.e., no new symbol is added), and efficiently computable, as it runs in logarithmic space (and therefore in polynomial time). Moreover, the size of the generated CNF formula never exceeds the size of the input (and is usually much smaller). We complement this transformation with modular evaluation results, which allow for efficient handling of large real-world reasoning problems. the proposed approach to stable model checking has been implemented in DLV-a state-of-the-art implementation of DLP. A number of experiments and benchmarks have been run using SATZ as Satisfiability checker. the results of the experiments are very positive and confirm the usefulness of our techniques. (C) 2003 Elsevier B.V. All rights reserved.
Propositional satisfiability (SAT) solvers provide a promising computational platform for logic programs under the stable model semantics. However. computing stable models of a logic program using a SAT solver presume...
详细信息
ISBN:
(纸本)9783642042379
Propositional satisfiability (SAT) solvers provide a promising computational platform for logic programs under the stable model semantics. However. computing stable models of a logic program using a SAT solver presumes translating the program into a set of clauses which is the input form accepted by most SAT solvers. this leads to fairly complex super-linear translations. there are, however, interesting extensions to plain clausal propositional representations Such as difference logic. A number of solvers have been developed for difference logic, in particular in the context of the satisfiability modulo theories (SMT) framework. and the goal of the paper is to study whether Such engines could be harnessed to the computation of stable models for logic programs in an effective way. To this end, we provide succinct translations front logic programs to theories of difference logic and evaluate the potential of SMT solvers in the computation of stable models using, these translations and a selection of benchmarks.
We present an extension epsilon L+perpendicular to T of the description logic epsilon L+perpendicular to for reasoning about prototypical properties and inheritance with exceptions. epsilon L+perpendicular to T is obt...
详细信息
ISBN:
(纸本)9783642042379
We present an extension epsilon L+perpendicular to T of the description logic epsilon L+perpendicular to for reasoning about prototypical properties and inheritance with exceptions. epsilon L+perpendicular to T is obtained by adding to epsilon L+perpendicular to a typicality operator T, which is intended to select the "typical" instances of a concept. In epsilon L+perpendicular to T knowledge bases may contain inclusions of the form "T(C) is subsumed by P", expressing that typical C-members have the property P. We show that the problem of entailment in epsilon L+perpendicular to T is in CO-NP.
We consider the problem of whether a given preferred answer set program can be reduced to a propositional formula. Research on this topic is of boththeoretical and practical interests: on one hand, it will shed new i...
详细信息
ISBN:
(纸本)9783642042379
We consider the problem of whether a given preferred answer set program can be reduced to a propositional formula. Research on this topic is of boththeoretical and practical interests: on one hand, it will shed new insights to understand the expressive power of preferred answer set programs on the other hand, it may also lead to efficient implementations for computing preferred answer sets of logic programs. In this paper, we focus on Brewka and Eiter's preferred answer set programs. We propose a translation from preferred answer set programs to propositional logic and show that there is one-to-one correspondence between the preferred answer sets of the program to the models of the resulting propositional theory. We then link this result to Brewka and Eiter's weakly preferred answer set semantics.
this paper gives a summary of the First Answer Set programming System Competition that was held in conjunction withthe Ninthinternationalconference on logicprogramming and nonmonotonicreasoning. the aims of the c...
详细信息
ISBN:
(纸本)9783540721994
this paper gives a summary of the First Answer Set programming System Competition that was held in conjunction withthe Ninthinternationalconference on logicprogramming and nonmonotonicreasoning. the aims of the competition were twofold: first, to collect challenging benchmark problems, and second, to provide a platform to assess a broad variety of Answer Set programming systems. the competition was inspired by similar events in neighboring fields, where regular benchmarking has been a major factor behind improvements in the developed systems and their ability to address practical applications.
Despite the obvious relevance of plausible reasoning to real-world problem solving, nonmonotoniclogics are rarely used in commercial applications or large- scale commonsense reasoning systems. this is largely because...
ISBN:
(纸本)3540667490
Despite the obvious relevance of plausible reasoning to real-world problem solving, nonmonotoniclogics are rarely used in commercial applications or large- scale commonsense reasoning systems. this is largely because few efficient algorithms and tools have thus far been developed.
暂无评论