A Natural Deduction style proof system for propositional $μ$-calculus and its formalization in inductive type theories

Details A Natural Deduction style proof system for propositional $μ$-calculus and its formalization in inductive type theories A Natural Deduction style proof system for propositional $μ$-calculus and its formalization in inductive type theories

1998-09-29

arxiv.org/abs/cs/9809120v1

Computer Science

Logic in Computer Science

17 pages; longer version of the paper which will appear in Proc. ICTCS'98 (World Scientific)

Scientific paper

In this paper, we present a formalization of Kozen's propositional modal $\mu$-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 $\mu$-calculus. The techniques we adopted can be readily ported to other languages and proof systems featuring similar problematic issues.

Affiliated with

Also associated with

No associations

Rating

A Natural Deduction style proof system for propositional $μ$-calculus and its formalization in inductive type theories does not yet have a rating. At this time, there are no reviews or comments for this scientific paper.

If you have personal experience with A Natural Deduction style proof system for propositional $μ$-calculus and its formalization in inductive type theories, we encourage you to share that experience with our LandOfFree.com community. Your opinion is very important and A Natural Deduction style proof system for propositional $μ$-calculus and its formalization in inductive type theories will most certainly appreciate the feedback.

Rate now

Comments { 0 }

Profile ID: LFWR-SCP-O-51537