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 | |