Skip to main content
CSIRO Logo Data 61 logo

Superposition and model evolution combined

Authors

Peter Baumgartner and Uwe Waldmann

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,
    issn             = {0302-9743},
    author           = {Baumgartner, Peter and Waldmann, Uwe},
    editor           = {{Renate Schmidt}},
    month            = jul,
    year             = {2009},
    keywords         = {first-order theorem proving},
    address          = {Montreal, Canada},
    title            = {Superposition and Model Evolution Combined},
    pages            = {17--34},
    booktitle        = {Proceedings of the  22nd International Conference on Automated Deduction},
    paperurl         = {https://ts.data61.csiro.au/publications/nicta_full_text/1824.pdf},
    publisher        = {Springer}
  }

Download