Superposition and Model Evolution Combined

Baumgartner, Peter; Waldmann, Uwe

doi:10.1007/978-3-642-02959-2_2

Item

ITEM ACTIONSEXPORT

Add to Basket

Please note that a newer version of this item is available:
https://pure.mpg.de/pubman/item/item_1324406_3

DetailsSummary

Released

Conference Paper

Superposition and Model Evolution Combined

MPS-Authors

/persons/resource/persons45689

Waldmann, Uwe
Automation of Logic, MPI for Informatics, Max Planck Society;

External Resource

No external resources are shared

Fulltext (restricted access)

There are currently no full texts shared for your IP range.

Fulltext (public)

There are no public fulltexts stored in PuRe

Supplementary Material (public)

There is no public supplementary material available

Citation

Baumgartner, P., & Waldmann, U. (2009). Superposition and Model Evolution Combined. In R. A. Schmidt (Ed.), Automated Deduction, CADE-22, 22nd International Conference on Automated Deduction (pp. 17-34). Berlin, Germany: Springer.

Cite as: https://hdl.handle.net/11858/00-001M-0000-000F-1A6C-9

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.