Document Open Access Logo

A Strictly Linear Subatomic Proof System

Authors Victoria Barrett , Alessio Guglielmi , Benjamin Ralph

PDF

File

Thumbnail PDF
PDF
LIPIcs.CSL.2025.39.pdf
  • Filesize: 0.8 MB
  • 22 pages

Document Identifiers

Subject Classification

ACM Subject Classification
  • Theory of computation → Proof theory
Keywords
  • Deep inference
  • Open deduction
  • Subatomic logic
  • Decision trees
  • Explicit substitutions
  • Cut elimination
  • Proof theory

Metrics

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

Abstract

We present a subatomic deep-inference proof system for a conservative extension of propositional classical logic with decision trees that is strictly linear. In a strictly linear subatomic system, a single linear rule shape subsumes not only the structural rules, such as contraction and weakening, but also the unit equality rules. An interpretation map from subatomic logic to propositional classical logic recovers the usual semantics and proof theoretic properties. By using explicit substitutions that indicate the substitution of one derivation into another, we are able to show that the unit-equality inference steps can be eliminated from a subatomic system for propositional classical logic with only a polynomial complexity cost in the size of the derivation, from which it follows that the system p-simulates Frege systems, and we show cut elimination for the resulting strictly linear system.

Cite As Get BibTex

Victoria Barrett, Alessio Guglielmi, and Benjamin Ralph. A Strictly Linear Subatomic Proof System. In 33rd EACSL Annual Conference on Computer Science Logic (CSL 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 326, pp. 39:1-39:22, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025) https://doi.org/10.4230/LIPIcs.CSL.2025.39

Author Details

Victoria Barrett
  • Department of Computer Science, University of Bath, UK
  • Inria Saclay, Palaiseau, France
Alessio Guglielmi
  • Department of Computer Science, University of Bath, UK
Benjamin Ralph
  • Department of Computer Science, University of Bath, UK

Funding

  • Barrett, Victoria: This work was supported by the Engineering and Physical Sciences Research Council [EP/R513155/1] and Inria Exploratory Action IMPROOF.

References

  1. Andrea Aler Tubella. A Study of Normalisation Through Subatomic Logic. PhD thesis, University of Bath, 2017. URL: https://people.bath.ac.uk/ag248/aat/phd.pdf.
  2. Andrea Aler Tubella and Alessio Guglielmi. Subatomic proof systems: Splittable systems. ACM Transactions on Computational Logic, 19(1):5:1-33, 2018. URL: https://doi.org/10.1145/3173544.
  3. Andrea Aler Tubella, Alessio Guglielmi, and Benjamin Ralph. Removing cycles from proofs. In Valentin Goranko and Mads Dam, editors, 26th EACSL Annual Conference on Computer Science Logic (CSL), volume 82 of Leibniz International Proceedings in Informatics (LIPIcs), pages 9:1-17. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2017. URL: https://doi.org/10.4230/LIPIcs.CSL.2017.9.
  4. Chris Barrett and Alessio Guglielmi. A subatomic proof system for decision trees. ACM Transactions on Computational Logic, 23(4):26:1-25, 2022. URL: https://doi.org/10.1145/3545116.
  5. Paola Bruscoli and Alessio Guglielmi. On the proof complexity of deep inference. ACM Transactions on Computational Logic, 10(2):14:1-34, 2009. URL: https://doi.org/10.1145/1462179.1462186.
  6. 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: https://doi.org/10.2168/LMCS-12(2:5)2016.
  7. Kai Brünnler. Two restrictions on contraction. Logic Journal of the IGPL, 11(5):525-529, 2003. URL: https://doi.org/10.1093/jigpal/11.5.525.
  8. Kai Brünnler. Locality for classical logic. Notre Dame Journal of Formal Logic, 47(4):557-580, 2006. URL: https://doi.org/10.1305/ndjfl/1168352668.
  9. Kai Brünnler and Alwen Fernanto Tiu. A local system for classical logic. In R. Nieuwenhuis and Andrei Voronkov, editors, Logic for Programming, Artificial Intelligence, and Reasoning (LPAR), volume 2250 of Lecture Notes in Computer Science, pages 347-361. Springer, 2001. URL: https://doi.org/10.1007/3-540-45653-8_24.
  10. Andrea Condoluci, Beniamino Accattoli, and Claudio Sacerdoti Coen. Sharing equality is linear. In Proceedings of the 21st International Symposium on Principles and Practice of Declarative Programming, PPDP '19, New York, NY, USA, 2019. Association for Computing Machinery. URL: https://doi.org/10.1145/3354166.3354174.
  11. Stephen A. Cook and Robert A. Reckhow. The relative efficiency of propositional proof systems. Journal of Symbolic Logic, 44(1):36-50, 1979. URL: https://doi.org/10.2307/2273702.
  12. Alessio Guglielmi. Formalism B, 2004. URL: https://people.bath.ac.uk/ag248/p/AG13.pdf.
  13. Alessio Guglielmi. A system of interaction and structure. ACM Transactions on Computational Logic, 8(1):1:1-64, 2007. URL: https://doi.org/10.1145/1182613.1182614.
  14. 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: https://doi.org/10.2168/LMCS-4(1:9)2008.
  15. Alessio Guglielmi, Tom Gundersen, and Lutz Straßburger. Breaking paths in atomic flows for classical logic. In Jean-Pierre Jouannaud, editor, 25th Annual IEEE Symposium on Logic in Computer Science (LICS), pages 284-293. IEEE, 2010. URL: https://doi.org/10.1109/LICS.2010.12.
  16. Tom Gundersen, Willem Heijltjes, and Michel Parigot. Atomic lambda calculus: A typed lambda-calculus with explicit sharing. In Orna Kupferman, editor, 28th Annual ACM/IEEE Symposium on Logic in Computer Science (LICS), pages 311-320. IEEE, 2013. URL: https://doi.org/10.1109/LICS.2013.37.
  17. M.S. Paterson and M.N. Wegman. Linear unification. Journal of Computer and System Sciences, 16(2):158-167, 1978. URL: https://doi.org/10.1016/0022-0000(78)90043-0.
  18. Alessio Santamaria. Towards a Godement calculus for dinatural transformations. PhD thesis, University of Bath, Somerset, UK, 2019. URL: https://ethos.bl.uk/OrderDetails.do?uin=uk.bl.ethos.787523.
  19. Lutz Straßburger. From deep inference to proof nets via cut elimination. Journal of Logic and Computation, 21(4):589-624, 2011. URL: https://doi.org/10.1093/logcom/exp047.
  20. Alwen Tiu. A system of interaction and structure II: The need for deep inference. Logical Methods in Computer Science, 2(2):4:1-24, 2006. URL: https://doi.org/10.2168/LMCS-2(2:4)2006.
Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail
© 2023-2025 Schloss Dagstuhl – LZI GmbH About DROPS Imprint Privacy Contact