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.
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.
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.
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.
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.
A new system CMODELS-2 which is able to fix ASSAT's disadvantages was presented. It was found that the new system organizes the search process more efficiently than ASSAT as it does not explore the same part of th...
详细信息
ISBN:
(纸本)354020721X
A new system CMODELS-2 which is able to fix ASSAT's disadvantages was presented. It was found that the new system organizes the search process more efficiently than ASSAT as it does not explore the same part of the search tree more than once. the input language of CMODELS is generated by the preprocessor LPARSE. CMODELS is an answer set solver that uses SAT solvers as search engines.
For a given semantics, two logic programs Pi(1) and Pi(2) can be said to be equivalent if they have the same intended models and strongly equivalent if for any program X, Pi(1) boolean OR X and Pi(2) boolean OR X are ...
详细信息
ISBN:
(纸本)354020721X
For a given semantics, two logic programs Pi(1) and Pi(2) can be said to be equivalent if they have the same intended models and strongly equivalent if for any program X, Pi(1) boolean OR X and Pi(2) boolean OR X are equivalent. Eiter and Fink have recently studied and characterised under answer set semantics a further, related property of uniform equivalence, where the extension X is required to be a set of atoms. We extend their main results to propositional theories in equilibrium logic and describe a tableaux proof system for checking the property of uniform equivalence. We also show that no new forms of equivalence are obtained by varying the logical form of expressions in the extension X. Finally, some examples are studied including special cases of nested and generalized rules.
We consider the simplification of logic programs under the stable-model semantics, with respect to the notions of strong and uniform equivalence between logic programs, respectively. Both notions have recently been co...
详细信息
ISBN:
(纸本)354020721X
We consider the simplification of logic programs under the stable-model semantics, with respect to the notions of strong and uniform equivalence between logic programs, respectively. Both notions have recently been considered for nonmonotonic logic programs (the latter dates back to the 1980s, though) and provide semantic foundations for optimizing programs with input. Extending previous work, we investigate syntactic and semantic rules for program transformation, based on proper notions of consequence. We furthermore provide encodings of these notions in answer-set programming, and give characterizations of programs which are semantically equivalent to positive and Horn programs, respectively. Finally, we investigate the complexity of program simplification and determining semantical equivalence, showing that the problems range between coNP and II2P complexity, and we present some tractable cases.
暂无评论