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]
Collections | ANU 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 | Size | Format | Image |
---|---|---|---|---|
01_Baumgartner_The_model_evolution_calculus_2008.pdf | 769.59 kB | Adobe 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