Expansion Trees with Cut

Federico Aschieri, Stefan Hetzl, Daniel Weller

Herbrand's theorem is one of the most fundamental insights in logic. From the syntactic point of view, it suggests a compact representation of proofs in classical first- and higher…