Deutsch
 
Hilfe Datenschutzhinweis Impressum
  DetailsucheBrowse

Datensatz

DATENSATZ AKTIONENEXPORT
  Elimination of equality via transformation with ordering constraints

Bachmair, L., Ganzinger, H., & Voronkov, A.(1997). Elimination of equality via transformation with ordering constraints (MPI-I-1997-2-012). Saarbrücken: Max-Planck-Institut für Informatik.

Item is

Dateien

einblenden: Dateien
ausblenden: Dateien
:
1997-2-012 (beliebiger Volltext), 11KB
Name:
1997-2-012
Beschreibung:
-
OA-Status:
Sichtbarkeit:
Öffentlich
MIME-Typ / Prüfsumme:
text/html / [MD5]
Technische Metadaten:
Copyright Datum:
-
Copyright Info:
-
Lizenz:
-

Externe Referenzen

einblenden:

Urheber

einblenden:
ausblenden:
 Urheber:
Bachmair, Leo1, Autor           
Ganzinger, Harald1, Autor           
Voronkov, Andrei1, Autor           
Affiliations:
1Programming Logics, MPI for Informatics, Max Planck Society, ou_40045              

Inhalt

einblenden:
ausblenden:
Schlagwörter: -
 Zusammenfassung: We refine Brand's method for eliminating equality axioms by (i) imposingeordering 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.

Details

einblenden:
ausblenden:
Sprache(n): eng - English
 Datum: 1997
 Publikationsstatus: Erschienen
 Seiten: 18 p.
 Ort, Verlag, Ausgabe: Saarbrücken : Max-Planck-Institut für Informatik
 Inhaltsverzeichnis: -
 Art der Begutachtung: -
 Identifikatoren: URI: http://domino.mpi-inf.mpg.de/internet/reports.nsf/NumberView/1997-2-012
Reportnr.: MPI-I-1997-2-012
BibTex Citekey: BachmairGanzingerVoronkov97
 Art des Abschluß: -

Veranstaltung

einblenden:

Entscheidung

einblenden:

Projektinformation

einblenden:

Quelle 1

einblenden:
ausblenden:
Titel: Research Report / Max-Planck-Institut für Informatik
Genre der Quelle: Reihe
 Urheber:
Affiliations:
Ort, Verlag, Ausgabe: -
Seiten: - Band / Heft: - Artikelnummer: - Start- / Endseite: - Identifikator: -