A Natural Deduction style proof system for propositional $μ$-calculus and its formalization in inductive type theories
| dc.creator | Miculan, Marino | |
| dc.date | 1998-09-29 | |
| dc.date.accessioned | 2026-07-07T03:23:42Z | |
| dc.date.available | 2026-07-07T03:23:42Z | |
| dc.description | In this paper, we present a formalization of Kozen's propositional modal $μ$-calculus, in the Calculus of Inductive Constructions. We address several problematic issues, such as the use of higher-order abstract syntax in inductive sets in presence of recursive constructors, the encoding of modal (``proof'') rules and of context sensitive grammars. The encoding can be used in the \Coq system, providing an experimental computer-aided proof environment for the interactive development of error-free proofs in the $μ$-calculus. The techniques we adopted can be readily ported to other languages and proof systems featuring similar problematic issues. | |
| dc.description | 17 pages; longer version of the paper which will appear in Proc. ICTCS'98 (World Scientific) | |
| dc.identifier | https://arxiv.org/abs/cs/9809120 | |
| dc.identifier | http://arxiv.org/abs/cs/9809120 | |
| dc.identifier.uri | http://salesiana.dossiersoluciones.com/handle/123456789/33047 | |
| dc.subject | Logic in Computer Science | |
| dc.subject | D.2.4; F.3.1; F.4.1 | |
| dc.title | A Natural Deduction style proof system for propositional $μ$-calculus and its formalization in inductive type theories | |
| dc.type | text |