Sciweavers

Share
SLOGICA
1998

Encoding Modal Logics in Logical Frameworks

10 years 11 months ago
Encoding Modal Logics in Logical Frameworks
We present and discuss various formalizations of Modal Logics in Logical Frameworks based on Type Theories. We consider both Hilbert- and Natural Deductionstyle 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.
Arnon Avron, Furio Honsell, Marino Miculan, Cristi
Added 23 Dec 2010
Updated 23 Dec 2010
Type Journal
Year 1998
Where SLOGICA
Authors Arnon Avron, Furio Honsell, Marino Miculan, Cristian Paravano
Comments (0)
books