In this work we describe a system for determining strong equivalence of disjunctive non-ground datalog programs under the stable model semantics. the problem is tackled by reducing it to the unsatisfiability problem o...
详细信息
ISBN:
(纸本)3540285385
In this work we describe a system for determining strong equivalence of disjunctive non-ground datalog programs under the stable model semantics. the problem is tackled by reducing it to the unsatisfiability problem of first-order formulas in the Bernays-Schonfinkel fragment. We then employ a tableaux-based theorem prover, which (unlike most other currently available provers) is guaranteed to terminate for these formulas. To the best of our knowledge, this is the first strong equivalence tester for disjunctive non-ground datalog.
We investigate the problem of reasoning in nonmonotonic extensions of first-order logic. In particular, we study reasoning in first-order MKNF, the modal logic of minimal knowledge and negation as failure introduced b...
详细信息
ISBN:
(纸本)3540667490
We investigate the problem of reasoning in nonmonotonic extensions of first-order logic. In particular, we study reasoning in first-order MKNF, the modal logic of minimal knowledge and negation as failure introduced by Lifschitz. MKNF can be considered as a unifying framework for several nonmonotonic formalisms, including default logic, autoepistemic logic, circumscription, and logicprogramming. By suitably extending deduction methods for propositional nonmonotoniclogics, we define techniques for reasoning in significant subsets of first-order MKNF, which allow for characterizing decidable fragments of first-order nonmonotonic modal logics. Due to the expressive abilities of MKNF, such techniques can be seen as general reasoning methods for several nonmonotonic formalisms based on first-order logic. We also analyze the relationship between such decidable fragments of MKNF and disjunctive Datalog.
We introduce a declarative approach for a coherent composition of autonomous databases. For this we use ID-logic, a formalism that extends classical logic with inductive definitions. We consider ID-logictheories that...
详细信息
ISBN:
(纸本)3540285385
We introduce a declarative approach for a coherent composition of autonomous databases. For this we use ID-logic, a formalism that extends classical logic with inductive definitions. We consider ID-logictheories that express, at the same time, the two basic challenges in database composition problems: relating different schemas of the local databases to one global schema (schema integration) and amalgamating the distributed and possibly contradictory data to one consistent database (data integration). We show that our framework supports different methods for schema integration (as well as their combinations) and that it provides a straightforward way of dealing with inconsistent data. Moreover, this framework facilitates the implementation of database repair and consistent query answering by means of a variety of reasoning systems.
In answer set programming systems like Smodels and some SAT solvers, constraint propagation is carried out by a mechanism called lookahead. the question arises as what is the pruning power of lookahead, and how such p...
详细信息
ISBN:
(纸本)3540285385
In answer set programming systems like Smodels and some SAT solvers, constraint propagation is carried out by a mechanism called lookahead. the question arises as what is the pruning power of lookahead, and how such pruning power fares in comparison withthe consistency techniques in solving CSPs. In this paper, we study the pruning power of lookahead by relating it to local consistencies under two different encodings from CSPs to answer set programs. this leads to an understanding of how the search space is pruned in an answer set solver with lookahead for solving CSPs. On the other hand, lookahead as a general constraint propagation mechanism provides a uniform algorithm for enforcing a variety of local consistencies. We also study the impact on the search efficiency under these encodings.
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.
the paper introduces Answer Set programming with External Predicates (ASP-EX), a framework aimed at enabling ASP to deal with external sources of computation. this feature is realized by the introduction of "para...
详细信息
ISBN:
(纸本)3540285385
the paper introduces Answer Set programming with External Predicates (ASP-EX), a framework aimed at enabling ASP to deal with external sources of computation. this feature is realized by the introduction of "parametric" external predicates, whose extension is not specified by means of a logic program but computed through external code. With respect to existing approaches it is explicitly addressed the issue of invention of new information coming from external predicates, in form of new, and possibly infinite, constant symbols. Several decidable restrictions of the language are identified as well as suitable algorithms for evaluating Answer Set Programs with external predicates. the framework paves the way to Answer Set programming in several directions such as pattern manipulation applications, as well as the possibility to exploit function symbols. ASP-EX has been successfully implemented in the DLV system, which is now enabled to make external program calls.
Possibilistic Defeasible logicprogramming (P-DeLP) is a logicprogramming language which combines features from argumentation theory and logicprogramming, incorporating as well the treatment of possibilistic uncerta...
详细信息
ISBN:
(纸本)3540285385
Possibilistic Defeasible logicprogramming (P-DeLP) is a logicprogramming language which combines features from argumentation theory and logicprogramming, incorporating as well the treatment of possibilistic uncertainty and fuzzy knowledge at object-language level. Solving a P-DeLP query Q accounts for performing an exhaustive analysis of arguments and defeaters for Q, resulting in a so-called dialectical tree, usually computed in a depth-first fashion. Computing dialectical trees efficiently in P-DeLP is an important issue, as some dialectical trees may be computationally more expensive than others which lead to equivalent results. In this paper we explore different aspects concerning how to speed up dialectical inference in P-DeLP. We introduce definitions which allow to characterize dialectical trees constructively rather than declaratively, identifying relevant features for pruning the associated search space. the resulting approach can be easily generalized to be applied in other argumentation frameworks based in logicprogramming.
this paper introduces a novel monotonic modal logic, able to characterise reflexive autoepistemic reasoning of the nonmonotonic variant of modal logic SW5: we add a second new modal operator into the original language...
详细信息
ISBN:
(纸本)9783319616605;9783319616599
this paper introduces a novel monotonic modal logic, able to characterise reflexive autoepistemic reasoning of the nonmonotonic variant of modal logic SW5: we add a second new modal operator into the original language of SW5, and show that the resulting formalism called MRAE* is strong enough to capture the minimal model notion underlying some major forms of nonmonotoniclogic among which are autoepistemic logic, default logic, and nonmonotoniclogicprogramming. the paper ends with a discussion of a general strategy, naturally embedding several nonmonotoniclogics of similar kinds.
We argue in favour of teaching modern programming to students of "non-scientific" undergraduate disciplines (humanities), considering that computer-assisted learning should not be reduced to the usage of too...
详细信息
ISBN:
(纸本)9789897581793
We argue in favour of teaching modern programming to students of "non-scientific" undergraduate disciplines (humanities), considering that computer-assisted learning should not be reduced to the usage of tools, but provides some answers to the question: how the knowledge is built. the computer science should be treated as an inherent part of their culture. We advocate the teaching of logicprogramming languages: Prolog, and of the Constraint programming languages, such as CHR. logicprogramming permits to formulate the computational problems and their solutions in a form more close to human reasoningthan several other languages, and adaptable to the domains of interest of the learners.
We prove two properties of logic programs under the answer set semantics that may be useful in connection with applications of logicprogramming to representing causality and to planning. One theorem is about the use ...
详细信息
ISBN:
(纸本)3540667490
We prove two properties of logic programs under the answer set semantics that may be useful in connection with applications of logicprogramming to representing causality and to planning. One theorem is about the use of disjunctive rules to express that an atom is exogenous. the other provides an alternative way of expressing that a plan does not include concurrently executed actions.
暂无评论