English
 
User Manual Privacy Policy Disclaimer Contact us
  Advanced SearchBrowse

Item

ITEM ACTIONSEXPORT

Released

Conference Paper

Superposition and Model Evolution Combined

MPS-Authors
/persons/resource/persons45689

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

Locator
There are no locators available
Fulltext (public)
There are no public fulltexts available
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: http://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.