2026-07-22T10:24:41Z https://drops.dagstuhl.de/oai

oai:drops-oai.dagstuhl.de:16303 2024-03-06T10:57:11Z ddc:004 open_access

A Graphical Proof Theory of Logical Time Acclavio, Matteo Horne, Ross Mauw, Sjouke Straßburger, Lutz proof theory causality deep inference Logical time is a partial order over events in distributed systems, constraining which events precede others. Special interest has been given to series-parallel orders since they correspond to formulas constructed via the two operations for "series" and "parallel" composition. For this reason, series-parallel orders have received attention from proof theory, leading to pomset logic, the logic BV, and their extensions. However, logical time does not always form a series-parallel order; indeed, ubiquitous structures in distributed systems are beyond current proof theoretic methods. In this paper, we explore how this restriction can be lifted. We design new logics that work directly on graphs instead of formulas, we develop their proof theory, and we show that our logics are conservative extensions of the logic BV. Schloss Dagstuhl – Leibniz-Zentrum für Informatik Matteo Acclavio and Ross Horne and Sjouke Mauw and Lutz Straßburger 2022 Is Part Of LIPIcs, Volume 228, 7th International Conference on Formal Structures for Computation and Deduction (FSCD 2022) InProceedings Text doc-type:ResearchArticle publishedVersion application/pdf doi:10.4230/LIPIcs.FSCD.2022.22 urn:nbn:de:0030-drops-163037 https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2022.22 eng https://creativecommons.org/licenses/by/4.0/legalcode