A theory of cut-restriction: first steps

Agata Ciabattoni, Timo Lang, Revantha Ramanayake

Cut-elimination is the bedrock of proof theory. It is the algorithm that eliminates cuts from a sequent calculus proof that leads to cut-free calculi and applications. Cut-eliminat…