Temporal BI: proof system, semantics and translations
DOI10.1016/j.tcs.2013.04.029zbMath1296.03014OpenAlexW2050129957MaRDI QIDQ391122
Publication date: 10 January 2014
Published in: Theoretical Computer Science (Search for Journal in Brave)
Full work available at URL: https://doi.org/10.1016/j.tcs.2013.04.029
completenesssequent calculusdecidabilitytemporal logiccut-eliminationresource semanticstopological semanticslogic of bunched implicationsGirard translationintuitionistic temporal linear logictemporal extension of BI
Logic in computer science (03B70) Cut-elimination and normal-form theorems (03F05) Temporal logic (03B44) Substructural logics (including relevance, entailment, linear logic, Lambek calculus, BCK and BCI logics) (03B47) Proof-theoretic aspects of linear logic and other substructural logics (03F52) Combined logics (03B62)
Related Items (1)
Cites Work
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Linear logic
- Synchronized linear-time temporal logic
- Bounded linear-time temporal logic: a proof-theoretic investigation
- A calculus and logic of resources and processes
- The Gentzenization and decidability of RW
- Algebra and logic for access control
- Combining linear-time temporal logic with constructiveness and paraconsistency
- \(TW_+\) and \(RW_+\) are decidable
- Distributed concurrent linear logic programming
- Decidable fragments of first-order temporal logics
- An approach to infinitary temporal proof theory
- Possible worlds and resources: The semantics of \(\mathbf{BI}\)
- The complexity of propositional linear temporal logics in simple cases
- From multiple sequent for additive linear logic to decision procedures for free lattices
- Gentzenization and decidability of some contraction-less relevant logics
- Linear and affine logics with temporal, spatial and epistemic operators
- The semantics and proof theory of the logic of bunched implications
- Tableaux for constructive concurrent dynamic logic
- First-order logic with two variables and unary temporal logic
- Uniform proofs as a foundation for logic programming
- Systems Modelling via Resources and Processes: Philosophy, Calculus, Semantics, and Logic
- Phase semantics for linear-time formalism
- The semantics of BI and resource tableaux
- Embedding Linear-Time Temporal Logic into Infinitary Logic: Application to Cut-Elimination for Multi-agent Infinitary Epistemic Linear-Time Temporal Logic
- Algebra and logic for resource-based systems modelling
- A Logical and Computational Theory of Located Resource
- Constructible falsity and inexact predicates
- Sequential Calculus for a First Order Infinitary Temporal Logic
- Algebraic laws for nondeterminism and concurrency
- The complexity of propositional linear temporal logics
- The Logic of Bunched Implications
- Semantic Labelled Tableaux for Propositional BI
- On bunched typing
- Combining Soft Linear Logic and Spatio-temporal Operators
- Resource-distribution via Boolean constraints
- Computer Science Logic
- AN NP-COMPLETE FRAGMENT OF LTL
- Semantics for relevant logics
- Solution to a problem of Ono and Komori
This page was built for publication: Temporal BI: proof system, semantics and translations
