2026-08-14T18:54:08Z https://drops.dagstuhl.de/oai

oai:drops-oai.dagstuhl.de:5533 2024-03-06T10:35:59Z ddc:004 open_access

A First-order Logic for String Diagrams Kissinger, Aleks Quick, David string diagrams compact closed monoidal categories abstract tensor systems first-order logic Equational reasoning with string diagrams provides an intuitive means of proving equations between morphisms in a symmetric monoidal category. This can be extended to proofs of infinite families of equations using a simple graphical syntax called !-box notation. While this does greatly increase the proving power of string diagrams, previous attempts to go beyond equational reasoning have been largely ad hoc, owing to the lack of a suitable logical framework for diagrammatic proofs involving !-boxes. In this paper, we extend equational reasoning with !-boxes to a fully-fledged first order logic with conjunction, implication, and universal quantification over !-boxes. This logic, called !L, is then rich enough to properly formalise an induction principle for !-boxes. We then build a standard model for !L and give an example proof of a theorem for non-commutative bialgebras using !L, which is unobtainable by equational reasoning alone. Schloss Dagstuhl – Leibniz-Zentrum für Informatik Aleks Kissinger and David Quick 2015 Is Part Of LIPIcs, Volume 35, 6th Conference on Algebra and Coalgebra in Computer Science (CALCO 2015) InProceedings Text doc-type:ResearchArticle publishedVersion application/pdf doi:10.4230/LIPIcs.CALCO.2015.171 urn:nbn:de:0030-drops-55335 https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CALCO.2015.171 eng https://creativecommons.org/licenses/by/3.0/legalcode