Superposition and model evolution combined

Peter Baumgartner*, Uwe Waldmann

*Corresponding author for this work

    Research output: Chapter in Book/Report/Conference proceedingConference contributionpeer-review

    10 Citations (Scopus)

    Abstract

    We present a new calculus for first-order theorem proving with equality, Με+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.

    Original languageEnglish
    Title of host publicationAutomated Deduction - CADE-22 - 22nd International Conference on Automated Deduction, Proceedings
    Pages17-34
    Number of pages18
    DOIs
    Publication statusPublished - 2009
    Event22nd International Conference on Automated Deduction, CADE-22 - Montreal, QC, Canada
    Duration: 2 Aug 20097 Aug 2009

    Publication series

    NameLecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
    Volume5663 LNAI
    ISSN (Print)0302-9743
    ISSN (Electronic)1611-3349

    Conference

    Conference22nd International Conference on Automated Deduction, CADE-22
    Country/TerritoryCanada
    CityMontreal, QC
    Period2/08/097/08/09

    Fingerprint

    Dive into the research topics of 'Superposition and model evolution combined'. Together they form a unique fingerprint.

    Cite this