Strong equivalence is an important property for nonmonotonic formalisms, allowing safe local changes to a nonmonotonictheory. this paper considers strong equivalence for nonmonotonic causal theories of the kind intro...
详细信息
ISBN:
(纸本)354020721X
Strong equivalence is an important property for nonmonotonic formalisms, allowing safe local changes to a nonmonotonictheory. this paper considers strong equivalence for nonmonotonic causal theories of the kind introduced by McCain and Turner. Causal theories T-1 and T-2 are strongly equivalent if, for every causal theory T, T-1 boolean OR T and T-2 boolean OR T are equivalent (that is, have the same causal models). the paper introduces a convenient characterization of this property in terms of so-called SE-models, much as was done previously for answer set programs and default theories. A similar result is provided for the nonmonotonic modal logic UCL. the paper also introduces a reduction from the problem of deciding strong equivalence of two causal theories to the problem of deciding equivalence of two sets of propositional formulas.
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.
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 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.
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.
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 language of nonmonotonic causal theories, defined by Norman McCain and Hudson Turner, is an important formalism for representing properties of actions. For causal theories of a special kind, called definite, a sim...
详细信息
ISBN:
(纸本)354020721X
the language of nonmonotonic causal theories, defined by Norman McCain and Hudson Turner, is an important formalism for representing properties of actions. For causal theories of a special kind, called definite, a simple translation into the language of logic programs under the answer set semantics is available. In this paper we define a similar translation for causal theories of a more general form, called almost definite. Such theories can be used, for instance, to characterize the transitive closure of a binary relation. the new translation leads to an implementation of a subclass of almost definite causal theories that employs the answer set solver SMODELS as the search engine.
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 nonmonotoniclogic 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.
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.
暂无评论