Intuitionistic Tableau Extracted

unofficial copies [PDF], [PS]


by James L. Caldwell

Proceedings of International Conference on Automated Reasoning with Analytic Tableaux and Related Methods (TABLEAUX'99), LNAI 1617, pp. 82-96, Springer-Verlag, 1999.

Abstract

This paper presents a formalization of a sequent presentation of intuitionisitic propositional logic and proof of decidability. The proof is implemented in the Nuprl system and the resulting proof object yields a "correct-by-construction" program for deciding intuitionisitc propositional sequents. The extracted program turns out to be an implementation of the tableau algorithm. If the argument to the resulting decision procedure is a valid sequent, a formal proof of that fact is returned, otherwise a counter-example in the form of a Kripke Countermodel is returned. The formalization roughly follows Aitken, Constable, and Underwood's presentation in but a number of adjustments and corrections have been made to ensure the extracted program is clean (no non-computational junk) and efficient.