Deutsch
 
Hilfe Datenschutzhinweis Impressum
  DetailsucheBrowse

Datensatz

DATENSATZ AKTIONENEXPORT
Zur Ablage hinzufügen
 Lokale TagsFreigabegeschichteDetailsÜbersicht
  Completion of First-order Clauses with Equality by Strict Superposition

Bachmair, L., & Ganzinger, H. (1991). Completion of First-order Clauses with Equality by Strict Superposition. In S. Kaplan, & M. Okada (Eds.), Conditional and Typed Rewriting Systems (pp. 162-180). Berlin: Springer.

Item is

 

einblenden: alle ausblenden: alle

Basisdaten

einblenden: ausblenden:
Datensatz-Permalink: https://hdl.handle.net/11858/00-001M-0000-001A-253B-F Versions-Permalink: https://hdl.handle.net/21.11116/0000-000E-0626-1
Genre: Konferenzbeitrag

Externe Referenzen

einblenden:
ausblenden:
externe Referenz:
https://rdcu.be/ds6ER (Verlagsversion)
Beschreibung:
-
OA-Status:
Keine Angabe

Urheber

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

Inhalt

einblenden:
ausblenden:
Schlagwörter: -
 Zusammenfassung: We have previously shown that strict superposition together with merging
paramodulation is refutationally complete for first-order clauses with
equality. This paper improves these results by considering a more powerful
framework for simplification and elimination of clauses. The framework gives
general criteria under which simplification and elimination do not destroy the
refutation completeness of the superposition calculus. One application is a
proof of the refutation completeness for alternative superposition strategies
with arbitrary selection functions for negative literals. With these powerful
simplification mechanisms it is often possible to compute the closure of
nontrivial sets of clauses under superposition in a finite number of steps.
Refutation or solving of \em goals\/} for such closed or {\em complete\/ sets
of clauses is simpler than for arbitrary sets of clauses. The results in this
paper contain as special cases or generalize many known results about about
ordered Knuth-Bendix-like completion of equations, of Horn clauses, of Horn
clauses over built-in Booleans, about completion of first-order clauses by
clausal rewriting, and inductive theorem proving for Horn clauses.

Details

einblenden:
ausblenden:
Sprache(n): eng - English
 Datum: 1991
 Publikationsstatus: Erschienen
 Seiten: -
 Ort, Verlag, Ausgabe: -
 Inhaltsverzeichnis: -
 Art der Begutachtung: -
 Identifikatoren: BibTex Citekey: BachmairGanzinger-91-ctrs
DOI: 10.1007/3-540-54317-1_89
 Art des Abschluß: -

Veranstaltung

einblenden:
ausblenden:
Titel: International Workshop on Conditional and Typed Rewriting
Veranstaltungsort: Montreal, Canada
Start-/Enddatum: -

Entscheidung

einblenden:

Projektinformation

einblenden:

Quelle 1

einblenden:
ausblenden:
Titel: Conditional and Typed Rewriting Systems
  Untertitel : 2nd International CTRS Workshop Montreal, Canada, June 11–14, 1990 Proceedings
  Kurztitel : CTRS 1990
Genre der Quelle: Konferenzband
 Urheber:
Kaplan, St.1, Herausgeber
Okada, M.1, Herausgeber
Affiliations:
1 External Organizations, ou_persistent22            
Ort, Verlag, Ausgabe: Berlin : Springer
Seiten: - Band / Heft: - Artikelnummer: - Start- / Endseite: 162 - 180 Identifikator: -

Quelle 2

einblenden:
ausblenden:
Titel: Lecture Notes in Computer Science
  Kurztitel : LNCS
Genre der Quelle: Reihe
 Urheber:
Affiliations:
Ort, Verlag, Ausgabe: -
Seiten: - Band / Heft: 516 Artikelnummer: - Start- / Endseite: - Identifikator: -