Title | ||
---|---|---|
An Approximative Inference Method for Solving THERE EXISTS FOR ALL SO Satisfiability Problems |
Abstract | ||
---|---|---|
The fragment there exists for all SO(ID) of second order logic extended with inductive definitions is expressive, and many interesting problems, such as conformant planning, can be naturally expressed as finite domain satisfiability problems of this logic. Such satisfiability problems are computationally hard (Sigma(P)(2)). In this paper, we develop an approximate, sound but incomplete method for solving such problems that transforms a there exists for all SO(ID) to a there exists SO(ID) problem. The finite domain satisfiability problem for the latter language is in NP and can be handled by several existing solvers. We show that this provides an effective method for solving practically useful problems, such as common examples of conformant planning. We also propose a more complete translation to there exists for all SO(FP), existential SO extended with nested inductive and coinductive definitions. |
Year | DOI | Venue |
---|---|---|
2010 | 10.1007/978-3-642-15675-5_28 | Lecture Notes in Artificial Intelligence |
Keywords | Field | DocType |
satisfiability | Existential quantification,Inference,Computer science,Satisfiability,Theoretical computer science | Conference |
Volume | ISSN | Citations |
6341 | 0302-9743 | 0 |
PageRank | References | Authors |
0.34 | 6 | 5 |
Name | Order | Citations | PageRank |
---|---|---|---|
Hanne Vlaeminck | 1 | 30 | 3.44 |
Johan Wittocx | 2 | 109 | 9.37 |
Joost Vennekens | 3 | 434 | 37.36 |
Marc Denecker | 4 | 1626 | 106.40 |
Maurice Bruynooghe | 5 | 2767 | 226.05 |