nlp is a compiler for nested logicprogramming under answer set semantics. It is designed as a front-end translating nested logic programs into disjunctive ones, whose answer sets are then computable by disjunctive lo...
详细信息
ISBN:
(纸本)354020721X
nlp is a compiler for nested logicprogramming under answer set semantics. It is designed as a front-end translating nested logic programs into disjunctive ones, whose answer sets are then computable by disjunctive logicprogramming systems, like dlv or gnt. nlp offers different translations: One is polynomial but necessitates the introduction of new atoms, another is exponential in the worst case but avoids extending the language. We report experimental results, comparing the translations on several classes of benchmark problems.
the Interactive theorem Prover (ITP), an environment that supports research into the theory and application of automatedreasoning, is described. ITP is an interactive system providing convenient access to and control...
详细信息
Several methods to compute the prime implicants and the prime implicates of a negation normal form (NNF) formula are developed and implemented. An algorithm PI is introduced that is an extension to negation normal for...
详细信息
Several methods to compute the prime implicants and the prime implicates of a negation normal form (NNF) formula are developed and implemented. An algorithm PI is introduced that is an extension to negation normal form of an algorithm given by Jackson and Pais. ir. correctness proof of the PI algorithm is given. the PI algorithm alone is sufficient in a computational sense, However, it can be combined with path dissolution, and it is shown empirically that this is often an advantage. None of these variations rely on conjunct ive normal form or on disjunctive normal form. A class of formulas is described for which reliance on CNF or on DNF results in ar. exponential increase in the time required to compute prime implicants/implicates. the possibility of avoiding this problem with efficient structure preserving clause form translations is examined briefly and appears unfavorable.
We introduce a family of partial stable model semantics for logic programs with arbitrary aggregate relations. the semantics are parametrized by the interpretation of aggregate relations in three-valued logic. Any sem...
详细信息
ISBN:
(纸本)354020721X
We introduce a family of partial stable model semantics for logic programs with arbitrary aggregate relations. the semantics are parametrized by the interpretation of aggregate relations in three-valued logic. Any semantics in this family satisfies two important properties: (i) it extends the partial stable semantics for normal logic programs and (ii) total stable models are always minimal. We also give a specific instance of the semantics and show that it has several attractive features.
We propose the Neural logic Machine (NLM), a neural-symbolic architecture for both inductive learning and logicreasoning. NLMs exploit the power of both neural networks-as function approximators, and logic programmin...
详细信息
We describe WSAT(CC), a local-search solver for computing models of theories in the language of propositional logic extended by cardinality atoms. WSAT(CC) is a processing back-end for the logic PS+, a recently propos...
详细信息
ISBN:
(纸本)354020721X
We describe WSAT(CC), a local-search solver for computing models of theories in the language of propositional logic extended by cardinality atoms. WSAT(CC) is a processing back-end for the logic PS+, a recently proposed formalism for answer-set programming.
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.
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.
暂无评论