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

DOI10.1007/978-3-540-74915-8_36zbMath1179.03056OpenAlexW1871326816MaRDI QIDQ3608433

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

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)

Related Items

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

Uses Software

• TTM