MPI-INF RG1 Publications: Journal Article: A Combined Superposition and Model Evolution Calculus

Journal Article
@Article
Artikel in Fachzeitschrift

Show entries of:

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

Action:

Options:

Library locked

Goto entry point

Author, Editor(s)

Author(s):

Baumgartner, Peter
Waldmann, Uwe

dblp
dblp

Not MPG Author(s):

Baumgartner, Peter

BibTeX cite key*:

BaumgartnerWaldmann2011

Title

Title*:

A Combined Superposition and Model Evolution Calculus

Journal

Journal Title*:	Journal of Automated Reasoning	Journal's URL:	http://www.springerlink.com/content/0168-7433/
Download URL for the article:	http://dx.doi.org/10.1007/s10817-010-9214-x	Language:	English

Publisher

Publisher's Name:	Springer	Publisher's URL:	http://www.springerlink.com/
Publisher's Address:	Dordrecht	ISSN:	0168-7433

Vol, No, pp, Date

Volume*:	47	Number:	2
Publishing Date:	August 2011
Pages*:	191-227	Number of VG Pages:	191-227
Page Start:	191	Page End:	227
Sequence Number:		DOI:	10.1007/s10817-010-9214-x

Note:
(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 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.
URL for the Abstract:
Categories, Keywords:	Theorem Proving
HyperLinks / References / URLs:
Copyright Message:
Personal Comments:
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:

@ARTICLE{BaumgartnerWaldmann2011,
AUTHOR = {Baumgartner, Peter and Waldmann, Uwe},
TITLE = {A Combined Superposition and Model Evolution Calculus},
JOURNAL = {Journal of Automated Reasoning},
PUBLISHER = {Springer},
YEAR = {2011},
NUMBER = {2},
VOLUME = {47},
PAGES = {191--227},
ADDRESS = {Dordrecht},
MONTH = {August},
ISBN = {0168-7433},
DOI = {10.1007/s10817-010-9214-x},
}

Entry last modified by Anja Becker, 03/16/2012

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

Attachment Section