Skip to main navigation Skip to search Skip to main content

A Graphical Proof Theory of Logical Time

  • University of Luxembourg
  • INRIA

Research output: Chapter in Book/Report/Conference proceedingConference contributionpeer-review

Abstract

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.

Original languageEnglish
Title of host publication7th International Conference on Formal Structures for Computation and Deduction, FSCD 2022
EditorsAmy P. Felty
PublisherSchloss Dagstuhl- Leibniz-Zentrum fur Informatik GmbH, Dagstuhl Publishing
ISBN (Electronic)9783959772334
DOIs
Publication statusPublished - 1 Jun 2022
Externally publishedYes
Event7th International Conference on Formal Structures for Computation and Deduction, FSCD 2022 - Haifa, Israel
Duration: 2 Aug 20225 Aug 2022

Publication series

NameLeibniz International Proceedings in Informatics, LIPIcs
Volume228
ISSN (Print)1868-8969

Conference

Conference7th International Conference on Formal Structures for Computation and Deduction, FSCD 2022
Country/TerritoryIsrael
CityHaifa
Period2/08/225/08/22

Keywords

  • causality
  • deep inference
  • proof theory

Fingerprint

Dive into the research topics of 'A Graphical Proof Theory of Logical Time'. Together they form a unique fingerprint.

Cite this