Mechanizing common knowledge logic using COQ

DOI10.1007/S10472-006-9042-1MaRDI QIDQ2643149zbMATH OpenOpenAlexFDO

Authors 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

Common knowledge logicCOQEpistemic logicHigher order common knowledge logicModalities

Mathematics Subject Classification ID

Mechanization of proofs and logical operations (03B35) Logics of knowledge and belief (including belief change) (03B42) Logic in artificial intelligence (68T27)

Recommendations

• Common knowledge logic in a higher order proof assistant
• The coinductive formulation of common knowledge
• The proof theory of common knowledge
• Two ways to common knowledge
• scientific article; zbMATH DE number 2068679

Cites work

• A formal semantics for SPKI
• A framework for defining logical frameworks
• A guide to completeness and complexity for modal logics of knowledge and belief
• A study of Kripke-type models for some modal logics by Gentzen's sequential method
• About cut elimination for logics of common knowledge
• Agreeing to disagree
• An Axiomatic Characterization of Common Knowledge
• Backward induction and common knowledge of rationality
• Common knowledge logic and game logic
• Common knowledge: Relating anti-founded situation semantics to modal logic neighbourhood semantics
• Constructivism in mathematics. An introduction. Volume II
• Deterministic propositional dynamic logic: finite models, complexity, and completeness
• Encoding modal logics in logical frameworks
• Games in dynamic-epistemic logic
• scientific article; zbMATH DE number 1234441 (Why is no real title available?)
• scientific article; zbMATH DE number 1556014 (Why is no real title available?)
• scientific article; zbMATH DE number 754675 (Why is no real title available?)
• scientific article; zbMATH DE number 795590 (Why is no real title available?)
• scientific article; zbMATH DE number 824735 (Why is no real title available?)
• scientific article; zbMATH DE number 234014 (Why is no real title available?)
• scientific article; zbMATH DE number 274399 (Why is no real title available?)
• scientific article; zbMATH DE number 3359806 (Why is no real title available?)
• Interactive theorem proving and program development. Coq'Art: the calculus of inductive constructions. Foreword by Gérard Huet and Christine Paulin-Mohring.
• Labelled modal logics: Quantifiers
• Labelled propositional modal logics: theory and practice
• Logic and structure.
• Propositional dynamic logic of regular programs
• The propositional dynamic logic of deterministic, well-structured programs

Cited in

(5)

• The coinductive formulation of common knowledge
• Saturation method for reflexive common knowledge logic
• Common knowledge logic in a higher order proof assistant
• scientific article; zbMATH DE number 7117799 (Why is no real title available?)
• Mechanizing bisimulation theorems for relation-changing logics in Coq

Describes a project that uses

Uses Software

• HOL
• Coq
• ML

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

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