Skip navigation
Skip navigation

Model Evolution with equality - Revised and Implemented

Baumgartner, Peter; Pelzer, Bjorn; Tinelli, Cesare


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]

CollectionsANU Research Publications
Date published: 2011
Type: Journal article
Source: Journal of Symbolic Computation
DOI: 10.1016/j.jsc.2011.12.031


File Description SizeFormat Image
01_Baumgartner_Model_Evolution_with_equality_2011.pdf571.92 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