Dual systems of tableaux and sequents for PLTL

DOI10.1016/j.jlap.2009.05.001zbMath1183.68596OpenAlexW1979014177MaRDI QIDQ1035676

Montserrat Hermo, Jose Gaintzarain, Paqui Lucio, Fernando Orejas, Marisa Navarro

Publication date: 4 November 2009

Published in: The Journal of Logic and Algebraic Programming (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1016/j.jlap.2009.05.001

zbMATH Keywords

tableauxtemporal logicsequent calculiinvariant-freecut-free

Mathematics Subject Classification ID

Logic in artificial intelligence (68T27) Temporal logic (03B44)

Related Items

Invariant-free clausal temporal resolution, Abstract Diagnosis for tccp using a Linear Temporal Logic, Tableaux for realizability of safety specifications, Branching-time logic \(\mathsf{ECTL}^{\#}\) and its tree-style one-pass tableau: extending fairness expressibility of \(\mathsf{ECTL}^+\), One-pass Context-based Tableaux Systems for CTL and ECTL, Extending Fairness Expressibility of ECTL+: A Tree-Style One-Pass Tableau Approach, Tableaux and sequent calculi for \textsf{CTL} and \textsf{ECTL}: satisfiability test with certifying proofs and models

Uses Software

• TTM

Cites Work

• Cut-free sequent systems for temporal logic
• Schlussweisen-Kalküle der Prädikatenlogik
• Temporal logic can be more expressive
• One-Pass Tableaux for Computation Tree Logic
• A Cut-Free and Invariant-Free Sequent Calculus for PLTL
• The complexity of propositional linear temporal logics
• Propositional temporal logics: decidability and completeness
• Investigation of finitary calculus for a discrete linear time logic by means of infinitary calculus
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item