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.

Utilizza questo identificativo per citare o creare un link a questo documento: https://hdl.handle.net/11390/677200
Citazioni
  • ???jsp.display-item.citation.pmc??? ND
  • Scopus 24
  • ???jsp.display-item.citation.isi??? ND
social impact