PRL Seminars

We show how efficient proof search procedures can be used to automate first-order proof construction within the NuPRL system.

The talk consists of three parts:

1. We give a program demonstration of implemented complete, sound, and fully automated theorem provers for first-order intuitionistic logic. These programs are able to find "compact proofs" of valid formulae even in cases where NuPRL's current automatic proof tactics cannot find a proof.
2. The theoretical background of the used proof methods will be explained. Beside the usual term unification (already used in theorem provers for classical logic) we need an additional specialised string unification to express the particular properties of intuitionistic logic.
3. In the last part we explain how a NuPRL sequent proof can be reconstructed from the compact representation of an automatically generated proof. We discuss the problem of avoiding any additional search during the reconstruction process as well the relevant properties of proof transformations with respect to proof complexity and program terms.