English
 
User Manual Privacy Policy Disclaimer Contact us
  Advanced SearchBrowse

Item

ITEM ACTIONSEXPORT

Released

Book Chapter

Inductive Theorem Proving by Consistency for First‐order Clauses

MPS-Authors
/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;

Locator
There are no locators available
Fulltext (public)
There are no public fulltexts available
Supplementary Material (public)
There is no public supplementary material available
Citation

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.


Cite as: http://hdl.handle.net/11858/00-001M-0000-0023-C3AD-F
Abstract
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.