Note: [] Address for correspondence: Wissensbasierte Systeme 184/3, TU Wien, Treitlstr. 3, A-1040 Wien, Austria
Note: [] This work was supported by the German Academic Exchange Service DAAD with a fellowship while the second author was a visiting scientist at Cornell University, Ithaca, NY, USA. Address for correspondence: FG Intellektik, FB Informatik, D-64283 Darmstadt, Germany
Abstract: We present a translation of intuitionistic sequent proofs from a multi-succedent calculus ℒ𝒥mc into a single-succedent calculus ℒ𝒥. 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 ℒ𝒥 cannot polynomially simulate ℒ𝒥mc (both without the cut rule), even in the prepositional fragment.
Keywords: Proof transformations, complexity, sequent calculi, program synthesis
