Deutsch
 
Hilfe Datenschutzhinweis Impressum
  DetailsucheBrowse

Datensatz

 
 
DownloadE-Mail
  Inductive Theorem Proving by Consistency for First‐order Clauses

Ganzinger, H., & Stuber, J. (1992). Inductive Theorem Proving by Consistency for First‐order Clauses. In J. Buchmann, H. Ganzinger, & W. J. Paul (Eds.), Informatik - Festschrift zum 60. Geburtstag von Günter Hotz (pp. 441-462). Wiesbaden: Teubner.

Item is

Externe Referenzen

einblenden:

Urheber

einblenden:
ausblenden:
 Urheber:
Ganzinger, Harald1, Autor           
Stuber, Jürgen1, Autor           
Affiliations:
1Programming Logics, MPI for Informatics, Max Planck Society, ou_40045              

Inhalt

einblenden:
ausblenden:
Schlagwörter: -
 Zusammenfassung: We show how the method of proof by consistency can be extended to proving \u000Aproperties of the perfect model of a set of first‐order clauses with equality. \u000ATechnically proofs by consistency will be similar to proofs by case analysis \u000Aover the term structure. As our method also allows to prove \u000Asufficient‐completeness of function definitions in parallel with proving an \u000Ainductive theorem we need not distinguish between constructors and defined \u000Afunctions. Our method is linear and refutationally complete with respect to the \u000Aperfect model, it supports lemmas in a natural way, and it provides for \u000Apowerful simplification and elimination techniques.

Details

einblenden:
ausblenden:
Sprache(n): eng - English
 Datum: 1992
 Publikationsstatus: Erschienen
 Seiten: -
 Ort, Verlag, Ausgabe: -
 Inhaltsverzeichnis: -
 Art der Begutachtung: -
 Identifikatoren: BibTex Citekey: GanzingerStuber-92
 Art des Abschluß: -

Veranstaltung

einblenden:

Entscheidung

einblenden:

Projektinformation

einblenden:

Quelle 1

einblenden:
ausblenden:
Titel: Informatik - Festschrift zum 60. Geburtstag von Günter Hotz
  Latex : Informatik ‐- {Festschrift zum 60. Geburtstag von Günter Hotz}
Genre der Quelle: Buch
 Urheber:
Buchmann, J.1, Herausgeber
Ganzinger, Harald2, Herausgeber           
Paul, W. J.1, Herausgeber
Affiliations:
1 External Organizations, ou_persistent22            
2 Programming Logics, MPI for Informatics, Max Planck Society, ou_40045            
Ort, Verlag, Ausgabe: Wiesbaden : Teubner
Seiten: - Band / Heft: - Artikelnummer: - Start- / Endseite: 441 - 462 Identifikator: -