13 October 2015, Logic Tea, Malvin Gattinger

Abstract

Dynamic Epistemic Logic (DEL) can model puzzles and complex information scenarios in a way that appeals to logicians. However, not much work on efficient implementations has been done and we do not know how the DEL framework performs in practice. In contrast, much progress has been made in
model checking for temporal logics. To use these ideas and move from explicit to symbolic model checking we provide a truth-preserving representation of Kripke models as knowledge structures with observational variables. On these structures we can translate every DEL formula to a boolean equivalent represented as a binary decision diagram (BDD).

The talk will first introduce a few logic puzzles and then give an introduction to DEL and symbolic model checking with BDDs. Finally, we show how large instances of the puzzles can be solved in a few seconds with our software.

For more information, please visit the website http://www.illc.uva.nl/logic_tea/ or contact Thomas Brochhagen (t.s.brochhagen at uva.nl), Johannes Marti (johannes.marti at gmail.com), Masa Mocnik (masa.mocnik at gmail.com) or Julian Schloder (julian.schloeder at gmail.com).