Paper Info
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 Vlaeminck1303.44
Johan Wittocx21099.37
Joost Vennekens343437.36
Marc Denecker41626106.40
Maurice Bruynooghe52767226.05