MPI-INF RG1 Publications: Proceedings Article: Superposition and Model Evolution Combined

Proceedings Article, Paper
@InProceedings
Beitrag in Tagungsband, Workshop

Show entries of:

this year (2013) | last year (2012) | two years ago (2011) | Notes URL

Action:

Options:

Library locked

Goto entry point

Author, Editor

Author(s):

Baumgartner, Peter
Waldmann, Uwe

dblp
dblp

Not MPG Author(s):

Baumgartner, Peter

Editor(s):

Schmidt, Renate A.

dblp

Not MPII Editor(s):

Schmidt, Renate A.

BibTeX cite key*:

BaumgartnerWaldmann2009CADE

Title, Booktitle

Title*:	Superposition and Model Evolution Combined
Booktitle*:	Automated Deduction - CADE-22 : 22nd International Conference on Automated Deduction

Event, URLs

URL of the conference:
URL for downloading the paper:	http://dx.doi.org/10.1007/978-3-642-02959-2_2
Event Address*:	Montreal, Canada	Language:	English
Event Date* (no longer used):		Organization:
Event Start Date:	2 August 2009	Event End Date:	7 August 2009

Publisher

Name*:	Springer	URL:	http://www.springer.de/
Address*:	Berlin, Germany	Type:

Vol, No, Year, pp.

Series:

Lecture Notes in Artificial Intelligence

Volume:	5663	Number:
Month:	August	Pages:	17-34
Year*:	2009	VG Wort Pages:	32
ISBN/ISSN:	978-3-642-02958-5	Sequence Number:
DOI:	10.1007/978-3-642-02959-2_2


(LaTeX) 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.
Keywords:	Theorem Proving


Download Access Level:	Public

Correlation

MPG Unit:	Max-Planck-Institut für Informatik

MPG Subunit:	Automation of Logic
Appearance:	MPII WWW Server, MPII FTP Server, MPG publications list, university publications list, working group publication list, Fachbeirat, VG Wort

BibTeX Entry:

@INPROCEEDINGS{BaumgartnerWaldmann2009CADE,
AUTHOR = {Baumgartner, Peter and Waldmann, Uwe},
EDITOR = {Schmidt, Renate A.},
TITLE = {Superposition and Model Evolution Combined},
BOOKTITLE = {Automated Deduction - CADE-22 : 22nd International Conference on Automated Deduction},
PUBLISHER = {Springer},
YEAR = {2009},
VOLUME = {5663},
PAGES = {17--34},
SERIES = {Lecture Notes in Artificial Intelligence},
ADDRESS = {Montreal, Canada},
MONTH = {August},
ISBN = {978-3-642-02958-5},
DOI = {10.1007/978-3-642-02959-2_2},
}

Entry last modified by Anja Becker, 03/25/2010

Edit History (please click the blue arrow to see the details)

Attachment Section