Breaking Paths in Atomic Flows for Classical Logic

This work belongs to a wider effort aimed at eliminating syntactic bureaucracy from proof systems. In this paper, we present a novel cut elimination procedure for classical propositional logic. It is based on the recently introduced atomic flows: they are purely graphical devices that abstract away from much of the typical bureaucracy of proofs. We make crucial use of the path breaker, an atomic-flow construction that avoids some nasty termination problems, and that can be used in any proof system with sufficient symmetry. This paper contains an original 2-dimensionaldiagram exposition of atomic flows, which helps us to connect atomic flows with other known formalisms.

• Type: Journal
• Year: 2010
• Where: LICS
• Authors: Alessio Guglielmi, Tom Gundersen, Lutz Straßburger
• Keywords: Atomic flows, Automated Reasoning, Classical Propositional Logic, LICS 2010, Nasty Termination Problems