Browsing by Author "Afshari, Bahareh"

Now showing 1 - 2 of 2
  • Thumbnail Image
    Item
    Finitary proof systems for Kozen’s μ.
    (Oberwolfach : Mathematisches Forschungsinstitut Oberwolfach, 2016) Afshari, Bahareh; Leigh, Graham E.
    We present three finitary cut-free sequent calculi for the modal [my]-calculus. Two of these derive annotated sequents in the style of Stirling’s ‘tableau proof system with names’ (4236) and feature special inferences that discharge open assumptions. The third system is a variant of Kozen’s axiomatisation in which cut is replaced by a strengthening of the v-induction inference rule. Soundness and completeness for the three systems is proved by establishing a sequence of embeddings between the calculi, starting at Stirling’s tableau-proofs and ending at the original axiomatisation of the [my]-calculus due to Kozen. As a corollary we obtain a completeness proof for Kozen’s axiomatisation which avoids the usual detour through automata or games.
  • Thumbnail Image
    Item
    Herbrand's Theorem as Higher Order Recursion
    (Oberwolfach : Mathematisches Forschungsinstitut Oberwolfach, 2018) Afshari, Bahareh; Hetzl, Stefan; Leigh, Graham E.
    We provide a means to compute Herbrand disjunctions directly from sequent calculus proofs with cuts. Our approach associates to a first-order classical proof π + ∃vF, where F is quantifier free, an acyclic higher order recursion scheme H whose language is finite and yields a Herbrand disjunction for ∃vF. More generally, we show that the language of H contains the Herbrand disjunction implicit in any cut-free proof obtained from π via a sequence of Gentzen-style cut reductions that always reduce the weak side of a cut before the strong side.