Encoding modal logics in logical frameworks

DOI10.1023/A:1005060022386MaRDI QIDQ1577344zbMATH OpenOpenAlexFDO

Authors Arnon Avron, Furio Honsell, Marino Miculan, Cristian Paravano

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, http://hdl.handle.net/11390/677200

zbMATH Keywords

consequence relationsformalizations of modal logics in logical frameworksnecessitation rulesproof assistantsproof development environmentsproof systemstype theoriestyped \(\lambda\)-calculus

Mathematics Subject Classification ID

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

Recommendations

• scientific article; zbMATH DE number 1523046
• Modal multilattice logic
• scientific article; zbMATH DE number 1471992
• CONCUR 2004 - Concurrency Theory
• scientific article; zbMATH DE number 125988
• Modal logic for rewriting theories
• Modal bilattice logic and its extensions
• Modal logics, justification logics, and realization
• Modal logics for qualitative possibility theory
• scientific article; zbMATH DE number 4012571

Cited in

(23)

• Proof-search in type-theoretic languages: An introduction
• On the formalization of the modal -calculus in the calculus of inductive constructions
• Relative properties of frame language
• A general framework for FDE-based modal logics
• On interactive proof-search for constructive modal necessity
• Dual and axiomatic systems for constructive S4, a formally verified equivalence
• Mechanizing common knowledge logic using COQ
• Comparing higher-order encodings in logical frameworks and tile logic
• A framework for defining logical frameworks
• Towards logical frameworks in the heterogeneous tool set Hets
• A modal Θ-valent approach of the notion of code
• scientific article; zbMATH DE number 1936763 (Why is no real title available?)
• scientific article; zbMATH DE number 1523046 (Why is no real title available?)
• scientific article; zbMATH DE number 1775492 (Why is no real title available?)
• A natural deduction approach to dynamic logic
• Brodskio kodavimo metodas teiginių logikai;Brodsky’s coding method for propositional logic
• Representing model theory in a type-theoretical logical framework
• Higher-order representation of substructural logics
• Axiomatic and dual systems for constructive necessity, a formally verified equivalence
• A logical framework combining model and proof theory
• Encoding type universes without using matching modulo associativity and commutativity
• Representing model theory in a type-theoretical logical framework
• A monadic formalization of ML5

Describes a project that uses

Uses Software

• Coq
• leanTAP

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

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q1577344)