Encoding modal logics in logical frameworks

Studia Logica 60 (1):161-208 (1998)

Abstract

We present and discuss various formalizations of Modal Logics in Logical Frameworks based on Type Theories. We consider both Hilbert- and Natural Deduction-style 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 -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

Download options

PhilArchive



    Upload a copy of this work     Papers currently archived: 72,766

External links

Setup an account with your affiliations in order to access resources via your University's proxy server

Through your library

Analytics

Added to PP
2009-01-28

Downloads
63 (#185,180)

6 months
1 (#386,989)

Historical graph of downloads
How can I increase my downloads?

Author's Profile

Arnon Avron
Tel Aviv University

References found in this work

A Natural Extension of Natural Deduction.Peter Schroeder-Heister - 1984 - Journal of Symbolic Logic 49 (4):1284-1300.
[Omnibus Review].Dag Prawitz - 1991 - Journal of Symbolic Logic 56 (3):1094-1096.
A Companion to Modal Logic.G. E. Hughes & M. J. Cresswell - 1995 - Studia Logica 54 (3):411-413.
Tableaus for Many-Valued Modal Logic.Melvin Fitting - 1995 - Studia Logica 55 (1):63 - 87.

View all 9 references / Add more references