2 papers
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…
cs.LO2016
On the Herbrand content of LK
Bahareh Afshari, Stefan Hetzl, Graham E. Leigh
We present a structural representation of the Herbrand content of LK-proofs with cuts of complexity prenex Sigma-2/Pi-2. The representation takes the form of a typed non-determinis…