Deutsch
 
Hilfe Datenschutzhinweis Impressum
  DetailsucheBrowse

Datensatz

DATENSATZ AKTIONENEXPORT
EndNote (UTF-8)
 
DownloadE-Mail
 Lokale TagsFreigabegeschichteDetailsÜbersicht
  Rewrite-based equational theorem proving with selection and simplification

Bachmair, L., & Ganzinger, H.(1991). Rewrite-based equational theorem proving with selection and simplification (MPI-I-91-208). Saarbrücken: Max-Planck-Institut für Informatik.

Item is

 

einblenden: alle

Basisdaten

ausblenden:
Datensatz-Permalink: https://hdl.handle.net/11858/00-001M-0000-0014-B13C-B Versions-Permalink: https://hdl.handle.net/11858/00-001M-0000-002D-9267-5
Genre: Bericht

Dateien

ausblenden: Dateien
:
MPI-I-91-208.pdf (beliebiger Volltext), 177KB
Öffnen   Speichern
Datei-Permalink:
https://hdl.handle.net/11858/00-001M-0000-0014-B17F-6
Name:
MPI-I-91-208.pdf
Beschreibung:
-
OA-Status:
Sichtbarkeit:
Öffentlich
MIME-Typ / Prüfsumme:
application/pdf / [MD5]
Technische Metadaten:
Öffnen
Copyright Datum:
-
Copyright Info:
-
Lizenz:
-

Externe Referenzen

einblenden:

Urheber

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

Inhalt

ausblenden:
Schlagwörter: -
 Zusammenfassung: We present various refutationally complete calculi for first-order clauses with equality that allow for arbitrary selection of negative atoms in clauses. Refutation completeness is established via the use of well-founded orderings on clauses for defining a Herbrand model for a consistent set of clauses. We also formulate an abstract notion of redundancy and show that the deletion of redundant clauses during the theorem proving process preserves refutation completeness. It is often possible to compute the closure of nontrivial sets of clauses under application of non-redundant inferences. The refutation of goals for such complete sets of clauses is simpler than for arbitrary sets of clauses, in particular one can restrict attention to proofs that have support from the goals without compromising refutation completeness. Additional syntactic properties allow to restrict the search space even further, as we demonstrate for so-called quasi-Horn clauses. The results in this paper contain as special cases or generalize many known results about Knuth-Bendix-like completion procedures (for equations, Horn clauses, and Horn clauses over built-in Booleans), completion of first-order clauses by clausal rewriting, and inductive theorem proving for Horn clauses.

Details

ausblenden:
Sprache(n): eng - English
 Datum: 1991
 Publikationsstatus: Erschienen
 Seiten: 24 p.
 Ort, Verlag, Ausgabe: Saarbrücken : Max-Planck-Institut für Informatik
 Inhaltsverzeichnis: -
 Art der Begutachtung: -
 Identifikatoren: Reportnr.: MPI-I-91-208
BibTex Citekey: BachmairGanzinger-91-mpii208
 Art des Abschluß: -

Veranstaltung

einblenden:

Entscheidung

einblenden:

Projektinformation

einblenden:

Quelle 1

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