In Renate A. Schmidt, editor, Automated Deduction, CADE-22, 22nd International Conference on Automated Deduction, LNAI 5663, pages 17-34, Montreal, Canada, August 2-7, 2009. Springer-Verlag.
Extended version of the proceedings article: [PDF file]
Revised version: A Combined Superposition and Model Evolution Calculus, accepted for JAR.
Abstract: We present a new calculus for first-order theorem proving with equality, ME+Sup, which generalizes both the Superposition calculus and the Model Evolution calculus (with equality) by integrating their inference rules and redundancy criteria in a non-trivial way. The main motivation is to combine the advantageous features of both---rather complementary---calculi in a single framework. For instance, Model Evolution, as a lifted version of the propositional DPLL procedure, contributes a non-ground splitting rule that effectively permits to split a clause into non variable disjoint subclauses. In the paper we present the calculus in detail. Our main result is its completeness under semantically justified redundancy criteria and simplification rules.