A combined superposition and model evolution calculus (Q438531)

The paper presents a new calculus for first-order theorem proving with equality, which generalizes both the superposition calculus and the model evolution calculus (with equality). This calculus integrates the inference rules of superposition and of model evolution preserving the individual semantically-based redundancy criteria of both calculi in a single framework. Moreover, this work simplifies the presentation of the model evolution calculus by using the better-known superposition framework. The main result of the paper is the completeness proof of the calculus under semantically justified redundancy criteria and simplification rules.