Guglielmi, Alessio ;
Gundersen, Tom ;
Parigot, Michel
A Proof Calculus Which Reduces Syntactic Bureaucracy
Abstract
In usual proof systems, like the sequent calculus, only a very limited way of combining proofs is available through the tree structure. We present in this paper a logicindependent proof calculus, where proofs can be freely composed by connectives, and prove its basic properties. The main advantage of this proof calculus is that it allows to avoid certain types of syntactic bureaucracy inherent to all usual proof systems, in particular the sequent calculus. Proofs in this system closely reflect their atomic flow, which traces the behaviour of atoms through structural rules. The general definition is illustrated by the standard deepinference system for propositional logic, for which there are known rewriting techniques that achieve cut elimination based only on the information in atomic flows.
BibTeX  Entry
@InProceedings{guglielmi_et_al:LIPIcs:2010:2649,
author = {Alessio Guglielmi and Tom Gundersen and Michel Parigot},
title = {{A Proof Calculus Which Reduces Syntactic Bureaucracy}},
booktitle = {Proceedings of the 21st International Conference on Rewriting Techniques and Applications},
pages = {135150},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {9783939897187},
ISSN = {18688969},
year = {2010},
volume = {6},
editor = {Christopher Lynch},
publisher = {Schloss DagstuhlLeibnizZentrum fuer Informatik},
address = {Dagstuhl, Germany},
URL = {http://drops.dagstuhl.de/opus/volltexte/2010/2649},
URN = {urn:nbn:de:0030drops26490},
doi = {http://dx.doi.org/10.4230/LIPIcs.RTA.2010.135},
annote = {Keywords: Logic, Proof theory, Deep Inference, Flow graphs, Proof Systems, Open Deduction, Rewriting, Confluence, Termination}
}
2010
Keywords: 

Logic, Proof theory, Deep Inference, Flow graphs, Proof Systems, Open Deduction, Rewriting, Confluence, Termination 
Seminar: 

Proceedings of the 21st International Conference on Rewriting Techniques and Applications

Related Scholarly Article: 


Issue date: 

2010 
Date of publication: 

2010 