• search hit 353 of 354
Back to Result List

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 proof­ procedure 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 litfing of the DPLL procedure, the new calculus contains a more systematic treatment of universal literals, one of FDPLL's optimizations, and so has the potential of leading to much faster implementations.

Download full text files

Export metadata

Additional Services

Share in Twitter Search Google Scholar
Author:Peter Baumgartner, Cesare Tinelli
Series (Volume no.):Fachberichte Informatik (2003,1)
Document Type:Part of Periodical
Date of completion:2004/06/08
Date of publication:2004/06/08
Publishing institution:Universität Koblenz-Landau, Campus Koblenz, Universitätsbibliothek
Release Date:2004/06/08
Tag:DPLL procedure; first-order logic; model generation; sequent calculi
Number of pages:61
Institutes:Fachbereich 4 / Institut für Informatik
Dewey Decimal Classification:0 Informatik, Informationswissenschaft, allgemeine Werke / 00 Informatik, Wissen, Systeme / 004 Datenverarbeitung; Informatik
Licence (German):License LogoEs gilt das deutsche Urheberrecht: § 53 UrhG