Skip to main content
PRL Project

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.