For my Master’s thesis, I formalized the theory of dynamic epistemic logic in the Lean theorem prover. Lean is an open source proof assistant originally developed by Leonardo de Moura at Microsoft Research. It combines interactive theorem proving with automated reasoning capabilities in a dependently typed programming language called the Calculus of Inductive Constructions.
Dynamic epistemic logic (DEL) provides a framework for reasoning about how knowledge changes for systems of agents as communication events occur. Formalizations of DEL can be used for verification purposes within artificial intelligence, security, databases, and distributed computing.
My research involved:
-
a deep embedding of dynamic epistemic logic in Lean,
-
proof theoretic contributions, including soundness and completeness results for public announcement logic without common knowledge,
-
model theoretic contributions, including frame definability and undefinability results via invariance under disjoint unions, generated subframes, bisimulations, and surjective bounded morphisms.
See my formalization and my master’s thesis.
⟣⟣⟣ Some of my past research projects: ⟢⟢⟢
|
|
|
|
|
|
|
|