LIPIcs.CSL.2017.9.pdf
- Filesize: 0.54 MB
- 17 pages
Document
Removing Cycles from Proofs
Authors
-
Part of:
Volume:
26th EACSL Annual Conference on Computer Science Logic (CSL 2017)
Series: Leibniz International Proceedings in Informatics (LIPIcs)
Conference: Computer Science Logic (CSL) - License:
Creative Commons Attribution 3.0 Unported license
- Publication Date: 2017-08-16
Cite As Get BibTex
Andrea Aler Tubella, Alessio Guglielmi, and Benjamin Ralph. Removing Cycles from Proofs. In 26th EACSL Annual Conference on Computer Science Logic (CSL 2017). Leibniz International Proceedings in Informatics (LIPIcs), Volume 82, pp. 9:1-9:17, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2017)
https://doi.org/10.4230/LIPIcs.CSL.2017.9
Abstract
If we track atom occurrences in classical propositional proofs in deep inference, we see that they can form cyclic structures between cuts and identity steps. These cycles are an obstacle to a very natural form of normalisation, that simply unfolds all the contractions in a proof. This mechanism, which we call ‘decomposition’, has many points of contact with explicit substitutions in lambda calculi. In the presence of cycles, decomposition does not terminate, and this is an obvious drawback if we want to interpret proofs computationally. One way of eliminating cycles is eliminating cuts. However, we could ask ourselves whether it is possible to eliminate cycles independently of (general) cut elimination. This paper shows an efficient way to do so, therefore establishing the independence of decomposition from cut elimination. In other words, cut elimination in propositional logic can be separated into three separate procedures: 1) cycle elimination, 2) unfolding of contractions, 3) elimination of cuts in the linear fragment.
Subject Classification
Keywords
- proof theory
- deep inference
- proof complexity
Metrics
- Access Statistics
-
Total Accesses (updated on a weekly basis)
0PDF Downloads
References
- Paola Bruscoli and Alessio Guglielmi. On the proof complexity of deep inference. ACM Transactions on Computational Logic (TOCL), 10(2):14, 2009. URL: http://dx.doi.org/10.1145/1462179.1462186.
- Paola Bruscoli, Alessio Guglielmi, Tom Gundersen, and Michel Parigot. Quasipolynomial normalisation in deep inference via atomic flows and threshold formulae. Logical Methods in Computer Science, 12(1):5:1-30, 2016. URL: http://dx.doi.org/10.2168/LMCS-12(2:5)2016.
- Kai Brünnler and Alwen Fernanto Tiu. A local system for classical logic. In Logic for Programming, Artificial Intelligence, and Reasoning, volume 2250, pages 347-361. Springer, 2001. URL: http://dx.doi.org/10.1007/3-540-45653-8_24.
- Samuel R. Buss. The undecidability of k-provability. Annals of Pure and Applied Logic, 53(1):75-102, 1991. URL: http://dx.doi.org/10.1016/0168-0072(91)90059-U.
- Samuel R. Buss. Some remarks on lengths of propositional proofs. Archive for Mathematical Logic, 34(6):377-394, 1995. URL: http://dx.doi.org/10.1007/BF02391554.
- Alessandra Carbone. The cost of a cycle is a square. The Journal of Symbolic Logic, 67(01):35-60, 2002. URL: http://dx.doi.org/10.2178/jsl/1190150028.
- Anupam Das. On the relative proof complexity of deep inference via atomic flows. Logical Methods in Computer Science, 11(1):4:1-27, 2015. URL: http://dx.doi.org/10.2168/LMCS-11(1:4)2015.
- Alessio Guglielmi and Tom Gundersen. Normalisation control in deep inference via atomic flows. Logical Methods in Computer Science, 4(1):9:1-36, 2008. URL: http://dx.doi.org/10.2168/LMCS-4(1:9)2008.
- Alessio Guglielmi, Tom Gundersen, and Michel Parigot. A proof calculus which reduces syntactic bureaucracy. In 21st International Conference on Rewriting Techniques and Applications (RTA), volume 6 of Leibniz International Proceedings in Informatics (LIPIcs), pages 135-150. Schloss Dagstuhl-Leibniz-Zentrum für Informatik, 2010. URL: http://dx.doi.org/10.4230/LIPIcs.RTA.2010.135.
- Alessio Guglielmi, Tom Gundersen, and Lutz Straßburger. Breaking paths in atomic flows for classical logic. In Logic in Computer Science (LICS), 2010 25th Annual IEEE Symposium on, pages 284-293. IEEE, 2010. URL: http://dx.doi.org/10.1109/LICS.2010.12.
- Tom Erik Gundersen. A general view of normalisation through atomic flows. Thesis, University of Bath, 2009. URL: https://tel.archives-ouvertes.fr/file/index/docid/509241/filename/thesis.pdf.
- Emil Jeřábek. Proof complexity of the cut-free calculus of structures. Journal of Logic and Computation, 19(2):323-339, 2008. URL: http://dx.doi.org/10.1093/logcom/exn054.
- Andrea Aler Tubella. A study of normalisation through subatomic logic. Thesis, University of Bath, 2017. URL: https://arxiv.org/pdf/1703.10258.pdf.