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 automatedreasoning ...
详细信息
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 automatedreasoning 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.
Interval Temporal logic (ITL) is a powerful formalism to reason about sequences of events that can occur simultaneously and in an overlapping fashion. Despite its importance for various application domains, little too...
详细信息
ISBN:
(纸本)9783319085876;9783319085869
Interval Temporal logic (ITL) is a powerful formalism to reason about sequences of events that can occur simultaneously and in an overlapping fashion. Despite its importance for various application domains, little tool support for automated ITL reasoning is available, possibly also owed to ITL's undecidability. We consider bounded satisfiability which approximates finite satisfiability and is only NP-complete. We provide an encoding into SAT that is designed to use the power of modern incremental SAT solvers. We present a tool that tests an ITL specification for finite satisfiability.
Several logics for reasoning under uncertainty distribute ''probability mass'' over sets in some sense. these include probabilistic logic, Dempster-Shafer theory, other logics based on belief functions...
详细信息
Several logics for reasoning under uncertainty distribute ''probability mass'' over sets in some sense. these include probabilistic logic, Dempster-Shafer theory, other logics based on belief functions, and second-order probabilistic logic. We show that these logics are instances of a certain type of linear programming model, typically with exponentially many variables. We also show how a single linear programming package can implement these logics computationally if one ''plugs in'' a different column generation subroutine for each logic, although the practicality of this approach has been demonstrated so far only for probabilistic logic.
We describe a method for abbreviating an analytic classical first-order logic by the introduction of a lemma. Our is based on first computing a compressed representation of present in the analytic proof and then a cut...
详细信息
ISBN:
(纸本)9783642287176
We describe a method for abbreviating an analytic classical first-order logic by the introduction of a lemma. Our is based on first computing a compressed representation of present in the analytic proof and then a cut-formula that
Defeasible reasoning is a rule-based approach for efficient reasoning with incomplete and inconsistent information. Such reasoning is, among others, useful for ontology integration, where conflicting information arise...
详细信息
Defeasible reasoning is a rule-based approach for efficient reasoning with incomplete and inconsistent information. Such reasoning is, among others, useful for ontology integration, where conflicting information arises naturally;and for the modeling of business rules and policies, where rules with exceptions are often used. this paper describes these scenarios in more detail, and reports on the implementation of a system for defeasible reasoning on the Web. the system (a) is syntactically compatible with RuleML;(b) features strict and defeasible rules, priorities and two kinds of negation;(c) is based on a translation to logicprogramming with declarative semantics;(d) is flexible and adaptable to different intuitions within defeasible reasoning;and (e) can reason with rules, RDF, RDF Schema and (parts of) OWL ontologies.
An approach where stable models of Disjunctive logic Programs (DLPs) are computed using SMODELS as a core engine is discussed. the approach is based on two program transformations using which the key tasks in computin...
详细信息
ISBN:
(纸本)354020721X
An approach where stable models of Disjunctive logic Programs (DLPs) are computed using SMODELS as a core engine is discussed. the approach is based on two program transformations using which the key tasks in computing disjunctive stable models can be reduced to computing stable models for normal programs. the implementation is based on an architecture where two SMODELS search engines interact. One of the engines is responsible for generating model candidates for a DLP given as input and the other checks for the minimality of the candidates.
Generating the prime implicates of a formula consists in finding its most general consequences. this has many fields of application in automatedreasoning, like planning and diagnosis, and although the subject has bee...
详细信息
ISBN:
(纸本)9783319085876;9783319085869
Generating the prime implicates of a formula consists in finding its most general consequences. this has many fields of application in automatedreasoning, like planning and diagnosis, and although the subject has been extensively studied (and still is) in propositional logic, very few have approached the problem in more expressive logics because of its intrinsic complexity. this paper presents one such approach for flat ground equational logic. Aiming at efficiency, it intertwines an existing method to generate all prime implicates of a formula with a rewriting technique that uses atomic equations to simplify the problem by removing constants during the search. the soundness, completeness and termination of the algorithm are proven. the algorithm has been implemented and an experimental analysis is provided.
One of the major reasons for the success of answer set programming in recent years was the shift from a theorem proving to a constraint programming view: problems are represented such that stable models, respectively ...
详细信息
ISBN:
(纸本)354020721X
One of the major reasons for the success of answer set programming in recent years was the shift from a theorem proving to a constraint programming view: problems are represented such that stable models, respectively answer sets, rather than theorems correspond to solutions. this shift in perspective proved extremely fruitful in many areas. We believe that going one step further from a "hard" to a "soft" constraint programming paradigm, or, in other words, to a paradigm of qualitative optimization, will prove equally fruitful. In this paper we try to support this claim by showing that several generic problems in logic based problem solving can be understood as qualitative optimization problems, and that these problems have simple and elegant formulations given adequate optimization constructs in the knowledge representation language.
the exploitation of ASP systems for solving real application problems pointed out the need of combining the expressive power of ASP programming withthe efficient data management features of existing DBMSs. this paper...
详细信息
ISBN:
(纸本)354020721X
the exploitation of ASP systems for solving real application problems pointed out the need of combining the expressive power of ASP programming withthe efficient data management features of existing DBMSs. this paper presents DLVDB, an extension to the DLV system allowing to instantiate logic programs directly on databases and to handle input and output data distributed on several databases.
the Dagstuhl Initiative for systematic benchmarking in answer set programming (ASP) is discussed. Benchmarking is needed in ASP to establish a good practices in the fields of satisfiablity testing and constraint progr...
详细信息
ISBN:
(纸本)354020721X
the Dagstuhl Initiative for systematic benchmarking in answer set programming (ASP) is discussed. Benchmarking is needed in ASP to establish a good practices in the fields of satisfiablity testing and constraint programming. the ASP is facing difficulty of not having a common input language and disagreement on all functionalities. the benchmarking system facilitates the execution of ASP solvers under the same conditions, quaranteeing reproducible and reliable performance outputs.
暂无评论