# Intellectics Group: Technical Report 99-02

## On Intuitionistic Proof Transformations, their
Complexity, and Application to Constructive Program Synthesis

### Uwe Egly and Stephan Schmitt

We present a translation of intuitionistic sequent proofs from a
multi-succedent calculus LJmc into a single-succedent calculus LJ. The
former gives a basis for automated proof search whereas the latter is
better suited for proof presentation and program construction from
proofs in a system for constructive program synthesis. Well-known
translations from the literature have a severe drawback; they use cuts
in order to establish the transformation with the undesired
consequence that the resulting program term is not intuitive. We
establish a transformation based on permutation of inferences and
discuss the relevant properties with respect to proof complexity and
program terms. As an important result we show that LJ cannot
polynomially simulate LJmc (both without the cut rule), even in the
propositional fragment.