On Intuitionistic Proof Transformations and their Application to Constructive Program Synthesis
by Uwe Egly
Visitor from Technische Universitaet Wien
This is joint work with Stephan Schmitt.
We present translations of first-order intuitionistic sequent proofs from a multi-succedent calculus LJmc into NuPRL's single-succedent calculus LJ. LJmc gives a basis for automated theorem proving whereas LJ is used for constructive program synthesis within NuPRL.
Well-known translations using the cut-rule have the severe drawback that the resulting program terms are not intuitive.
We establish a cut-free transformation based on permutation of inferences which preserves the original sub-specification wrt.the resulting program term.
This translation suffers form the suprising result that NuPRL's calculus LJ (without the cut-rule) cannot polyno- mially simulate LJmc.
We present some improvements of our translation by providing a more controlled introduction of the cut-rule during the translation process. This yields an at most polynomial increase of proof length AND preserves the intended specification within the program term.