The Model Evolution Calculus

10 years 6 months ago
The Model Evolution Calculus
The DPLL procedure is the basis of some of the most successful propositional satisfiability solvers to date. Although originally devised as a proofprocedure for first-order logic, it has been used almost exclusively for propositional logic so far because of its highly inefficient treatment of quantifiers, based on instantiation into ground formulas. The recent FDPLL calculus by Baumgartner was the first successful attempt to lift the procedure to the first-order level without resorting to ground instantiations. FDPLL lifts to the first-order case the core of the DPLL procedure, the splitting rule, but ignores other aspects of the procedure that, although not necessary for completeness, are crucial for its effectiveness in practice. In this paper, we present a new calculus loosely based on FDPLL that lifts these aspects as well. In addition to being a more faithful lifting of the DPLL procedure, the new calculus contains a more systematic treatment of universal literals, one of FDPLL�...
Peter Baumgartner, Cesare Tinelli
Added 03 Dec 2009
Updated 03 Dec 2009
Type Conference
Year 2003
Where CADE
Authors Peter Baumgartner, Cesare Tinelli
Comments (0)