Document

# New Minimal Linear Inferences in Boolean Logic Independent of Switch and Medial

## File

LIPIcs.FSCD.2021.14.pdf
• Filesize: 0.85 MB
• 19 pages

## Acknowledgements

The authors would like to thank Lutz Strassburger, Ross Horne and Matteo Acclavio for several interesting discussions surrounding this work. We are also grateful to the anonymous reviewers for their valuable feedback and suggestions.

## Cite As

Anupam Das and Alex A. Rice. New Minimal Linear Inferences in Boolean Logic Independent of Switch and Medial. In 6th International Conference on Formal Structures for Computation and Deduction (FSCD 2021). Leibniz International Proceedings in Informatics (LIPIcs), Volume 195, pp. 14:1-14:19, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2021)
https://doi.org/10.4230/LIPIcs.FSCD.2021.14

## Abstract

A linear inference is a valid inequality of Boolean algebra in which each variable occurs at most once on each side. Equivalently, it is a linear rewrite rule on Boolean terms that constitutes a valid implication. Linear inferences have played a significant role in structural proof theory, in particular in models of substructural logics and in normalisation arguments for deep inference proof systems. Systems of linear logic and, later, deep inference are founded upon two particular linear inferences, switch : x ∧ (y ∨ z) → (x ∧ y) ∨ z, and medial : (w ∧ x) ∨ (y ∧ z) → (w ∨ y) ∧ (x ∨ z). It is well-known that these two are not enough to derive all linear inferences (even modulo all valid linear equations), but beyond this little more is known about the structure of linear inferences in general. In particular despite recurring attention in the literature, the smallest linear inference not derivable under switch and medial ("switch-medial-independent") was not previously known. In this work we leverage recently developed graphical representations of linear formulae to build an implementation that is capable of more efficiently searching for switch-medial-independent inferences. We use it to find two "minimal" 8-variable independent inferences and also prove that no smaller ones exist; in contrast, a previous approach based directly on formulae reached computational limits already at 7 variables. One of these new inferences derives some previously found independent linear inferences. The other exhibits structure seemingly beyond the scope of previous approaches we are aware of; in particular, its existence contradicts a conjecture of Das and Strassburger.

## Subject Classification

##### ACM Subject Classification
• Theory of computation → Equational logic and rewriting
• Theory of computation → Proof theory
• Theory of computation → Linear logic
##### Keywords
• rewriting
• linear inference
• proof theory
• linear logic
• implementation

## Metrics

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

## References

1. Matteo Acclavio, Ross Horne, and Lutz Straßburger. An analytic propositional proof system on graphs. CoRR, abs/2012.01102, 2020. URL: http://arxiv.org/abs/2012.01102.
2. Matteo Acclavio, Ross Horne, and Lutz Straßburger. Logic beyond formulas: A proof system on graphs. In Holger Hermanns, Lijun Zhang, Naoki Kobayashi, and Dale Miller, editors, LICS '20: 35th Annual ACM/IEEE Symposium on Logic in Computer Science, Saarbrücken, Germany, July 8-11, 2020, pages 38-52. ACM, 2020. URL: https://doi.org/10.1145/3373718.3394763.
3. Andreas Blass. A game semantics for linear logic. Ann. Pure Appl. Log., 56(1-3):183-220, 1992. URL: https://doi.org/10.1016/0168-0072(92)90073-9.
4. Coenraad Bron and Joep Kerbosch. Finding all cliques of an undirected graph (algorithm 457). Commun. ACM, 16(9):575-576, 1973.
5. Kai Brünnler. Deep inference and symmetry in classical proofs. PhD thesis, Dresden University of Technology, Germany, 2003. URL: http://hsss.slub-dresden.de/hsss/servlet/hsss.urlmapping.MappingServlet?id=1064911987703-3819.
6. Kai Brünnler and Alwen Fernanto Tiu. A local system for classical logic. In Robert Nieuwenhuis and Andrei Voronkov, editors, Logic for Programming, Artificial Intelligence, and Reasoning, 8th International Conference, LPAR 2001, Havana, Cuba, December 3-7, 2001, Proceedings, volume 2250 of Lecture Notes in Computer Science, pages 347-361. Springer, 2001. URL: https://doi.org/10.1007/3-540-45653-8_24.
7. Cameron Calk, Anupam Das, and Tim Waring. Beyond formulas-as-cographs: an extension of boolean logic to arbitrary graphs. CoRR, abs/2004.12941, 2020. URL: http://arxiv.org/abs/2004.12941.
8. Stephen A. Cook and Robert A. Reckhow. On the lengths of proofs in the propositional calculus (preliminary version). In Robert L. Constable, Robert W. Ritchie, Jack W. Carlyle, and Michael A. Harrison, editors, Proceedings of the 6th Annual ACM Symposium on Theory of Computing, April 30 - May 2, 1974, Seattle, Washington, USA, pages 135-148. ACM, 1974. URL: https://doi.org/10.1145/800119.803893.
9. Stephen A. Cook and Robert A. Reckhow. The relative efficiency of propositional proof systems. J. Symb. Log., 44(1):36-50, 1979. URL: https://doi.org/10.2307/2273702.
10. Anupam Das. On the proof complexity of cut-free bounded deep inference. In Kai Brünnler and George Metcalfe, editors, Automated Reasoning with Analytic Tableaux and Related Methods - 20th International Conference, TABLEAUX 2011, Bern, Switzerland, July 4-8, 2011. Proceedings, volume 6793 of Lecture Notes in Computer Science, pages 134-148. Springer, 2011. URL: https://doi.org/10.1007/978-3-642-22119-4_12.
11. Anupam Das. Rewriting with Linear Inferences in Propositional Logic. In Femke van Raamsdonk, editor, 24th International Conference on Rewriting Techniques and Applications (RTA 2013), volume 21 of Leibniz International Proceedings in Informatics (LIPIcs), pages 158-173, Dagstuhl, Germany, 2013. Schloss Dagstuhl-Leibniz-Zentrum fuer Informatik. URL: https://doi.org/10.4230/LIPIcs.RTA.2013.158.
12. Anupam Das. An unavoidable contraction loop in monotone deep inference, 2017. URL: http://cs.bath.ac.uk/ag/das/con-loop.pdf.
13. Anupam Das. A new linear inference of size 8. The Proof Theory Blog, June 2020. URL: https://prooftheory.blog/2020/06/25/new-linear-inference/.
14. Anupam Das and Lutz Straßburger. No complete linear term rewriting system for propositional logic. In Maribel Fernández, editor, 26th International Conference on Rewriting Techniques and Applications, RTA 2015, June 29 to July 1, 2015, Warsaw, Poland, volume 36 of LIPIcs, pages 127-142. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2015. URL: https://doi.org/10.4230/LIPIcs.RTA.2015.127.
15. Anupam Das and Lutz Straßburger. On linear rewriting systems for boolean logic and some applications to proof theory. Log. Methods Comput. Sci., 12(4), 2016. URL: https://doi.org/10.2168/LMCS-12(4:9)2016.
16. Jean-Yves Girard. Linear logic. Theor. Comput. Sci., 50:1-102, 1987. URL: https://doi.org/10.1016/0304-3975(87)90045-4.
17. Alessio Guglielmi. A system of interaction and structure. ACM Trans. Comput. Log., 8(1):1, 2007. URL: https://doi.org/10.1145/1182613.1182614.
18. Alessio Guglielmi and Tom Gundersen. Normalisation control in deep inference via atomic flows. Log. Methods Comput. Sci., 4(1), 2008. URL: https://doi.org/10.2168/LMCS-4(1:9)2008.
19. Tom Gundersen. A General View of Normalisation through Atomic Flows. PhD thesis, University of Bath, UK, 2009. URL: https://tel.archives-ouvertes.fr/tel-00441540.
20. Giorgi Japaridze. Introduction to cirquent calculus and abstract resource semantics. CoRR, abs/math/0506553, 2005. URL: http://arxiv.org/abs/math/0506553.
21. Giorgi Japaridze. Elementary-base cirquent calculus I: parallel and choice connectives. CoRR, abs/1707.04823, 2017. URL: http://arxiv.org/abs/1707.04823.
22. Jan Krajícek. The cook-reckhow definition. CoRR, abs/1909.03691, 2019. URL: http://arxiv.org/abs/1909.03691.
23. Lê Thành Dung Nguyên and Thomas Seiller. Coherent interaction graphs. In Thomas Ehrhard, Maribel Fernández, Valeria de Paiva, and Lorenzo Tortora de Falco, editors, Proceedings Joint International Workshop on Linearity & Trends in Linear Logic and Applications, Linearity-TLLA@FLoC 2018, Oxford, UK, 7-8 July 2018, volume 292 of EPTCS, pages 104-117, 2018. URL: https://doi.org/10.4204/EPTCS.292.6.
24. Alex Rice. Linear inferences of size 7. The Proof Theory Blog, October 2020. URL: https://prooftheory.blog/2020/10/01/linear-inferences-of-size-7/.
25. Alex Rice. ěrb|lin_inf| rust crate. https://github.com/alexarice/lin_inf, 2021.
26. Lutz Straßburger. A local system for linear logic. In Matthias Baaz and Andrei Voronkov, editors, Logic for Programming, Artificial Intelligence, and Reasoning, 9th International Conference, LPAR 2002, Tbilisi, Georgia, October 14-18, 2002, Proceedings, volume 2514 of Lecture Notes in Computer Science, pages 388-402. Springer, 2002. URL: https://doi.org/10.1007/3-540-36078-6_26.
27. Lutz Straßburger. Linear logic and noncommutativity in the calculus of structures. PhD thesis, Dresden University of Technology, Germany, 2003. URL: http://hsss.slub-dresden.de/hsss/servlet/hsss.urlmapping.MappingServlet?id=1063208959250-7293.
28. Lutz Straßburger. A characterization of medial as rewriting rule. In Franz Baader, editor, Term Rewriting and Applications, 18th International Conference, RTA 2007, Paris, France, June 26-28, 2007, Proceedings, volume 4533 of Lecture Notes in Computer Science, pages 344-358. Springer, 2007. URL: https://doi.org/10.1007/978-3-540-73449-9_26.
29. Lutz Straßburger. Personal communication, 2012.
30. Lutz Straßburger. Extension without cut. Ann. Pure Appl. Log., 163(12):1995-2007, 2012. URL: https://doi.org/10.1016/j.apal.2012.07.004.
31. Alvin Šipraga. An automated search of linear inference rules. Summer research project. Supervised by Alessio Guglielmi and Anupam Das, 2012. URL: http://arcturus.su/mimir/autolininf.pdf.