Dual systems of tableaux and sequents for PLTL

DOI10.1016/J.JLAP.2009.05.001MaRDI QIDQ1035676zbMATH OpenOpenAlexFDO

Authors Jose Gaintzarain, M. Hermo, P. Lucio, Marisa Navarro, Fernando Orejas

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

sequent calculitemporal logictableauxinvariant-freecut-free

Mathematics Subject Classification ID

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

Recommendations

• scientific article; zbMATH DE number 446843
• Sequent systems for PLTL
• Systematic semantic tableaux for PLTL
• Finite sequent calculi for PLTL
• Foundations of Software Science and Computational Structures
• A Cut-Free and Invariant-Free Sequent Calculus for PLTL
• PTL sequent calculus system
• Prefixed tableau systems for logic of proofs and provability
• Dual tableau for monoidal triangular norm logic MTL
• A tableau style proof system for two paraconsistent logics

Cites work

• scientific article; zbMATH DE number 4170873 (Why is no real title available?)
• scientific article; zbMATH DE number 1189110 (Why is no real title available?)
• scientific article; zbMATH DE number 67448 (Why is no real title available?)
• scientific article; zbMATH DE number 830431 (Why is no real title available?)
• scientific article; zbMATH DE number 3327279 (Why is no real title available?)
• scientific article; zbMATH DE number 3333259 (Why is no real title available?)
• A Cut-Free and Invariant-Free Sequent Calculus for PLTL
• Cut-free sequent systems for temporal logic
• Deep sequent systems for modal logic
• Investigation of finitary calculus for a discrete linear time logic by means of infinitary calculus
• One-Pass Tableaux for Computation Tree Logic
• Propositional temporal logics: decidability and completeness
• Schlussweisen-Kalküle der Prädikatenlogik
• Systematic semantic tableaux for PLTL
• Tableau methods for modal and temporal logics
• Temporal logic can be more expressive
• The complexity of propositional linear temporal logics

Cited in

(11)

• Branching-time logic \(\mathsf{ECTL}^{\#}\) and its tree-style one-pass tableau: extending fairness expressibility of \(\mathsf{ECTL}^+\)
• Abstract diagnosis for tccp using a linear temporal logic
• Extending fairness expressibility of ECTL\(^+\): a tree-style one-pass tableau approach
• Systematic semantic tableaux for PLTL
• Tableaux and sequent calculi for \textsf{CTL} and \textsf{ECTL}: satisfiability test with certifying proofs and models
• Finite sequent calculi for PLTL
• Tableaux for realizability of safety specifications
• One-pass Context-based Tableaux Systems for CTL and ECTL
• Two-dimensional tableaux
• Invariant-free clausal temporal resolution
• Towards an efficient implementation of a tableau method for reactive safety specifications

Describes a project that uses

Uses Software

• TTM

This page was built for publication: Dual systems of tableaux and sequents for PLTL

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