Encoding modal logics in logical frameworks
From MaRDI portal
Publication:1577344
DOI10.1023/A:1005060022386zbMath0954.03021MaRDI QIDQ1577344
Arnon Avron, Marino Miculan, Furio Honsell, Cristian Paravano
Publication date: 14 February 2001
Published in: Studia Logica (Search for Journal in Brave)
proof systems; consequence relations; typed \(\lambda\)-calculus; proof assistants; formalizations of modal logics in logical frameworks; necessitation rules; proof development environments; type theories
03B45: Modal logic (including the logic of norms)
03B35: Mechanization of proofs and logical operations
03B40: Combinatory logic and lambda calculus
Related Items
Proof-search in type-theoretic languages: An introduction, On the formalization of the modal \(\mu\)-calculus in the calculus of inductive constructions
Uses Software