Proceedings Article, Paper
@InProceedings
Beitrag in Tagungsband, Workshop


Show entries of:

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

Action:

login to update

Options:




Library Locked Library locked




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



Note, Abstract, ©


(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
Show details for Edit History (please click the blue arrow to see the details)Edit History (please click the blue arrow to see the details)
Show details for Attachment SectionAttachment Section