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 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 . MEE 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.