We present and discuss various formal]zations of Modal Logics in Logical Frameworks based on Type Theories. We consider both Hubert- and Natural Deductionstyle proof systems for representing both truth (local) and validity (global) consequence relations for various Modal Logics We introduce several techniques for encoding the structural peculiarities of necessitation rules, in the typed A-calculus metalanguage of the Logical Frameworks. These formalizations yield readily proof-editors for Modal Logics when implemented in Proof Development Environments, such as Coq or LEGO. © 1998 Kluwer Academic Publishers.
Encoding Modal Logics in Logical Frameworks
HONSELL, Furio;MICULAN, Marino;
1998-01-01
Abstract
We present and discuss various formal]zations of Modal Logics in Logical Frameworks based on Type Theories. We consider both Hubert- and Natural Deductionstyle proof systems for representing both truth (local) and validity (global) consequence relations for various Modal Logics We introduce several techniques for encoding the structural peculiarities of necessitation rules, in the typed A-calculus metalanguage of the Logical Frameworks. These formalizations yield readily proof-editors for Modal Logics when implemented in Proof Development Environments, such as Coq or LEGO. © 1998 Kluwer Academic Publishers.File in questo prodotto:
| File | Dimensione | Formato | |
|---|---|---|---|
|
SL98.pdf
accesso aperto
Tipologia:
Documento in Post-print
Licenza:
Creative commons
Dimensione
449.82 kB
Formato
Adobe PDF
|
449.82 kB | Adobe PDF | Visualizza/Apri |
I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.
