Formalized Soundness and Completeness of Epistemic Logic

Asta Halkjær From, Alexander Birch Jensen, Jørgen Villadsen

Research output: Chapter in Book/Report/Conference proceedingArticle in proceedingsResearchpeer-review

27 Downloads (Pure)

Abstract

Epistemic logic allows reasoning about the knowledge of agents, and deductive proof systems enable this reasoning with a few axioms and inference rules. We strengthen the logical foundations of such a system by formalizing it in the proof assistant Isabelle/HOL. Our definitions are given in the precise language of higher-order logic and every step of our soundness and completeness proofs is mechanically checked.
Original languageEnglish
Title of host publicationProceedings of International Workshop on Logical Aspects in Multi-Agent Systems and Strategic Reasoning
Number of pages3
Publication date2021
Publication statusPublished - 2021
EventInternational Workshop on Logical Aspects in Multi-Agent Systems and Strategic Reasoning -
Duration: 3 May 20214 May 2021

Workshop

WorkshopInternational Workshop on Logical Aspects in Multi-Agent Systems and Strategic Reasoning
Period03/05/202104/05/2021

Keywords

  • Epistemic Logic
  • Isabelle/HOL
  • Formal Proof
  • Agent Logic

Cite this