Document Open Access Logo

Removing Cycles from Proofs

Authors Andrea Aler Tubella, Alessio Guglielmi, Benjamin Ralph

Thumbnail PDF


  • Filesize: 0.54 MB
  • 17 pages

Document Identifiers

Author Details

Andrea Aler Tubella
Alessio Guglielmi
Benjamin Ralph

Cite AsGet 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)


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.
  • proof theory
  • deep inference
  • proof complexity


  • Access Statistics
  • Total Accesses (updated on a weekly basis)
    PDF Downloads


  1. Paola Bruscoli and Alessio Guglielmi. On the proof complexity of deep inference. ACM Transactions on Computational Logic (TOCL), 10(2):14, 2009. URL:
  2. 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:
  3. 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:
  4. Samuel R. Buss. The undecidability of k-provability. Annals of Pure and Applied Logic, 53(1):75-102, 1991. URL:
  5. Samuel R. Buss. Some remarks on lengths of propositional proofs. Archive for Mathematical Logic, 34(6):377-394, 1995. URL:
  6. Alessandra Carbone. The cost of a cycle is a square. The Journal of Symbolic Logic, 67(01):35-60, 2002. URL:
  7. 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:
  8. 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:
  9. 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:
  10. 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:
  11. Tom Erik Gundersen. A general view of normalisation through atomic flows. Thesis, University of Bath, 2009. URL:
  12. Emil Jeřábek. Proof complexity of the cut-free calculus of structures. Journal of Logic and Computation, 19(2):323-339, 2008. URL:
  13. Andrea Aler Tubella. A study of normalisation through subatomic logic. Thesis, University of Bath, 2017. URL:
Questions / Remarks / Feedback

Feedback for Dagstuhl Publishing

Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail