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 language | English |
|---|---|
| Title of host publication | Proceedings of International Workshop on Logical Aspects in Multi-Agent Systems and Strategic Reasoning |
| Number of pages | 3 |
| Publication date | 2021 |
| Publication status | Published - 2021 |
| Event | International Workshop on Logical Aspects in Multi-Agent Systems and Strategic Reasoning - Duration: 3 May 2021 → 4 May 2021 |
Workshop
| Workshop | International Workshop on Logical Aspects in Multi-Agent Systems and Strategic Reasoning |
|---|---|
| Period | 03/05/2021 → 04/05/2021 |
Keywords
- Epistemic Logic
- Isabelle/HOL
- Formal Proof
- Agent Logic