Skip navigation
Skip navigation

The model evolution calculus as a first-order DPLL method

Baumgartner, Peter; Tinelli, Cesare

Description

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
URI: http://hdl.handle.net/1885/50162
Source: Artificial Intelligence
DOI: 10.1016/j.artint.2007.09.005

Download

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:  20 July 2017/ Responsible Officer:  University Librarian/ Page Contact:  Library Systems & Web Coordinator