2 papers
cs.LO2025
Cut elimination for Cyclic Proofs: A Case Study in Temporal Logic
Bahareh Afshari, Johannes Kloibhofer
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 fragmen…
cs.LO2025
Cut-elimination for the alternation-free modal mu-calculus
Bahareh Afshari, Johannes Kloibhofer
We present a syntactic cut-elimination procedure for the alternation-free fragment of the modal mu-calculus. Cut reduction is carried out within a cyclic proof system, where proofs…