We present a theoretical and practical approach to the modular natural deduction presentation of modal logics and their implementation in a logical framework. Our work treats a large and well-known class of modal logics (including K, D, T , B, S4, S4:2, KD45, S5) in a uniform way with respect to soundness and completeness for semantics, and faithfulness and adequacy of the implementation. Moreover, it results in a pleasingly simple and usable implementation of these logics.

A Modular Presentation of Modal Logics in a Logical Framework

VIGANO', Luca
1998

Abstract

We present a theoretical and practical approach to the modular natural deduction presentation of modal logics and their implementation in a logical framework. Our work treats a large and well-known class of modal logics (including K, D, T , B, S4, S4:2, KD45, S5) in a uniform way with respect to soundness and completeness for semantics, and faithfulness and adequacy of the implementation. Moreover, it results in a pleasingly simple and usable implementation of these logics.
1575860988
1575860996
Modal logics; logical frameworks; proof theory
File in questo prodotto:
Non ci sono file associati a questo prodotto.

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/11562/243775
Citazioni
  • ???jsp.display-item.citation.pmc??? ND
  • Scopus ND
  • ???jsp.display-item.citation.isi??? ND
social impact