Speaker
Armand Feuilleaubois
Universität Bern
Talks at this conference:
Friday, 16:55, J330 
Cyclic cut elimination for the stratified fragment of the modal μcalculus 
Authors: Armand Feuilleaubois and Thomas Studer Kloibhofer and Afshari presented in [1] a new cut elimination procedure for annotated cyclic proofs of a temporal modal logic using only the eventually operator, \(F\). This method has the advantage of preserving the regularity of the proof throughout the cut elimination process. We present a cut elimination procedure for the stratified fragment of the modal \(\mu\)calculus, based on the method of Kloibhofer and Afshari in [1]. The stratified fragment of the modal \(\mu\)calculus, as defined by Jäger, Kretz, and Studer in [2], is the fragment such that formulas \(\mu X.\mathcal{A}[X]\), \(\nu X.\mathcal{A}[X]\), with \(\mathcal{A}[X]\) positive in the variable \(X\), may only contain subformulas \(\mu Y.\mathcal{B}[Y]\), \(\nu Y.\mathcal{B}[Y]\) where \(X\) does not appear as a free variable. Thus, the meaning of an inner nested fixed point will not depend on the outer fixed point within which it is nested. This fragment itself contains as fragments CTL, PDL, and the logic of common knowledge. Thus, we also obtain cut elimination for these fragments. Bibliography
