Cut elimination for Cyclic Proofs: A Case Study in Temporal Logic

2024/05/03 by Afshari, Bahareh, Kloibhofer, Johannes · 3 citations
#FOS: Computer and information sciences #FOS: Mathematics #Logic (math.LO) #Logic in Computer Science (cs.LO)

paper · doi:10.48550/arxiv.2405.01935

Abstract

We consider modal logic extended with the well-known temporal operator 'eventually' and provide a cut-elimination procedure for a cyclic sequent calculus that captures this fragment. The work showcases an adaptation of the reductive cut-elimination method to cyclic calculi. Notably, the proposed algorithm applies to a cyclic proof and directly outputs a cyclic cut-free proof without appealing to intermediate machinery for regularising the end proof.

Cited by

• Uniform interpolation for interpretability logic
• Cut-elimination for the alternation-free modal mu-calculus
• Coalgebraic proof translations for non-wellfounded proofs

Related

• A study of cut-elimination for a non-labelled cyclic proof system for propositional dynamic logics
• Cut-elimination for the alternation-free modal mu-calculus
• A study for recovering the cut-elimination property in cyclic proof systems by restricting the arity of inductive predicates
• Cut elimination for a non-wellfounded system for the master modality
• Cut elimination for propositional cyclic proof systems with fixed-point operators