Matrixbased Constructive Theorem Proving.


Christoph Kreitz, Jens Otten, Stephan Schmitt, Brigitte Pientka.  
In S. Hölldobler, ed., Intellectics and Computational Logic  Papers in honor of Wolfgang Bibel, Applied Logic Series 19, pages 189205, Kluwer, 2000. 

Abstract 

Bibel's connection method, originally developed for classical logic,
has been extended to a variety of nonclassical logics and used to
control the creation of sequent proofs for interactive proof
assistants. Matrix methods for intuitionistic logic also are the
central inference engine for program synthesis and verification. We
present a coherent account of matrix methods for constructive
theorem proving and show how to extend them to inductive theorem
proving by integrating rippling techniques into the unification
process.

Also available:
Prologue
(PS
/ PDF)
and Epilogue (PS / PDF) to the book The PDF quality is not very good because a gothic font is used 
Back to overview of papers 

Bibtex Entry 

@InCollection{inc:Kreitz+00a, author = "Christoph Kreitz and Jens Otten and Stephan Schmitt and Brigitte Pientka", title = "Matrixbased Constructive Theorem Proving", booktitle = "Intellectics and Computational Logic. Papers in honor of Wolfgang Bibel", publisher = "Kluwer", year = "2000", editor = "Steffen H{\"o}lldobler", number = "19", series = "Applied Logic Series", pages = "189205" } 