The Cut-Elimination System CERES

Examples

To make yourself familiar with the system CERES and the additional tools we have prepared the following examples:

Simple Proofs:
Very simple examples just to get a glimpse of how cut-elimination is done with CERES and how the workflow with the auxiliary tools molds.
An Exponential Example:
Instances of a proof schema which gives exponential cut-free proves. These examples clearly justify and suggest the use of computer aided cut-elimination systems.
The Tape Proof:
A convenient sized proof of a simple but practical mathematical statement.
The Lattice Proof:
A larger proof of a still simple but more practical mathematical statement.
Fürstenberg's Prime Proof:
A huge formal proof of a significant number-theoretical mathematical statement with a complex indirect topological proof.
The Prime-Divisor Proof:
A second-order proof, showing that the least number principle implies the fact that every number greater than 1 has a prime divisor.