Encoding modal logics in logical frameworks

, , &
Studia Logica 60 (1):161-208 (1998)
  Copy   BIBTEX

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.

Categories

Keywords

Reprint years

DOI

10.1023/a:1005060022386

Other Versions

No versions found

Links

PhilArchive

External links

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

Through your library

My notes

Similar books and articles

Simple sequent systems for the modal logics K,D,T, and S4.Rea Golan - 2025 - Logic Journal of the IGPL 33 (3):1-24.
Admissibility of cut in congruent modal logics.Andrzej Indrzejczak - 2011 - Logic and Logical Philosophy 20 (3):189-203.
Proof systems for various fde-based modal logics.Sergey Drobyshevich & Heinrich Wansing - 2020 - Review of Symbolic Logic 13 (4):720-747.
Modal pure type systems.Tijn Borghuis - 1998 - Journal of Logic, Language and Information 7 (3):265-296.
Proof Theory for Functional Modal Logic.Shawn Standefer - 2018 - Studia Logica 106 (1):49-84.
Labelled modal logics: Quantifiers. [REVIEW]David Basin, Seán Matthews & Luca Viganò - 1998 - Journal of Logic, Language and Information 7 (3):237-263.
Hypersequent Calculi for Modal Logics.Samara Elizabeth Burns - unknown
Fitch-style natural deduction for modal paralogics.Hans Lycke - 2009 - Logique Et Analyse 52 (207):193-218.
Automated Proof Search in Non-classical Logics: Efficient Matrix Proof Methods for Modal and Intuitionistic Logics.Lincoln A. Wallen - 1990 - MIT Press (MA).
Proof Methods for Modal and Intuitionistic Logics.Melvin Chris Fitting - 1983 - Dordrecht and Boston: Reidel.

Analytics

Added to PP
2009-01-28

Downloads
168 (#245,508)

6 months
25 (#388,002)

Historical graph of downloads
How can I increase my downloads?

Author's Profile

Photo of Arnon Avron
Arnon Avron
Tel Aviv University

Citations of this work

Modal Hybrid Logic.Andrzej Indrzejczak - 2007 - Logic and Logical Philosophy 16 (2-3):147-257.

View all 6 citations / Add more citations

References found in this work

The collected papers of Gerhard Gentzen.Gerhard Gentzen - 1969 - Amsterdam,: North-Holland Pub. Co.. Edited by M. E. Szabo.
Modal logic and classical logic.Johan van Benthem - 1983 - Atlantic Highlands, N.J.: Distributed in the U.S.A. by Humanities Press.
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.
Simple consequence relations.Arnon Avron - 1991 - Information And Computation 92 (1):105–139.

View all 16 references / Add more references