Superposition and model evolution combined
Authors
Max-Planck-Institute for Computer Science
Abstract
We present a new calculus for first-order theorem proving with equality, \MESUP, 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 allows now to split a clause into \emph{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.
BibTeX Entry
@inproceedings{Baumgartner_Waldmann_09, publisher = {Springer}, author = {Baumgartner, Peter and Waldmann, Uwe}, issn = {0302-9743}, month = jul, editor = {{Renate Schmidt}}, year = {2009}, keywords = {first-order theorem proving}, title = {Superposition and Model Evolution Combined}, booktitle = {Automated Deduction --- CADE-22}, pages = {17--34}, address = {Montreal, Canada} }