Encoding modal logics in logical frameworks

DOI10.1023/A:1005060022386zbMath0954.03021OpenAlexW1541261556MaRDI QIDQ1577344

Cristian Paravano, Marino Miculan, Furio Honsell, Arnon Avron

Publication date: 14 February 2001

Published in: Studia Logica (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1023/a:1005060022386

zbMATH Keywords

proof systemsconsequence relationstyped \(\lambda\)-calculusproof assistantsformalizations of modal logics in logical frameworksnecessitation rulesproof development environmentstype theories

Mathematics Subject Classification ID

Modal logic (including the logic of norms) (03B45) Mechanization of proofs and logical operations (03B35) Combinatory logic and lambda calculus (03B40)

Related Items (12)

Towards Logical Frameworks in the Heterogeneous Tool Set Hets ⋮ On interactive proof-search for constructive modal necessity ⋮ Mechanizing common knowledge logic using COQ ⋮ Dual and axiomatic systems for constructive S4, a formally verified equivalence ⋮ Representing model theory in a type-theoretical logical framework ⋮ A logical framework combining model and proof theory ⋮ A natural deduction approach to dynamic logic ⋮ Representing Model Theory in a Type-Theoretical Logical Framework ⋮ Axiomatic and dual systems for constructive necessity, a formally verified equivalence ⋮ Proof-search in type-theoretic languages: An introduction ⋮ On the formalization of the modal \(\mu\)-calculus in the calculus of inductive constructions ⋮ A Framework for Defining Logical Frameworks

Uses Software

• Coq
• leanTAP

This page was built for publication: Encoding modal logics in logical frameworks