Intuitionistic Proof Transformations: Complexity and Applications
Uwe Egly, Stephan Schmitt · Electronic Notes in Theoretical Computer Science · 1998
We investigate a proof transformation from the multi-succedent calculus LJmc to Gentzen's single-succedent calculus LJ intuitionistic logic. We analyze the complexity of such a transformation and show that there exists no polynomial simulation between the cut-free versions of LJmc and CJ . Applications of proof transformations are motivated within constructive program synthesis systems since LJmc gives a basis for automated proof search whereas LJ is better suited for proof presentation and program construction from proofs. Well-known transformations from the literature are based on the cut-rule and suffer from the undesired consequence that the resulting program terms are not intuitive. We present a cut-free transformation of intuitionistic sequent proofs from LJmc to CJ based on permutation of inferences, and contrast its worst-case complexity with its effects on the quality of program terms.