@INPROCEEDINGS{Baumgartner:Tinelli:ModelEvolutionCalculusEquality:CADE:2005,
  AUTHOR = {Peter Baumgartner and Cesare Tinelli},
  TITLE = {The Model Evolution Calculus with Equality},
  CROSSREF = {CADE:05},
  PAGES = {392-408},
  URL = {http://www.mpi-sb.mpg.de/~baumgart/publications/BaumgartnerTinelli-CADE-20.pdf},
  ABSTRACT = {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 ordered
  paramodulation inference rule, where equations used for
  paramodulation 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 result is the correctness of the MEE calculus in the
  presence of very general redundancy elimination criteria.}
}