Baumgartner, PeterPelzer, BjornTinelli, Cesare2015-12-080747-7171http://hdl.handle.net/1885/30996In 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.Keywords: Automated theorem proving; Instance-based methods201110.1016/j.jsc.2011.12.0312016-02-24