Temporal BI: proof system, semantics and translations
type: Item
instance of: scholarly article
title: Temporal BI: proof system, semantics and translations
zbMATH Open document ID: 1296.03014
author: Norihiro Kamide
published in: Theoretical Computer Science
publication date: 2014-01-10T00:00:00Z
Mathematics Subject Classification ID: 03B44
Mathematics Subject Classification ID: 03B47
Mathematics Subject Classification ID: 03B62
Mathematics Subject Classification ID: 03B70
Mathematics Subject Classification ID: 03F05
Mathematics Subject Classification ID: 03F52
zbMATH DE Number: 6244027
zbMATH Keywords: temporal logic
zbMATH Keywords: completeness
zbMATH Keywords: decidability
zbMATH Keywords: logic of bunched implications
zbMATH Keywords: temporal extension of BI
zbMATH Keywords: sequent calculus
zbMATH Keywords: cut-elimination
zbMATH Keywords: topological semantics
zbMATH Keywords: resource semantics
zbMATH Keywords: intuitionistic temporal linear logic
zbMATH Keywords: Girard translation
MaRDI profile type: Publication
full work available at URL: j.tcs.2013.04.029
OpenAlex ID: W2050129957
cites work: Q4471865
cites work: Constructible falsity and inexact predicates
cites work: Q4539612
cites work: An approach to infinitary temporal proof theory
cites work: Q4704742
cites work: The Gentzenization and decidability of RW
cites work: Gentzenization and decidability of some contraction-less relevant logics
cites work: Q4938418
cites work: A Logical and Computational Theory of Located Resource
cites work: Algebra and logic for resource-based systems modelling
cites work: Algebra and logic for access control
cites work: The complexity of propositional linear temporal logics in simple cases
cites work: Q4342081
cites work: Q4085699
cites work: First-order logic with two variables and unary temporal logic
cites work: Semantic Labelled Tableaux for Propositional BI
cites work: The semantics of BI and resource tableaux
cites work: \(TW_+\) and \(RW_+\) are decidable
cites work: Linear logic
cites work: Resource-distribution via Boolean constraints
cites work: Algebraic laws for nondeterminism and concurrency
cites work: Decidable fragments of first-order temporal logics
cites work: Combining Soft Linear Logic and Spatio-temporal Operators
cites work: Linear and affine logics with temporal, spatial and epistemic operators
cites work: Q5460163
cites work: Embedding Linear-Time Temporal Logic into Infinitary Logic: Application to Cut-Elimination for Multi-agent Infinitary Epistemic Linear-Time Temporal Logic
cites work: Phase semantics for linear-time formalism
cites work: Bounded linear-time temporal logic: a proof-theoretic investigation
cites work: Combining linear-time temporal logic with constructiveness and paraconsistency
cites work: Sequential Calculus for a First Order Infinitary Temporal Logic
cites work: Distributed concurrent linear logic programming
cites work: Computer Science Logic
cites work: From multiple sequent for additive linear logic to decision procedures for free lattices
cites work: Uniform proofs as a foundation for logic programming
cites work: AN NP-COMPLETE FRAGMENT OF LTL
cites work: On bunched typing
cites work: The Logic of Bunched Implications
cites work: Q5556395
cites work: The semantics and proof theory of the logic of bunched implications
cites work: Possible worlds and resources: The semantics of \(\mathbf{BI}\)
cites work: A calculus and logic of resources and processes
cites work: Systems modelling via resources and processes: philosophy, calculus, semantics, and logic
cites work: The complexity of propositional linear temporal logics
cites work: Solution to a problem of Ono and Komori
cites work: Semantics for relevant logics
cites work: Q4219025
cites work: Synchronized linear-time temporal logic
cites work: Tableaux for constructive concurrent dynamic logic
cites work: Timed Petri nets and temporal linear logic
DOI: 10.1016/J.TCS.2013.04.029
description: scientific article; zbMATH DE number 6244027