Sciweavers

Share
LICS
2010
IEEE

Breaking Paths in Atomic Flows for Classical Logic

8 years 3 months ago
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.
Alessio Guglielmi, Tom Gundersen, Lutz Straß
Added 29 Jan 2011
Updated 29 Jan 2011
Type Journal
Year 2010
Where LICS
Authors Alessio Guglielmi, Tom Gundersen, Lutz Straßburger
Comments (0)
books