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):

Bachmair, Leo
Ganzinger, Harald
Voronkov, Andrei

dblp
dblp
dblp



Editor(s):

Kirchner, Claude
Kirchner, Hélène

dblp
dblp



BibTeX cite key*:

BachmairGanzingerVoronkov-98-cade

Title, Booktitle

Title*:

Elimination of Equality via Transformation with Ordering Constraints

Booktitle*:

Proceedings of the 15th International Conference on Automated Deduction (CADE-98)

Event, URLs

URL of the conference:


URL for downloading the paper:


Event Address*:

Lindau, Germany

Language:

English

Event Date*
(no longer used):

July, 5-10 1998

Organization:


Event Start Date:

17 September 2019

Event End Date:

17 September 2019

Publisher

Name*:

Springer

URL:


Address*:

Berlin, Germany

Type:


Vol, No, Year, pp.

Series:

Lecture Notes in Artificial Intelligence

Volume:

1421

Number:


Month:

July

Pages:

175-190

Year*:

1998

VG Wort Pages:


ISBN/ISSN:

3-540-64675-2

Sequence Number:


DOI:




Note, Abstract, ©

Note:

Short version of MPI-I-97-2-012

(LaTeX) Abstract:

We refine Brand's method for eliminating equality axioms by

(i)
imposing ordering constraints on
auxiliary variables introduced during the transformation process
and
(ii)
avoiding certain transformations of
positive equations with a variable on the right-hand side.
The refinements are both of theoretical and practical interest.
For instance,
the second refinement is implemented in Setheo
and appears to be critical for that prover's
performance on equational problems.
The correctness of this variant of Brand's method was an open problem
that is solved by the more general results in the present paper.
The experimental results we obtained from a
prototype implementation of our proposed method for the model elimination prover
Protein also show some dramatic improvements of the proof search.
Ordering constraints have already been widely used in
equational theorem provers based on paramodulation.
We prove the correctness of our refinements
of Brand's method by establishing a suitable connection
to basic paramodulation calculi and
thereby shed new light on the connection
between different approaches to equational theorem proving.

HyperLinks / References / URLs:

\hgURL{~hg/pca.html#98CADE.1}



Download
Access Level:


Correlation

MPG Unit:

Max-Planck-Institut für Informatik



MPG Subunit:

Programming Logics Group

Audience:

experts only

Appearance:

MPII WWW Server, MPII FTP Server, MPG publications list, university publications list, working group publication list, Fachbeirat



BibTeX Entry:

@INPROCEEDINGS{BachmairGanzingerVoronkov-98-cade,
AUTHOR = {Bachmair, Leo and Ganzinger, Harald and Voronkov, Andrei},
EDITOR = {Kirchner, Claude and Kirchner, H{\'e}l{\`e}ne},
TITLE = {Elimination of Equality via Transformation with Ordering Constraints},
BOOKTITLE = {Proceedings of the 15th International Conference on Automated Deduction (CADE-98)},
PUBLISHER = {Springer},
YEAR = {1998},
VOLUME = {1421},
PAGES = {175--190},
SERIES = {Lecture Notes in Artificial Intelligence},
ADDRESS = {Lindau, Germany},
MONTH = {July},
ISBN = {3-540-64675-2},
}


Entry last modified by Uwe Brahm, 03/12/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)
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)
Andreas Nonnengart
Created
03/30/1999 03:50:53 PM
Revisions
5.
4.
3.
2.
1.
Editor(s)
Uwe Brahm
Christine Kiesel
Christine Kiesel
Uwe Brahm
Uwe Brahm
Edit Dates
04/14/99 07:01:52 PM
30/03/99 16:22:20
30/03/99 15:56:43
29.03.99 19:21:39
29.03.99 19:21:09