KnowledgeBase » SEMINAR » ID = 506

On Intuitionistic Proof Transformations and their Application to Constructive Program Synthesis

by Uwe Egly
1998-1999

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.