### Abstract

Language | English |
---|---|

Title of host publication | 2010 25th Annual IEEE Symposium on Logic in Computer Science, LICS |

Publisher | IEEE |

Pages | 284-293 |

Number of pages | 10 |

ISBN (Electronic) | 9781424475896 |

ISBN (Print) | 9781424475889 |

DOIs | |

Status | Published - Jul 2010 |

Event | 25th 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

Name | Proceedings - Symposium on Logic in Computer Science |
---|---|

ISSN (Print) | 1043-6871 |

### Conference

Conference | 25th Annual IEEE Symposium on Logic in Computer Science, LICS 2010, July 11, 2010 - July 14, 2010 |
---|---|

Country | UK United Kingdom |

City | Edinburgh |

Period | 1/07/10 → … |

### Fingerprint

### Cite this

*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.

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution

*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

}

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 -