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.
Almost all existing methodologies and automated tools for knowledge acquisition are somehow based on classical mathematical logic or its various classical conservative extensions. this paper proposes a new approach to...
详细信息
ISBN:
(纸本)3540408037
Almost all existing methodologies and automated tools for knowledge acquisition are somehow based on classical mathematical logic or its various classical conservative extensions. this paper proposes a new approach to knowledge acquisition problem: automated knowledge acquisition by relevant reasoning based on strong relevant logic. the paper points out why any of the classical mathematical logic, its various classical conservative extensions, and traditional relevant logics is not a suitable logical basis for knowledge acquisition, shows that strong relevant logic is a more hopeful candidate for the purpose, and establishes a conceptional foundation for automated knowledge acquisition by relevant reasoning based on strong relevant logic.
Many NP-complete problems can be encoded in the answer set semantics of logic programs in a very concise way, where the encoding reflects the typical "guess and check" nature of NP problems: the property is ...
详细信息
ISBN:
(纸本)354020721X
Many NP-complete problems can be encoded in the answer set semantics of logic programs in a very concise way, where the encoding reflects the typical "guess and check" nature of NP problems: the property is encoded in a way such that polynomial size certificates for it correspond to stable models of a program. However, the problem-solving capacity of full disjunctive logic programs (DLPs) is beyond NP at the second level of the polynomial hierarchy. While problems there also have a "guess and check" structure, an encoding in a DLP is often non-obvious, in particular if the "check" itself is co-NP-complete;usually, such problems are solved by interleaving separate "guess" and "check" programs, where the check is expressed by inconsistency of the check program. We present general transformations of head-cycle free (extended) logic programs into stratified disjunctive logic programs which enable one to integrate such "guess" and "check" programs automatically into a single disjunctive logic program. Our results complement recent results on meta-interpretation in ASP, and extend methods and techniques for a declarative "guess and check" problem solving paradigm through ASP.
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.
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.
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.
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.
this paper presents a modified version of forward chaining method of reasoning and a prototype implementation called Sylar - System for logic and automatedreasoning, which can be used for situation management. the me...
详细信息
ISBN:
(纸本)9783319198576;9783319198569
this paper presents a modified version of forward chaining method of reasoning and a prototype implementation called Sylar - System for logic and automatedreasoning, which can be used for situation management. the method, presented by the authors, implements Modus Ponens and Modus Tollens by Truth tables and a SAT solver to discover hidden knowledge and suggest decisions. Also, it gives the opportunity to use multi-step inferences. Proposed method is suitable for this specific kind of decision making process.
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.
暂无评论