# * A Constructive Completeness Proof for the Intuitionistic Propositional Calculus *

## by Judith Underwood

1990

- Tech Report TR90-1179 http://hdl.handle.net/1813/7019
- unofficial copies PDF, PS

**Abstract**

This paper presents a constructive proof of completeness of Kripke models for the intuitionistic propositional calculus. The computational content of the proof is a form of the tableau decision procedure. If a formula is valid, the algorithm produces a proof of the formula in the form of an inhabitant of the corresponding type; if not, it produces a Kripke model and a state in the model such that the formula is not forced at that state in that model.

**bibTex ref: Und90**

cite link