2026-07-25T21:33:27Z https://drops.dagstuhl.de/oai

oai:drops-oai.dagstuhl.de:18015 2024-03-06T11:00:52Z ddc:004 open_access

Labelled Tableaux for Linear Time Bunched Implication Logic Galmiche, Didier Méry, Daniel Temporal Logic Bunched Implication Logic Labelled Deduction Tableaux In this paper, we define the logic of Linear Temporal Bunched Implications (LTBI), a temporal extension of the Bunched Implications logic BI that deals with resource evolution over time, by combining the BI separation connectives and the LTL temporal connectives. We first present the syntax and semantics of LTBI and illustrate its expressiveness with a significant example. Then we introduce a tableau calculus with labels and constraints, called TLTBI, and prove its soundness w.r.t. the Kripke-style semantics of LTBI. Finally we discuss and analyze the issues that make the completeness of the calculus not trivial in the general case of unbounded timelines and explain how to solve the issues in the more restricted case of bounded timelines. Schloss Dagstuhl – Leibniz-Zentrum für Informatik Didier Galmiche and Daniel Méry 2023 Is Part Of LIPIcs, Volume 260, 8th International Conference on Formal Structures for Computation and Deduction (FSCD 2023) InProceedings Text doc-type:ResearchArticle publishedVersion application/pdf doi:10.4230/LIPIcs.FSCD.2023.31 urn:nbn:de:0030-drops-180159 https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2023.31 eng https://creativecommons.org/licenses/by/4.0/legalcode