Common knowledge logic in a higher order proof assistant

DOI10.1007/978-3-642-37651-1_11MaRDI QIDQ4916081zbMATH OpenOpenAlexFDO

Authors Pierre Lescanne

Publication date 19 April 2013

Published in Programming Logics (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1007/978-3-642-37651-1_11

Mathematics Subject Classification ID

Logics of knowledge and belief (including belief change) (03B42)

Recommendations

• Mechanizing common knowledge logic using COQ
• The proof theory of common knowledge
• scientific article; zbMATH DE number 2068679
• The coinductive formulation of common knowledge
• Two ways to common knowledge

Cites work

• Backward induction and common knowledge of rationality
• Cheating husbands and other stories: A case study of knowledge, action, and communication
• 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 786495 (Why is no real title available?)
• scientific article; zbMATH DE number 795590 (Why is no real title available?)
• Hypothetical knowledge and games with perfect information
• Interactive theorem proving and program development. Coq'Art: the calculus of inductive constructions. Foreword by Gérard Huet and Christine Paulin-Mohring.
• Linear logic
• Mechanizing common knowledge logic using COQ

Cited in

(6)

• The coinductive formulation of common knowledge
• Mechanizing common knowledge logic using COQ
• Common Knowledge Semantics of Armstrong’s Axioms
• Intuitionistic common knowledge or belief
• scientific article; zbMATH DE number 7117799 (Why is no real title available?)
• scientific article; zbMATH DE number 7668120 (Why is no real title available?)

Describes a project that uses

Uses Software

• Coq

This page was built for publication: Common knowledge logic in a higher order proof assistant

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