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 (M E), a first-order version of the propositional DPLL procedure. The new calculus,M E-E, is a proper extension of the M E calculus without equality. Like M E it maintains an explicit candidate model, which is searched for by DPLL-style splitting. For equational reasoning M E-E uses an adapted version of the superposition inference rule, where equations used for superposition are drawn (only) from the candidate model. The calculus also features a generic, semantically justified simplification rule which covers many simplification techniques known from superposition-style theorem proving. Our main theoretical result is the correctness of the M E-E calculus in the presence of very general redundancy elimination criteria. We also describe our implementation of the calculus, the E-Darwin system, and we report on practical experiments with it on the TPTP problem library. (C) 2011 Elsevier Ltd. All rights reserved.
automated theorem proving instance-based methods