TY - GEN
T1 - A Graphical Proof Theory of Logical Time
AU - Acclavio, Matteo
AU - Horne, Ross
AU - Mauw, Sjouke
AU - Straßburger, Lutz
N1 - Publisher Copyright:
© Matteo Acclavio, Ross Horne, Sjouke Mauw, and Lutz Straßburger
PY - 2022/6/1
Y1 - 2022/6/1
N2 - 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.
AB - 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.
KW - causality
KW - deep inference
KW - proof theory
UR - https://www.scopus.com/pages/publications/85129984609
U2 - 10.4230/LIPIcs.FSCD.2022.22
DO - 10.4230/LIPIcs.FSCD.2022.22
M3 - Conference contribution
AN - SCOPUS:85129984609
T3 - Leibniz International Proceedings in Informatics, LIPIcs
BT - 7th International Conference on Formal Structures for Computation and Deduction, FSCD 2022
A2 - Felty, Amy P.
PB - Schloss Dagstuhl- Leibniz-Zentrum fur Informatik GmbH, Dagstuhl Publishing
T2 - 7th International Conference on Formal Structures for Computation and Deduction, FSCD 2022
Y2 - 2 August 2022 through 5 August 2022
ER -