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|
|Keywords||Hilbert and Natural-Deduction proof systems for Modal Logics Logical Frameworks Typed λ-calculus Proof Assistants|
|Categories||categorize this paper)|
|Through your library||Configure|
Similar books and articles
Luca Viganò (2000). Labelled Non-Classical Logics. Kluwer Academic Publishers.
David Basin, Seán Matthews & Luca Viganò (1998). Labelled Modal Logics: Quantifiers. [REVIEW] Journal of Logic, Language and Information 7 (3):237-263.
Jc Beall, Ross Brady, Michael Dunn, Allen Hazen, Edwin Mares, John Slaney, Robert K. Meyer, Graham Priest, Greg Restall, David Ripley & Richard Sylvan (2012). On the Ternary Relation and Conditionality. Journal of Philosophical Logic 41 (3):595-612.
Marcus Kracht & Frank Wolter (1997). Simulation and Transfer Results in Modal Logic – a Survey. Studia Logica 59 (2):149-177.
Stéphane Demri & Dov Gabbay (2000). On Modal Logics Characterized by Models with Relative Accessibility Relations: Part II. Studia Logica 66 (3):349-384.
Roy A. Benton (2002). A Simple Incomplete Extension of T Which is the Union of Two Complete Modal Logics with F.M.P. Journal of Philosophical Logic 31 (6):527-541.
Added to index2009-01-28
Total downloads2 ( #246,081 of 722,857 )
Recent downloads (6 months)0
How can I increase my downloads?