Skip to main content

TS

A combined superposition and model evolution calculus

Authors

Peter Baumgartner and Uwe Waldmann

NICTA

Australian National University

Max-Planck-Institute for Computer Science

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 these two rather complementary calculi in a single framework. In particular, 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. We also show how under certain assumptions the model representation computed by a (finite and fair) derivation can be queried in an effective way.

BibTeX Entry

  @article{Baumgartner_Waldmann_11,
    author           = {Baumgartner, Peter and Waldmann, Uwe},
    journal          = {Journal of Automated Reasoning},
    issn             = {0168-7433},
    number           = {2},
    month            = aug,
    volume           = {47},
    year             = {2011},
    keywords         = {automated theorem proving, instance-based methods, superposition},
    title            = {A Combined Superposition and Model Evolution Calculus},
    pages            = {191-227}
  }

Download

Served by Apache on Linux on seL4.