Article ID | Journal | Published Year | Pages | File Type |
---|---|---|---|---|
431081 | The Journal of Logic and Algebraic Programming | 2008 | 23 Pages |
Abstract
This paper presents a new model construction for a natural cut-free infinitary version of the propositional modal μ-calculus. Based on that the completeness of and the related system Kω(μ) can be established directly – no detour, for example through automata theory, is needed. As a side result we also obtain a finite, cut-free sound and complete system for the propositional modal μ-calculus.
Related Topics
Physical Sciences and Engineering
Computer Science
Computational Theory and Mathematics