Document Open Access Logo

BV and Pomset Logic Are Not the Same

Authors Lê Thành Dũng (Tito) Nguyễn , Lutz Straßburger

PDF
Thumbnail PDF

File

LIPIcs.CSL.2022.32.pdf
  • Filesize: 0.85 MB
  • 17 pages

Document Identifiers

Author Details

Lê Thành Dũng (Tito) Nguyễn
  • CNRS & IRISA, Rennes, France
Lutz Straßburger
  • Inria Saclay & École Polytechnique, Palaiseau, France

Cite As Get BibTex

Lê Thành Dũng (Tito) Nguyễn and Lutz Straßburger. BV and Pomset Logic Are Not the Same. In 30th EACSL Annual Conference on Computer Science Logic (CSL 2022). Leibniz International Proceedings in Informatics (LIPIcs), Volume 216, pp. 32:1-32:17, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2022) https://doi.org/10.4230/LIPIcs.CSL.2022.32

Abstract

BV and pomset logic are two logics that both conservatively extend unit-free multiplicative linear logic by a third binary connective, which (i) is non-commutative, (ii) is self-dual, and (iii) lies between the "par" and the "tensor". It was conjectured early on (more than 20 years ago), that these two logics, that share the same language, that both admit cut elimination, and whose connectives have essentially the same properties, are in fact the same. In this paper we show that this is not the case. We present a formula that is provable in pomset logic but not in BV.

Subject Classification

ACM Subject Classification
  • Theory of computation → Linear logic
  • Theory of computation → Proof theory
Keywords
  • proof nets
  • deep inference
  • pomset logic
  • system BV
  • cographs
  • dicographs
  • series-parallel orders

Metrics

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

References

  1. V. Michele Abrusci and Paul Ruet. Non-commutative logic I: the multiplicative fragment. Annals of Pure and Applied Logic, 101(1):29-64, 1999. URL: https://doi.org/10.1016/S0168-0072(99)00014-7.
  2. 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.
  3. Paola Bruscoli. A purely logical account of sequentiality in proof search. In Peter J. Stuckey, editor, Logic Programming, 18th International Conference, ICLP 2002, Copenhagen, Denmark, July 29 - August 1, 2002, Proceedings, volume 2401 of Lecture Notes in Computer Science, pages 302-316. Springer, 2002. URL: https://doi.org/10.1007/3-540-45619-8_21.
  4. Denis Béchet, Philippe de Groote, and Christian Retoré. A complete axiomatisation for the inclusion of series-parallel partial orders. In Hubert Comon, editor, Rewriting Techniques and Applications, 8th International Conference, RTA-97, Sitges, Spain, June 2-5, 1997, Proceedings, volume 1232 of Lecture Notes in Computer Science, pages 230-240. Springer, 1997. URL: https://doi.org/10.1007/3-540-62950-5_74.
  5. Anupam Das and Alex A. Rice. New minimal linear inferences in boolean logic independent of switch and medial. In Naoki Kobayashi, editor, 6th International Conference on Formal Structures for Computation and Deduction, FSCD 2021, July 17-24, 2021, Buenos Aires, Argentina (Virtual Conference), volume 195 of LIPIcs, pages 14:1-14:19. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2021. URL: https://doi.org/10.4230/LIPIcs.FSCD.2021.14.
  6. Anupam Das and Lutz Straßburger. On linear rewriting systems for boolean logic and some applications to proof theory. Logical Methods in Computer Science, 12(4), 2016. URL: https://doi.org/10.2168/LMCS-12(4:9)2016.
  7. Arnaud Fleury and Christian Retoré. The mix rule. Mathematical Structures in Computer Science, 4(2):273-285, 1994. URL: https://doi.org/10.1017/S0960129500000451.
  8. Jean-Yves Girard. Linear logic. Theoretical Computer Science, 50(1):1-101, January 1987. URL: https://doi.org/10.1016/0304-3975(87)90045-4.
  9. Jean-Yves Girard. Towards a geometry of interaction. In J. W. Gray and A. Scedrov, editors, Categories in Computer Science and Logic, volume 92 of Contemporary Mathematics, pages 69-108. American Mathematical Society, Providence, RI, 1989. Proceedings of a Summer Research Conference held June 14-20, 1987. URL: https://doi.org/10.1090/conm/092/1003197.
  10. Alessio Guglielmi. A system of interaction and structure. ACM Transactions on Computational Logic, 8(1), January 2007. According to the author, the published version contains errors introduced by the editorial processing; the authoritative version is https://arxiv.org/abs/cs/9910023. URL: https://doi.org/10.1145/1182613.1182614.
  11. Alessio Guglielmi and Lutz Straßburger. Non-commutativity and MELL in the Calculus of Structures. In Gerhard Goos, Juris Hartmanis, Jan van Leeuwen, and Laurent Fribourg, editors, Computer Science Logic, volume 2142, pages 54-68. Springer Berlin Heidelberg, Berlin, Heidelberg, 2001. URL: https://doi.org/10.1007/3-540-44802-0_5.
  12. Ross Horne and Alwen Tiu. Constructing weak simulations from linear implications for processes with private names. Mathematical Structures in Computer Science, 29(8):1275-1308, 2019. URL: https://doi.org/10.1017/S0960129518000452.
  13. Ross Horne, Alwen Tiu, Bogdan Aman, and Gabriel Ciobanu. De morgan dual nominal quantifiers modelling private names in non-commutative logic. ACM Transactions on Computational Logic, 20(4):22:1-22:44, 2019. URL: https://doi.org/10.1145/3325821.
  14. Ozan Kahramanoğulları. System BV without the Equalities for Unit. In Computer and Information Sciences - ISCIS 2004, volume 3280, pages 986-995. Springer Berlin Heidelberg, Berlin, Heidelberg, 2004. URL: https://doi.org/10.1007/978-3-540-30182-0_99.
  15. Ozan Kahramanoğulları. System BV is NP-complete. Annals of Pure and Applied Logic, 152(1):107-121, March 2008. URL: https://doi.org/10.1016/j.apal.2007.11.005.
  16. Joachim Lambek. The mathematics of sentence structure. The American Mathematical Monthly, 65(3):154-170, 1958. URL: http://www.jstor.org/stable/2310058.
  17. Alain Lecomte and Christian Retoré. Pomset logic as an alternative categorial grammar. In Formal Grammar, pages 181-196. FoLLI, 1995. Google Scholar
  18. Lê Thành Dũng Nguyên. Complexity of correctness for pomset logic proof nets, 2020. URL: http://arxiv.org/abs/1912.10606.
  19. Peter W. O'Hearn and David J. Pym. The logic of bunched implications. Bulletin of Symbolic Logic, 5(2):215-244, 1999. URL: https://doi.org/10.2307/421090.
  20. Christian Retoré. Réseaux et séquents ordonnés. PhD thesis, Université Paris VII, February 1993. URL: https://tel.archives-ouvertes.fr/tel-00585634.
  21. Christian Retoré. Pomset logic: A non-commutative extension of classical linear logic. In Typed Lambda Calculi and Applications, volume 1210, pages 300-318. Springer Berlin Heidelberg, Berlin, Heidelberg, 1997. URL: https://doi.org/10.1007/3-540-62688-3_43.
  22. Christian Retoré. Pomset Logic as a Calculus of Directed Cographs. Research Report 3714, INRIA, June 1999. URL: https://hal.inria.fr/inria-00072953.
  23. Christian Retoré. Handsome proof-nets: perfect matchings and cographs. Theoretical Computer Science, 294(3):473-488, February 2003. URL: https://doi.org/10.1016/S0304-3975(01)00175-X.
  24. Christian Retoré. Pomset Logic: The other approach to noncommutativity in logic. In Claudia Casadio and Philip J. Scott, editors, Joachim Lambek: the interplay of mathematics, logic, and linguistics, Outstanding Contributions to Logic, chapter 9, pages 299-346. Springer, 2021. URL: https://doi.org/10.1007/978-3-030-66545-6_9.
  25. Sergey Slavnov. On noncommutative extensions of linear logic. Logical Methods in Computer Science, Volume 15, Issue 3, September 2019. URL: https://doi.org/10.23638/LMCS-15(3:30)2019.
  26. Lutz Straßburger. System NEL is undecidable. Electronic Notes in Theoretical Computer Science, 84:166-177, 2003. URL: https://doi.org/10.1016/S1571-0661(04)80853-3.
  27. Lutz Straßburger. Extension without cut. Annals of Pure and Applied Logic, 163(12):1995-2007, 2012. URL: https://doi.org/10.1016/j.apal.2012.07.004.
  28. Lutz Straßburger. Linear Logic and Noncommutativity in the Calculus of Structures. PhD Thesis, Technische Universität Dresden, 2003. URL: https://www.lix.polytechnique.fr/~lutz/papers/dissvonlutz.pdf.
  29. David N. Yetter. Quantales and (noncommutative) linear logic. The Journal of Symbolic Logic, 55(1):41-64, March 1990. URL: https://doi.org/10.2307/2274953.
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-2024 Schloss Dagstuhl – LZI GmbH About DROPS Imprint Privacy Contact