Analysis of Clause set Schema Aided by Automated Theorem Proving: A Case Study [Extended Paper]

David Cerna, Alexander Leitsch

The schematic CERES method [8] is a recently developed method of cut elimination for proof schemata, that is a sequence of proofs with a recursive construction. Proof schemata can…