TY - GEN
T1 - Breaking paths in atomic flows for classical logic
AU - Guglielmi, Alessio
AU - Gundersen, Tom
AU - Straburger, Lutz
PY - 2010/7
Y1 - 2010/7
N2 - 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-dimensional-diagram exposition of atomic flows, which helps us to connect atomic flows with other known formalisms.
AB - 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-dimensional-diagram exposition of atomic flows, which helps us to connect atomic flows with other known formalisms.
UR - http://www.scopus.com/inward/record.url?scp=78449276753&partnerID=8YFLogxK
UR - http://dx.doi.org/10.1109/LICS.2010.12
U2 - 10.1109/LICS.2010.12
DO - 10.1109/LICS.2010.12
M3 - Chapter in a published conference proceeding
SN - 9781424475889
T3 - Proceedings - Symposium on Logic in Computer Science
SP - 284
EP - 293
BT - 2010 25th Annual IEEE Symposium on Logic in Computer Science, LICS
PB - IEEE
T2 - 25th Annual IEEE Symposium on Logic in Computer Science, LICS 2010, July 11, 2010 - July 14, 2010
Y2 - 1 July 2010
ER -