4 papers
The Limit of Recursion in State-based Systems
Bahareh Afshari, Giacomo Barlucchi, Graham E. Leigh
We prove that omega^2 strictly bounds the iterations required for modal definable functions to reach a fixed point across all countable structures. The result corrects and extends…
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…
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…
Demystifying
Bahareh Afshari, Graham E. Leigh, Guillermo Menèndez Turata
We explore the theory of illfounded and cyclic proofs for the propositional modal -calculus. A fine analysis of provability for classical and intuitionistic modal logic provide…