Proceedings Article, Paper
@InProceedings
Beitrag in Tagungsband, Workshop


Show entries of:

this year (2019) | last year (2018) | two years ago (2017) | Notes URL

Action:

login to update

Options:








Author, Editor

Author(s):

Baumgartner, Peter
Tinelli, Cesare

dblp
dblp

Not MPG Author(s):

Tinelli, Cesare

Editor(s):

Nieuwenhuis, Robert

dblp

Not MPII Editor(s):

Nieuwenhuis, Robert

BibTeX cite key*:

Baumgartner:Tinelli:ModelEvolutionCalculusEquality:CADE:2005

Title, Booktitle

Title*:

The Model Evolution Calculus with Equality

Booktitle*:

Automated deduction - CADE-20 : 20th International Conference on Automated Deduction

Event, URLs

URL of the conference:


URL for downloading the paper:

http://www.mpi-inf.mpg.de/~baumgart/publications/BaumgartnerTinelli-CADE-20.pdf

Event Address*:

Tallinn, Estonia

Language:

English

Event Date*
(no longer used):


Organization:


Event Start Date:

22 July 2005

Event End Date:

27 August 2005

Publisher

Name*:

Springer

URL:

http://www.springer-ny.com/

Address*:

New York, USA

Type:


Vol, No, Year, pp.

Series:

Lecture Notes in Artificial Intelligence

Volume:

3632

Number:


Month:


Pages:

392-408

Year*:

2005

VG Wort Pages:

28

ISBN/ISSN:

3-540-28005-7

Sequence Number:


DOI:




Note, Abstract, ©


(LaTeX) Abstract:

In many theorem proving applications, a proper treatment of
equational theories or equality is mandatory. In this paper we show
how to integrate a modern treatment of equality in the Model
Evolution calculus (ME), a first-order version of the propositional
DPLL procedure. The new calculus, MEE, is a proper extension of
the ME calculus without equality. Like ME it maintains an explicit
``candidate model'', which is searched for by DPLL-style splitting.
For equational reasoning MEE uses an adapted version of the ordered
paramodulation inference rule, where equations used for
paramodulation are drawn (only) from the candidate model. The
calculus also features a generic, semantically justified
simplification rule which covers many simplification techniques
known from superposition-style theorem proving. Our main result is
the refutational completeness of the MEE calculus.

Keywords:

Automated Theorem Proving, Instance Based Methods, Equality



Download
Access Level:

Public

Correlation

MPG Unit:

Max-Planck-Institut für Informatik



MPG Subunit:

Programming Logics Group

Appearance:

MPII WWW Server, MPII FTP Server, MPG publications list, university publications list, working group publication list, Fachbeirat, CCL bibliography, VG Wort



BibTeX Entry:

@INPROCEEDINGS{Baumgartner:Tinelli:ModelEvolutionCalculusEquality:CADE:2005,
AUTHOR = {Baumgartner, Peter and Tinelli, Cesare},
EDITOR = {Nieuwenhuis, Robert},
TITLE = {The Model Evolution Calculus with Equality},
BOOKTITLE = {Automated deduction - CADE-20 : 20th International Conference on Automated Deduction},
PUBLISHER = {Springer},
YEAR = {2005},
VOLUME = {3632},
PAGES = {392--408},
SERIES = {Lecture Notes in Artificial Intelligence},
ADDRESS = {Tallinn, Estonia},
ISBN = {3-540-28005-7},
}


Entry last modified by Uwe Brahm, 01/28/2008
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 Edit History (please click the blue arrow to see the details)Edit History (please click the blue arrow to see the details)

Editor(s)
Peter Baumgartner
Created
05/01/2005 02:43:23 PM
Revisions
4.
3.
2.
1.
0.
Editor(s)
Uwe Brahm
Christine Kiesel
Viorica Sofronie-Stokkermans
Peter Baumgartner
Peter Baumgartner
Edit Dates
09-06-2006 18:58:49
21.12.2005 09:53:47
11/21/2005 03:35:30 PM
05/02/2005 01:54:21 PM
05/01/2005 02:43:23 PM
Show details for Attachment SectionAttachment Section
Hide details for Attachment SectionAttachment Section