HLK ProofTool
TU Vienna logic.at Theory and Logic Group (E185-2)

An Exponential Example

In "Cut Normal Forms and Proof Complexity" Matthias Baaz and Alexander Leitsch investigated a schema of proofs of the sequents where denotes the transitivity of , i.e. . Note that all cut-free proofs of are of length .

Note that, due to their sizes, some of the following files are compressed (gziped). We recommend you leave them compressed since uncompressing would yield files of tremendous sizes (more then 1 GB in some cases). Besides the system CERES and all our tools are also capable of working with gziped files directly.