Sequent systems for PLTL

MaRDI QIDQ2799620zbMATH OpenFDO

Authors Romas Alonderis, R. Pliuškevičius

Publication date 13 April 2016

Published in Lietuvos Matematikos Rinkinys. Proceedings of the Lithuanian Mathematical Society. Series A (Search for Journal in Brave)

zbMATH Keywords

\(\omega\)-type ruleinvariant-like rulelooping axiomssequent calculitemporal logicsweak-induction rule

Mathematics Subject Classification ID

Temporal logic (03B44) Proof theory in general (including proof-theoretic semantics) (03F03) Structure of proofs (03F07)

Recommendations

• Loop-type sequent calculi for temporal logic
• Systematic semantic tableaux for PLTL
• PTL sequent calculus system
• A Cut-Free and Invariant-Free Sequent Calculus for PLTL
• Cut, invariant rule, and loop-check free sequent calculus for PLTL

Cited in

(14)

• Dual systems of tableaux and sequents for PLTL
• PTL sequent calculus system
• Loop-type sequent calculi for temporal logic
• Propositional linear temporal logic with initial validity semantics
• Cut, invariant rule, and loop-check free sequent calculus for PLTL
• Systematic semantic tableaux for PLTL
• Natural Deduction Calculus for Linear-Time Temporal Logic
• A Cut-Free and Invariant-Free Sequent Calculus for PLTL
• Decidability for Priorean linear time using a fixed-point labelled calculus
• An Axiomatization of Linear Temporal Logic in the Calculus of Inductive Constructions
• Finite sequent calculi for PLTL
• More efficient proof-search for sequents of temporal logic
• A finitary-language semantics for propositional linear temporal logic
• Loop-check free sequent calculi for unary fragment of temporal logic

This page was built for publication: Sequent systems for PLTL

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