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.
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.
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 propose a model to manage the distributed computation of answer sets within a general framework. this design incorporates a variety of software and hardware architectures and allows its easy use with a diverse cadr...
详细信息
ISBN:
(纸本)3540285385
We propose a model to manage the distributed computation of answer sets within a general framework. this design incorporates a variety of software and hardware architectures and allows its easy use with a diverse cadre of computational elements. Starting from a generic algorithmic scheme, we develop a platform for distributed answer set computation, describe its current state of implementation, and give some experimental results.
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.
Open answer set programming (OASP) is an extension of answer set programming where one may ground a program with an arbitrary superset of the program's constants. We define a fixed point logic (FPL) extension of C...
详细信息
ISBN:
(纸本)3540285385
Open answer set programming (OASP) is an extension of answer set programming where one may ground a program with an arbitrary superset of the program's constants. We define a fixed point logic (FPL) extension of Clark's completion such that open answer sets correspond to models of FPL formulas and identify a syntactic subclass of programs, called (loosely) guarded programs. Whereas reasoning with general programs in OASP is undecidable, the FPL translation of (loosely) guarded programs falls in the decidable (loosely) guarded fixed point logic (mu(L)GF). Moreover, we reduce normal closed ASP to loosely guarded OASP, enabling a characterization of an answer set semantics by mu LGF formulas. Finally, we relate guarded OASP to Datalog LITE, thus linking an answer set semantics to a semantics based on fixed point models of extended stratified Datalog programs. From this correspondence, we deduce 2-EXPTIME-completeness of satisfiability checking w.r.t. (loosely) guarded programs.
We consider the problem of identifying equivalence of two knowledge bases which are capable of abductive reasoning. Here, a knowledge base is written in either first-order logic or nonmonotoniclogicprogramming. In t...
详细信息
We consider the problem of identifying equivalence of two knowledge bases which are capable of abductive reasoning. Here, a knowledge base is written in either first-order logic or nonmonotoniclogicprogramming. In this work, we will give two definitions of abductive equivalence. the first one, explainable equivalence, requires that two abductive programs have the same explainability for any observation. Another one, explanatory equivalence, guarantees that any observation has exactly the same explanations in each abductive framework. Explanatory equivalence is a stronger notion than explainable equivalence. In first-order abduction, explainable equivalence can be verified by the notion of extensional equivalence in default theories. In nonmonotoniclogic programs, explanatory equivalence can be checked by means of the notion of relative strong equivalence. We also show the complexity results for abductive equivalence.
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.
this paper motivates and presents a nonmonotonic version of Contextual Intensional logic, a type-theoretic logic intended as a general formalism for reasoning about context. In developing this logic, it is necessary t...
详细信息
Aggregates in answer set programming (ASP) have recently been studied quite intensively. the main focus of previous work has been on defining suitable semantics for programs with arbitrary, potentially recursive aggre...
详细信息
ISBN:
(纸本)3540285385
Aggregates in answer set programming (ASP) have recently been studied quite intensively. the main focus of previous work has been on defining suitable semantics for programs with arbitrary, potentially recursive aggregates. By now, these efforts appear to have converged. On another line of research, the relation between unfounded sets and (aggregate-free) answer sets has lately been rediscovered. It turned out that most of the currently available answer set solvers rely on this or closely related results (e.g., loop formulas). In this paper, we unite these lines and give a new definition of unfounded sets for disjunctive logic programs with arbitrary, possibly recursive aggregates. While being syntactically somewhat different, we can show that this definition properly generalizes all main notions of unfounded sets that have previously been defined for fragments of the language. We demonstrate that, as for restricted languages, answer sets can be crisply characterized by unfounded sets: they are precisely the unfounded-free models. this result can be seen as a confirmation of the robustness of the definition of answer sets for arbitrary aggregates. We also provide a comprehensive complexity analysis for unfounded sets, and study its impact on answer set computation.
暂无评论