The model evolution calculus with equality

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 (ℳε), a first-order version of the prepositional DPLL procedure. The new calculus, ℳεE, is a proper extension of the ℳε calculus without equality. Like ℳε it maintains an explicit candidate model, which is searched for by DPLL-style splitting. For equational reasoning ℳεE 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 ℳεE calculus in the presence of very general redundancy elimination criteria. Show more