Combining linear-time temporal logic with constructiveness and paraconsistency
The linear-time temporal logic (based on classical logic) is known to be useful for expressing temporal reasoning in computer science. From this viewpoint it is interesting to combine linear time with other aspects such as constructiveness or inconsistency-tolerance. In fact, it has been pointed out by Maier that certain intuitionistic linear-time temporal logic admits an elegant characterization of safety and liveness properties, where the logic is presented there in an algebraic setting. This paper provides Gentzen-type systems for intuitionistic and paraconsistent bounded linear-time temporal logics, respectively. Their time domain is bounded by a fixed positive integer, so that the logics are shown to enjoy faithful embeddings into intuitionistic logic and Nelson's paraconsistent logic, respectively, while almost all useful temporal axioms are available. The authors establish for them some fundamental properties such as completeness with respect to Kripke semantics, cut-elimination, and decidability. They are also formulated in natural deduction systems with normalization as well as in sound and complete display calculi.
- A Paraconsistent Linear-time Temporal Logic
- Strong Normalization of a Typed Lambda Calculus for Intuitionistic Bounded Linear-time Temporal Logic
- Paraconsistent sequential linear-time temporal logic: combining paraconsistency and sequentiality in temporal reasoning
- Constructive linear-time temporal logic: proof systems and Kripke semantics
- Bounded linear-time temporal logic: a proof-theoretic investigation
- A proof-theoretic investigation of a logic of positions
- A semantical study of constructible falsity
- Analysis and synthesis of logics. How to cut and paste reasoning systems
- Computer Science Logic
- Constructible falsity
- Constructible falsity and inexact predicates
- Constructive negation, implication, and co-implication
- Decidable fragments of first-order temporal logics
- Display logic
- Displaying and deciding substructural logics. I: Logics with contraposition
- Displaying modal logic
- Embedding Linear-Time Temporal Logic into Infinitary Logic: Application to Cut-Elimination for Multi-agent Infinitary Epistemic Linear-Time Temporal Logic
- Handbook of philosophical logic. Vol. 6
- scientific article; zbMATH DE number 2070200 (Why is no real title available?)
- scientific article; zbMATH DE number 2079776 (Why is no real title available?)
- scientific article; zbMATH DE number 1405444 (Why is no real title available?)
- scientific article; zbMATH DE number 3275554 (Why is no real title available?)
- scientific article; zbMATH DE number 970633 (Why is no real title available?)
- Inconsistency-tolerant description logic. II: A tableau algorithm for \(\mathcal{CALC}^{\mathsf C}\)
- Infinitary propositional intuitionistic logic
- Informational interpretation of substructural propositional logics
- LAR: A logic of algorithmic reasoning
- Logic Programming with Strong Negation and Inexact Predicates
- Natural deduction systems for Nelson's paraconsistent logic and its neighbors
- Semantical analyses of propositional systems of Fitch and Nelson
- Sequential Calculus for a First Order Infinitary Temporal Logic
- Tableaux for constructive concurrent dynamic logic
- The logic of information structures
- Paraconsistent computation tree logic
- A decidable paraconsistent relevant logic: Gentzen system and Routley-Meyer semantics
- A Paraconsistent Linear-time Temporal Logic
- Embedding Linear-Time Temporal Logic into Infinitary Logic: Application to Cut-Elimination for Multi-agent Infinitary Epistemic Linear-Time Temporal Logic
- Intuitionistic linear-time -calculus
- Inconsistency-tolerant multi-agent calculus
- Temporal BI: proof system, semantics and translations
- The intuitionistic temporal logic of dynamical systems
- Representing any-time and program-iteration by infinitary conjunction
- Paraconsistent sequential linear-time temporal logic: combining paraconsistency and sequentiality in temporal reasoning
- Temporal Gödel-Gentzen and Girard translations
- scientific article; zbMATH DE number 1444739 (Why is no real title available?)
- Complete intuitionistic temporal logics for topological dynamics
- scientific article; zbMATH DE number 7311251 (Why is no real title available?)
- Intuitionistic linear temporal logics
- Embedding theorems for LTL and its variants
- Advances in Computing Science – ASIAN 2003. Progamming Languages and Distributed Computation Programming Languages and Distributed Computation
- Exploring the Jungle of Intuitionistic Temporal Logics
- Synchronized linear-time temporal logic
- Ill-founded proof systems for intuitionistic linear-time temporal logic
- On a generalization of Heyting algebras. I
- Unification in linear temporal logic LTL
- Unified sequent calculi and natural deduction systems for until-free linear-time temporal logics
- Constructive linear-time temporal logic: proof systems and Kripke semantics
- Bounded linear-time temporal logic: a proof-theoretic investigation
- Proof theory of Nelson's paraconsistent logic: a uniform perspective
This page was built for publication: Combining linear-time temporal logic with constructiveness and paraconsistency
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q975875)
