On Intuitionistic Proof Transformations, their Complexity, and Application to Constructive Program Synthesis
Uwe Egly, Stephan Schmitt ยท Fundamenta Informaticae ยท 1999
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 p