## Tableau for Intuitionistic Predicate Logic as Metatheory

**Judith Underwood**
*Abstract:* We show how the tableau procedure for
intuitionistic predicate logic can be interpreted as the
computational content of a metatheorem about Kripke models for the
logic. The metatheory we use is based on constructive type theory,
but we shall explore classical extensions to the theory. We begin
by describing how infinite tableau developments may be represented
as co-inductive types in such a theory. We then show how a bounded
tableau search procedure can be interpreted as the computational
content of a theorem about prefixes of (possibly infinite) Kripke
countermodels. Next, we examine how classical reasoning may be
introduced in the proof without affecting the computational
content. This leads to a stronger theorem with the same bounded
tableau search as its computational content. Finally, we discuss
the unbounded tableau procedure as the computational content of a
related theorem.

*LFCS report ECS-LFCS-95-321,
February 1995.*

Previous |

Index |

Next