We present a natural deduction proof system for the propositional modal μ-calculus and its formalization in the calculus of inductive constructions. We address several problematic issues, such as the use of higher-order abstract syntax in inductive sets in the presence of recursive constructors, and the formalization of modal (sequent-style) rules and of context sensitive grammars. The formalization can be used in the system Coq, providing an experimental computer-aided proof environment for the interactive development of error-free proofs in the modal μ-calculus. The techniques we adopt can be readily ported to other languages and proof systems featuring similar problematic issues. © 2001 Academic Press.
On the formalization of the modal mu-calculus in the calculus of inductive constructions
MICULAN, Marino
2001-01-01
Abstract
We present a natural deduction proof system for the propositional modal μ-calculus and its formalization in the calculus of inductive constructions. We address several problematic issues, such as the use of higher-order abstract syntax in inductive sets in the presence of recursive constructors, and the formalization of modal (sequent-style) rules and of context sensitive grammars. The formalization can be used in the system Coq, providing an experimental computer-aided proof environment for the interactive development of error-free proofs in the modal μ-calculus. The techniques we adopt can be readily ported to other languages and proof systems featuring similar problematic issues. © 2001 Academic Press.| File | Dimensione | Formato | |
|---|---|---|---|
|
IC01.pdf
non disponibili
Tipologia:
Documento in Post-print
Licenza:
Non pubblico
Dimensione
391.17 kB
Formato
Adobe PDF
|
391.17 kB | Adobe PDF | Visualizza/Apri Richiedi una copia |
I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.
