English
 
Help Privacy Policy Disclaimer
  Advanced SearchBrowse

Item

ITEM ACTIONSEXPORT
Add to Basket
  Local TagsRelease HistoryDetailsSummary

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;

External Resource
No external resources are shared
Fulltext (restricted access)
There are currently no full texts shared for your IP range.
Fulltext (public)
There are no public fulltexts stored in PuRe
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: https://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.