A Graphical Proof Theory of Logical Time
| Autor: | Acclavio, Matteo, Horne, Ross, Mauw, Sjouke, Straßburger, Lutz |
|---|---|
| Přispěvatelé: | University of Luxembourg [Luxembourg], Automatisation et ReprésenTation: fOndation du calcUl et de la déducTion (PARTOUT), Laboratoire d'informatique de l'École polytechnique [Palaiseau] (LIX), École polytechnique (X)-Centre National de la Recherche Scientifique (CNRS)-École polytechnique (X)-Centre National de la Recherche Scientifique (CNRS)-Inria Saclay - Ile de France, Institut National de Recherche en Informatique et en Automatique (Inria)-Institut National de Recherche en Informatique et en Automatique (Inria), École polytechnique (X)-Centre National de la Recherche Scientifique (CNRS), Editor: Amy P. Felty, Acclavio, M., Horne, R., Mauw, S., Strassburger, L. |
| Jazyk: | angličtina |
| Rok vydání: | 2022 |
| Předmět: |
Computer science [C05] [Engineering
computing & technology] causality Theory of computation → Linear logic deep inference Digital Object Identifier 10.4230/LIPIcs.FSCD.2022.22 Theory of computation → Process calculi phrases proof theory [INFO.INFO-LO]Computer Science [cs]/Logic in Computer Science [cs.LO] proof theory Sciences informatiques [C05] [Ingénierie informatique & technologie] 2012 ACM Subject Classification Theory of computation → Proof theory Theory of computation → Linear logic Theory of computation → Process calculi phrases proof theory TheoryofComputation_MATHEMATICALLOGICANDFORMALLANGUAGES Theory of computation → Proof theory Theory of computation → Process calculi 2012 ACM Subject Classification Theory of computation → Proof theory Computer Science::Logic in Computer Science deep inference |
| Zdroj: | 7th International Conference on Formal Structures for Computation and Deduction (FSCD 2022) 7th International Conference on Formal Structures for Computation and Deduction (FSCD 2022), Aug 2022, Haifa, Israel. ⟨10.4230/LIPIcs.FSCD.2022.22⟩ |
| DOI: | 10.4230/lipics.fscd.2022.22 |
| Popis: | 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. LIPIcs, Vol. 228, 7th International Conference on Formal Structures for Computation and Deduction (FSCD 2022), pages 22:1-22:25 |
| Databáze: | OpenAIRE |
| Externí odkaz: |
|