A Cut-Free and Invariant-Free Sequent Calculus for PLTL

DOI10.1007/978-3-540-74915-8_36MaRDI QIDQ3608433zbMATH OpenOpenAlexFDO

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

Publication date 5 March 2009

Published in Computer Science Logic (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1007/978-3-540-74915-8_36

Mathematics Subject Classification ID

Cut-elimination and normal-form theorems (03F05) Temporal logic (03B44)

Recommendations

• Cut, invariant rule, and loop-check free sequent calculus for PLTL
• Finite sequent calculi for PLTL
• Cut-elimination and a permutation-free sequent calculus for intuitionistic logic
• A contraction-free and cut-free sequent calculus for propositional dynamic logic
• Sequent systems for PLTL
• A Cut-Free Sequent Calculus for Bi-intuitionistic Logic
• A cut-free sequent calculus for pure type systems verifying the structural rules of Gentzen/Kleene
• A cut-free sequent calculus for the logic of constant domains with a limited amount of duplications
• Contraction-free sequent calculi for intuitionistic logic
• PTL sequent calculus system

Cited in

(12)

• Dual systems of tableaux and sequents for PLTL
• Cut, invariant rule, and loop-check free sequent calculus for PLTL
• More efficient proof-search for sequents of temporal logic
• One-Pass Tableaux for Computation Tree Logic
• Finite sequent calculi for PLTL
• Invariant-free clausal temporal resolution
• Sequent systems for PLTL
• On the proof theory of the modal mu-calculus
• Cut-free sequent systems for temporal logic
• Loop-type sequent calculi for temporal logic
• A derivation-loop method for temporal logic
• Refutation-aware Gentzen-style calculi for propositional until-free linear-time temporal logic

Describes a project that uses

Uses Software

• TTM

This page was built for publication: A Cut-Free and Invariant-Free Sequent Calculus for PLTL

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