Efficient Automated Proof Search and Proof Reconstruction in Intuitionistic Logic
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:
- 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.
- 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
- 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.