Matrix-based Constructive Theorem Proving

unofficial copies [PDF], [PS]


by Christoph Kreitz, Jens Otten, Stephan Schmitt, and Brigitte Pientka

Intellectics and Computational Logic: Papers in honor of Wolfgang Bibel, S. Hölldobler (ed.), pp. 189-205, Kluwer, 2000.

Abstract

Bibel's connection method, originally developed for classical logic, has been extended to a variety of non-classical 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.