Deutsch
 
Hilfe Datenschutzhinweis Impressum
  DetailsucheBrowse

Datensatz

 
 
DownloadE-Mail
  A Combined Superposition and Model Evolution Calculus

Baumgartner, P., & Waldmann, U. (2011). A Combined Superposition and Model Evolution Calculus. Journal of Automated Reasoning, 47(2), 191-227. doi:10.1007/s10817-010-9214-x.

Item is

Externe Referenzen

einblenden:

Urheber

einblenden:
ausblenden:
 Urheber:
Baumgartner, Peter1, Autor           
Waldmann, Uwe2, Autor           
Affiliations:
1External Organizations, ou_persistent22              
2Automation of Logic, MPI for Informatics, Max Planck Society, ou_1116545              

Inhalt

einblenden:
ausblenden:
Schlagwörter: -
 Zusammenfassung: 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 \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. We also show how under certain assumptions the model representation computed by a (finite and fair) derivation can be queried in an effective way.

Details

einblenden:
ausblenden:
Sprache(n): eng - English
 Datum: 2011
 Publikationsstatus: Erschienen
 Seiten: -
 Ort, Verlag, Ausgabe: -
 Inhaltsverzeichnis: -
 Art der Begutachtung: Expertenbegutachtung
 Identifikatoren: eDoc: 619011
DOI: 10.1007/s10817-010-9214-x
URI: http://dx.doi.org/10.1007/s10817-010-9214-x
Anderer: Local-ID: C125716C0050FB51-7A229209F0F88A46C12578410073AE24-BaumgartnerWaldmann2011
 Art des Abschluß: -

Veranstaltung

einblenden:

Entscheidung

einblenden:

Projektinformation

einblenden:

Quelle 1

einblenden:
ausblenden:
Titel: Journal of Automated Reasoning
Genre der Quelle: Zeitschrift
 Urheber:
Affiliations:
Ort, Verlag, Ausgabe: Dordrecht : Springer
Seiten: - Band / Heft: 47 (2) Artikelnummer: - Start- / Endseite: 191 - 227 Identifikator: ISSN: 0168-7433