Breaking paths in atomic flows for classical logic

Alessio Guglielmi, Tom Gundersen, Lutz Straburger

Research output: Chapter in Book/Report/Conference proceedingConference contribution

  • 12 Citations

Abstract

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.
LanguageEnglish
Title of host publication2010 25th Annual IEEE Symposium on Logic in Computer Science, LICS
PublisherIEEE
Pages284-293
Number of pages10
ISBN (Electronic)9781424475896
ISBN (Print)9781424475889
DOIs
StatusPublished - Jul 2010
Event25th Annual IEEE Symposium on Logic in Computer Science, LICS 2010, July 11, 2010 - July 14, 2010 - Edinburgh, UK United Kingdom
Duration: 1 Jul 2010 → …

Publication series

NameProceedings - Symposium on Logic in Computer Science
ISSN (Print)1043-6871

Conference

Conference25th Annual IEEE Symposium on Logic in Computer Science, LICS 2010, July 11, 2010 - July 14, 2010
CountryUK United Kingdom
CityEdinburgh
Period1/07/10 → …

Fingerprint

logic
circuit breakers
elimination
diagrams
symmetry

Cite this

Guglielmi, A., Gundersen, T., & Straburger, L. (2010). Breaking paths in atomic flows for classical logic. In 2010 25th Annual IEEE Symposium on Logic in Computer Science, LICS (pp. 284-293). (Proceedings - Symposium on Logic in Computer Science). IEEE. DOI: 10.1109/LICS.2010.12

Breaking paths in atomic flows for classical logic. / Guglielmi, Alessio; Gundersen, Tom; Straburger, Lutz.

2010 25th Annual IEEE Symposium on Logic in Computer Science, LICS . IEEE, 2010. p. 284-293 (Proceedings - Symposium on Logic in Computer Science).

Research output: Chapter in Book/Report/Conference proceedingConference contribution

Guglielmi, A, Gundersen, T & Straburger, L 2010, Breaking paths in atomic flows for classical logic. in 2010 25th Annual IEEE Symposium on Logic in Computer Science, LICS . Proceedings - Symposium on Logic in Computer Science, IEEE, pp. 284-293, 25th Annual IEEE Symposium on Logic in Computer Science, LICS 2010, July 11, 2010 - July 14, 2010, Edinburgh, UK United Kingdom, 1/07/10. DOI: 10.1109/LICS.2010.12
Guglielmi A, Gundersen T, Straburger L. Breaking paths in atomic flows for classical logic. In 2010 25th Annual IEEE Symposium on Logic in Computer Science, LICS . IEEE. 2010. p. 284-293. (Proceedings - Symposium on Logic in Computer Science). Available from, DOI: 10.1109/LICS.2010.12
Guglielmi, Alessio ; Gundersen, Tom ; Straburger, Lutz. / Breaking paths in atomic flows for classical logic. 2010 25th Annual IEEE Symposium on Logic in Computer Science, LICS . IEEE, 2010. pp. 284-293 (Proceedings - Symposium on Logic in Computer Science).
@inproceedings{f859cc9c4308438497ae15a17bfd1291,
title = "Breaking paths in atomic flows for classical logic",
abstract = "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.",
author = "Alessio Guglielmi and Tom Gundersen and Lutz Straburger",
year = "2010",
month = "7",
doi = "10.1109/LICS.2010.12",
language = "English",
isbn = "9781424475889",
series = "Proceedings - Symposium on Logic in Computer Science",
publisher = "IEEE",
pages = "284--293",
booktitle = "2010 25th Annual IEEE Symposium on Logic in Computer Science, LICS",
address = "USA United States",

}

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 - Conference contribution

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

ER -