The model evolution calculus as a first-order DPLL method
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|
|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.