Model Evolution with equality - Revised and Implemented
In many theorem proving applications, a proper treatment of equational theories or equality is mandatory. In this paper, we show how to integrate a modern treatment of equality in the Model Evolution calculus (. ME), a first-order version of the propositional DPLL procedure. The new calculus, . MEE, is a proper extension of the . ME calculus without equality. Like . ME it maintains an explicit . candidate model, which is searched for by DPLL-style splitting. For equational reasoning . MEE uses...[Show more]
|Collections||ANU Research Publications|
|Source:||Journal of Symbolic Computation|
|01_Baumgartner_Model_Evolution_with_equality_2011.pdf||571.92 kB||Adobe PDF||Request a copy|
Items in Open Research are protected by copyright, with all rights reserved, unless otherwise indicated.