Mechanizing common knowledge logic using COQ

DOI10.1007/s10472-006-9042-1zbMath1122.03007OpenAlexW2001676074MaRDI QIDQ2643149

Pierre Lescanne

Publication date: 23 August 2007

Published in: Annals of Mathematics and Artificial Intelligence (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1007/s10472-006-9042-1

zbMATH Keywords

Epistemic logicModalitiesCommon knowledge logicCOQHigher order common knowledge logic

Mathematics Subject Classification ID

Related Items (1)

Common Knowledge Logic in a Higher Order Proof Assistant

Uses Software

• Coq
• ML
• HOL

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Interactive theorem proving and program development. Coq'Art: the calculus of inductive constructions. Foreword by Gérard Huet and Christine Paulin-Mohring.
• The propositional dynamic logic of deterministic, well-structured programs
• Constructivism in mathematics. An introduction. Volume II
• A guide to completeness and complexity for modal logics of knowledge and belief
• Agreeing to disagree
• A study of Kripke-type models for some modal logics by Gentzen's sequential method
• Propositional dynamic logic of regular programs
• Labelled modal logics: Quantifiers
• Encoding modal logics in logical frameworks
• About cut elimination for logics of common knowledge
• Deterministic propositional dynamic logic: finite models, complexity, and completeness
• Backward induction and common knowledge of rationality
• Common knowledge: Relating anti-founded situation semantics to modal logic neighbourhood semantics
• A Framework for Defining Logical Frameworks
• Games in Dynamic-Epistemic Logic
• An Axiomatic Characterization of Common Knowledge
• Common knowledge logic and game logic
• Labelled propositional modal logics: theory and practice
• A Formal Semantics for SPKI
• Logic and structure.

This page was built for publication: Mechanizing common knowledge logic using COQ