dc.contributor.author Afshari, Bahareh dc.contributor.author Leigh, Graham E. dc.date.accessioned 2017-02-07T08:41:10Z dc.date.available 2017-02-07T08:41:10Z dc.date.issued 2016-12-30 dc.identifier.uri http://publications.mfo.de/handle/mfo/1275 dc.description Research in Pairs 2016 en_US dc.description.abstract We present three finitary cut-free sequent calculi for the modal $μ$-calculus. Two of these derive annotated sequents in the style of Stirling’s ‘tableau proof system with names’ (2014) 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 $ν$-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 $μ$-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. en_US dc.language.iso en_US en_US dc.publisher Mathematisches Forschungsinstitut Oberwolfach en_US dc.relation.ispartofseries Oberwolfach Preprints;2016,26 dc.title Finitary Proof Systems for Kozen's μ en_US dc.type Preprint en_US dc.identifier.doi 10.14760/OWP-2016-26 local.scientificprogram Research in Pairs 2016 en_US local.series.id OWP-2016-26 dc.identifier.urn urn:nbn:de:101:1-20170103958 dc.identifier.ppn 165516290X
﻿