Bounded linear-time temporal logic: a proof-theoretic investigation

DOI10.1016/J.APAL.2011.12.002MaRDI QIDQ764266zbMATH OpenOpenAlexFDO

Authors Norihiro Kamide

Publication date 13 March 2012

Published in Annals of Pure and Applied Logic (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1016/j.apal.2011.12.002

zbMATH Keywords

resolutionmodal logictemporal logicsequent calculus

Mathematics Subject Classification ID

Modal logic (including the logic of norms) (03B45) Cut-elimination and normal-form theorems (03F05) Temporal logic (03B44)

Recommendations

• Combining linear-time temporal logic with constructiveness and paraconsistency
• Strong Normalization of a Typed Lambda Calculus for Intuitionistic Bounded Linear-time Temporal Logic
• Publication:4938418
• The temporal logic of branching time
• scientific article; zbMATH DE number 1088203

Cites work

• scientific article; zbMATH DE number 3860378 (Why is no real title available?)
• scientific article; zbMATH DE number 3871318 (Why is no real title available?)
• scientific article; zbMATH DE number 4170873 (Why is no real title available?)
• scientific article; zbMATH DE number 3974944 (Why is no real title available?)
• scientific article; zbMATH DE number 1189100 (Why is no real title available?)
• scientific article; zbMATH DE number 67448 (Why is no real title available?)
• scientific article; zbMATH DE number 1215493 (Why is no real title available?)
• scientific article; zbMATH DE number 1223711 (Why is no real title available?)
• scientific article; zbMATH DE number 1142326 (Why is no real title available?)
• scientific article; zbMATH DE number 2070200 (Why is no real title available?)
• scientific article; zbMATH DE number 1405444 (Why is no real title available?)
• scientific article; zbMATH DE number 1406469 (Why is no real title available?)
• scientific article; zbMATH DE number 5270677 (Why is no real title available?)
• scientific article; zbMATH DE number 5050044 (Why is no real title available?)
• A proof-theoretic investigation of a logic of positions
• AN NP-COMPLETE FRAGMENT OF LTL
• An approach to infinitary temporal proof theory
• Clausal temporal resolution
• Combining linear-time temporal logic with constructiveness and paraconsistency
• Computer Science Logic
• Concerning the semantic consequence relation in first-order temporal logic
• Constructivism in mathematics. An introduction. Volume I
• Decidable fragments of first-order temporal logics
• Embedding Linear-Time Temporal Logic into Infinitary Logic: Application to Cut-Elimination for Multi-agent Infinitary Epistemic Linear-Time Temporal Logic
• First-order logic with two variables and unary temporal logic
• Investigation of finitary calculus for a discrete linear time logic by means of infinitary calculus
• LAR: A logic of algorithmic reasoning
• Linear and affine logics with temporal, spatial and epistemic operators
• Monodic temporal resolution
• Nonclausal deduction in first-order temporal logic
• Proof theory
• Quantized linear logic, involutive quantales and strong negation
• Sequential Calculus for a First Order Infinitary Temporal Logic
• Tableaux for constructive concurrent dynamic logic
• Temporal resolution using a breadth-first search algorithm
• The complexity of propositional linear temporal logics
• The complexity of propositional linear temporal logics in simple cases
• The logic of information structures
• Uniform proofs as a foundation for logic programming

Cited in

(10)

• Temporal BI: proof system, semantics and translations
• A bounded domain property for an expressive fragment of first-order linear temporal logic
• Combining linear-time temporal logic with constructiveness and paraconsistency
• scientific article; zbMATH DE number 5270677 (Why is no real title available?)
• A Paraconsistent Linear-time Temporal Logic
• From Linear to Branching-Time Temporal Logics: Transfer of Semantics and Definability
• Cyclic Proofs for Linear Temporal Logic
• A decidable temporal relevant logic for time-dependent relevant human reasoning
• Refutation-aware Gentzen-style calculi for propositional until-free linear-time temporal logic
• scientific article; zbMATH DE number 1405444 (Why is no real title available?)

Describes a project that uses

Uses Software

• TRP++

This page was built for publication: Bounded linear-time temporal logic: a proof-theoretic investigation

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q764266)