arXiv subjects

Bahareh Afshari

Publications and source records attributed to Bahareh Afshari.

5 recordsLinked to original sources

arXiv2025

The Limit of Recursion in State-based Systems

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 the previously claimed result by the first and third authors on closure ordinals of the alternation-free mu-calculus in [3]. The new approach sees a reincarnation of Kozen's well-annotations, devised for showing the finite model property for the modal mu-calculus. We develop a theory of 'conservative' well-annotations where minimality of annotations is guaranteed, and isolate parts of the structure that locally determine the closure ordinal of relevant formulas. This adoption of well-annotations enables a direct and clear pumping process that rules out closure ordinals between omega^2 and the limit of countability.

cs.LO↗

arXiv2025

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

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.

cs.LO↗

arXiv2025

Cut-elimination for the alternation-free modal mu-calculus

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 are finitely branching but may be non-wellfounded. The structure of such proofs is exploited to directly transform a cyclic proof with cuts into a cut-free one, without detouring through other logics or relying on intermediate machinery for regularisation. Novel ingredients include the use of multicuts and results from the theory of well-quasi-orders, the later used in the termination argument.

cs.LO↗

arXiv2025

Demystifying $μ$

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 provides a novel bridge between finitary, cyclic and illfounded conceptions of proof and re-enforces the importance of two normal form theorems for the logic: guardedness and disjunctiveness.

math.LO↗

arXiv2016

On the Herbrand content of LK

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-deterministic tree grammar of order 2 which generates a finite language of first-order terms that appear in the Herbrand expansions obtained through cut-elimination. In particular, for every Gentzen-style reduction between LK-proofs we study the induced grammars and classify the cases in which language equality and inclusion hold.

cs.LO↗