Skip navigation
Skip navigation

The model evolution calculus as a first-order DPLL method

Baumgartner, Peter; Tinelli, Cesare


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 FDPLL calculus by Baumgartner was the first successful attempt to lift the procedure to the first-order level without resorting to ground...[Show more]

CollectionsANU Research Publications
Date published: 2008
Type: Journal article
Source: Artificial Intelligence
DOI: 10.1016/j.artint.2007.09.005


File Description SizeFormat Image
01_Baumgartner_The_model_evolution_calculus_2008.pdf769.59 kBAdobe PDF    Request a copy

Items in Open Research are protected by copyright, with all rights reserved, unless otherwise indicated.

Updated:  19 May 2020/ Responsible Officer:  University Librarian/ Page Contact:  Library Systems & Web Coordinator