A Natural Deduction style proof system for propositional $\mu$-calculus and its formalization in inductive type theories
Logic in Computer Science
2007-05-23 v1
Abstract
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.
Keywords
Cite
@article{arxiv.cs/9809120,
title = {A Natural Deduction style proof system for propositional $\mu$-calculus and its formalization in inductive type theories},
author = {Marino Miculan},
journal= {arXiv preprint arXiv:cs/9809120},
year = {2007}
}
Comments
17 pages; longer version of the paper which will appear in Proc. ICTCS'98 (World Scientific)