MPI-INF Logo
Publications

Server    domino.mpi-inf.mpg.de

Proceedings Article, Paper
@InProceedings
Beitrag in Tagungsband, Workshop

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
Conference URL::
Downloading URL:
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
Hide details for Edit History (please click the blue arrow to see the details)Edit History (please click the blue arrow to see the details)

Editor(s)
[Library]
Created
08/24/2009 08:33:57 PM
Revision
1.
0.


Editor
Anja Becker
Uwe Waldmann


Edit Date
25.03.2010 11:18:13
24.08.2009 20:33:57