Automated Theorem Proving for a Fragment of Dynamic Epistemic Logic with Public and Private Announcements

24^th April 2012, 15:00 Ashton Lecture Theatre
Dr. Mehrnoosh Sadrzadeh
Dept of Computer Science
University of Oxford
UK

Abstract

Dynamic Epistemic Logic (DEL) is a logic of actions and propositions
enriched with epistemic modalities. It can reason about properties of
multi-agent scenarios, where agents communicate via honest/dishonest
public and private announcements and as a result their knowledge and
belief gets updated. The original logical theory of DEL is based on a
Hilbert-style axiomatization, hence it is not very powerful when it
comes to automate the logical reasoning. The existing automated
reasoners of DEL are all semantic-based and rely on model checking
techniques, which suffer from the usual state explosion problems.

In this talk I will present a Gentzen-style sequent calculus for a
negation-free fragment of Dynamic Epistemic Logic. Apart from the
logical and structural rules, the calculus also has assumption rules
to encode the specifics of scenarios (accessibility relations, action
models, preconditions) and reason about each scenario individually.
The calculus is cut-free, sound, and complete, and its proof rules
have been implemented in Haskell. It can automatically solve puzzles
such as muddy children and consecutive numbers, and their variants
with dishonest public and private announcements. Time permitting, I
will discuss extensions to the full fragment which includes negation.

Joint work with Roy Dyckhoff and Julien Truffaut