Studia Logica 60 (1):161-208 (1998)
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
|Keywords||Hilbert and Natural-Deduction proof systems for Modal Logics Logical Frameworks Typed λ-calculus Proof Assistants|
|Categories||categorize this paper)|
References found in this work BETA
No references found.
Citations of this work BETA
No citations found.
Similar books and articles
A Simple Incomplete Extension of T Which is the Union of Two Complete Modal Logics with F.M.P.Roy A. Benton - 2002 - Journal of Philosophical Logic 31 (6):527-541.
On Modal Logics Characterized by Models with Relative Accessibility Relations: Part II.Stéphane Demri & Dov Gabbay - 2000 - Studia Logica 66 (3):349-384.
Simulation and Transfer Results in Modal Logic – a Survey.Marcus Kracht & Frank Wolter - 1997 - Studia Logica 59 (2):149-177.
Labelled Modal Logics: Quantifiers. [REVIEW]David Basin, Seán Matthews & Luca Viganò - 1998 - Journal of Logic, Language and Information 7 (3):237-263.
The Method of Hypersequents in the Proof Theory of Propositional Non-Classical Logics.Arnon Avron - unknown
Added to index2009-01-28
Total downloads35 ( #147,616 of 2,171,850 )
Recent downloads (6 months)1 ( #326,616 of 2,171,850 )
How can I increase my downloads?