Recent searches
Search options
Is there something like a framework for cut elimination?
As far as I know, to design a system that admits cut you need (1) deep intuition, and (2) to write some of the worst proofs ever conceived
Is there some kind of metatheory for designing proof systems that have "cut elimination by construction"?
@julesh I think that canonical calculi by Arnon Avron, Anna Zamansky, and others provide one answer. I used one of these in my masters thesis.