Deutsch
 
Hilfe Datenschutzhinweis Impressum
  DetailsucheBrowse

Datensatz

DATENSATZ AKTIONENEXPORT

Freigegeben

Buchkapitel

Inductive Theorem Proving by Consistency for First‐order Clauses

MPG-Autoren
/persons/resource/persons44474

Ganzinger,  Harald
Programming Logics, MPI for Informatics, Max Planck Society;

/persons/resource/persons45567

Stuber,  Jürgen
Programming Logics, MPI for Informatics, Max Planck Society;

Externe Ressourcen
Es sind keine externen Ressourcen hinterlegt
Volltexte (beschränkter Zugriff)
Für Ihren IP-Bereich sind aktuell keine Volltexte freigegeben.
Volltexte (frei zugänglich)
Es sind keine frei zugänglichen Volltexte in PuRe verfügbar
Ergänzendes Material (frei zugänglich)
Es sind keine frei zugänglichen Ergänzenden Materialien verfügbar
Zitation

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.


Zitierlink: https://hdl.handle.net/11858/00-001M-0000-0023-C3AD-F
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.