Journal Article
@Article
Artikel in Fachzeitschrift


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(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, Abstract, ©

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
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)
Hide details for Attachment SectionAttachment Section