Show simple item record

dc.contributor.authorAfshari, Bahareh
dc.contributor.authorLeigh, Graham E.
dc.date.accessioned2017-02-07T08:41:10Z
dc.date.available2017-02-07T08:41:10Z
dc.date.issued2016-12-30
dc.identifier.urihttp://publications.mfo.de/handle/mfo/1275
dc.descriptionResearch in Pairs 2016en_US
dc.description.abstractWe 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.isoen_USen_US
dc.publisherMathematisches Forschungsinstitut Oberwolfachen_US
dc.relation.ispartofseriesOberwolfach Preprints;2016,26
dc.titleFinitary Proof Systems for Kozen's μen_US
dc.typePreprinten_US
dc.identifier.doi10.14760/OWP-2016-26
local.scientificprogramResearch in Pairs 2016en_US
local.series.idOWP-2016-26
dc.identifier.urnurn:nbn:de:101:1-20170103958
dc.identifier.ppn165516290X


Files in this item

Thumbnail

This item appears in the following Collection(s)

Show simple item record