Restrictions for loop-check in sequent calculus for temporal logic

zbMATH Open1344.03020MaRDI QIDQ2811591FDOQ2811591

Authors: Adomas Birštunas 

Publication date: 10 June 2016

Published in: Lietuvos Matematikos Rinkinys. Lietuvos Matematiku Draugijos Darbai (Search for Journal in Brave)

Recommendations

• Restrictions for loop-check in sequent calculus for temporal logic with until operator
• Loop-check specification for a sequent calculus of temporal logic
• Loop-type sequent calculi for temporal logic
• Specialization of loop rules of a sequent calculus of intuitionistic temporal logic with time gaps
• Infinitary calculus without loop rules for restricted sequents of the first-order linear temporal logic
• A derivation-loop method for temporal logic
• scientific article; zbMATH DE number 1502114
• Reasoning in a restricted temporal logic
• Constraining cycle alternations in model checking for interval temporal logic
• Temporal Logics for Concurrent Recursive Programs: Satisfiability and Model Checking

zbMATH Keywords

temporal logicsequent calculusefficient loop-check

Mathematics Subject Classification ID

Temporal logic (03B44)

Cited In (7)

• Restrictions for loop-check in sequent calculus for temporal logic with until operator
• Cut, invariant rule, and loop-check free sequent calculus for PLTL
• More efficient proof-search for sequents of temporal logic
• Loop-check specification for a sequent calculus of temporal logic
• Method of marks for propositional linear temporal logic
• Specialization of loop rules of a sequent calculus of intuitionistic temporal logic with time gaps
• Efficient loop-check for KD45 logic

This page was built for publication: Restrictions for loop-check in sequent calculus for temporal logic

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