More efficient proof-search for sequents of temporal logic

DOI10.15388/LMR.2022.29752MaRDI QIDQ5058432zbMATH OpenFDO

Authors Romas Alonderis

Publication date 20 December 2022

Published in Lietuvos matematikos rinkinys (Search for Journal in Brave)

Full work available at URL https://doi.org/10.15388/LMR.2022.29752

zbMATH Keywords

backward proof-searchloop-type sequent calculitemporal logics

Mathematics Subject Classification ID

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

Recommendations

• Restrictions for loop-check in sequent calculus for temporal logic
• Sequent systems for PLTL
• PTL sequent calculus system
• Loop-type sequent calculi for temporal logic
• Cut, invariant rule, and loop-check free sequent calculus for PLTL

Cites work

• A completeness proof for an infinitary tense-logic
• A Cut-Free and Invariant-Free Sequent Calculus for PLTL
• Cut-free sequent systems for temporal logic
• Cyclic Proofs for Linear Temporal Logic
• Decision complexity of variants of propositional dynamic logic
• scientific article; zbMATH DE number 4170873 (Why is no real title available?)
• scientific article; zbMATH DE number 3937153 (Why is no real title available?)
• scientific article; zbMATH DE number 1189110 (Why is no real title available?)
• scientific article; zbMATH DE number 1333594 (Why is no real title available?)
• scientific article; zbMATH DE number 5585443 (Why is no real title available?)
• Loop-type sequent calculi for temporal logic

Cited in

(2)

• Search strategies for resolution in temporal logics
• scientific article; zbMATH DE number 2090535 (Why is no real title available?)

Describes a project that uses

Uses Software

• TTM

This page was built for publication: More efficient proof-search for sequents of temporal logic

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