BEGIN:VCALENDAR
VERSION:2.0
PRODID:-//University of Liverpool Computer Science Seminar System//v2//EN
BEGIN:VEVENT
DTSTAMP:20260920T141618Z
UID:Seminar-dept-283@lxserverM.csc.liv.ac.uk
ORGANIZER:CN=Lutz Oettershagen:MAILTO:Lutz.Oettershagen@liverpool.ac.uk
DTSTART:20120424T150000
DTEND:20120424T160000
SUMMARY:School Seminar Series
DESCRIPTION:Dr. Mehrnoosh Sadrzadeh: Automated Theorem Proving for a Fragment of Dynamic Epistemic Logic with Public and Private Announcements\n\nDynamic Epistemic Logic (DEL) is a logic of actions and propositions\nenriched with epistemic modalities. It can reason about properties of\nmulti-agent scenarios, where agents communicate via honest/dishonest\npublic and private announcements and as a result their knowledge and\nbelief gets updated. The original logical theory of DEL is based on a\nHilbert-style axiomatization, hence it is not very powerful when it\ncomes to automate the logical reasoning. The existing  automated\nreasoners of DEL are all semantic-based and rely on model checking\ntechniques, which suffer from the usual  state explosion problems.\n\nIn this talk I  will present a Gentzen-style sequent calculus for a\nnegation-free fragment of Dynamic Epistemic Logic. Apart from the\nlogical and structural rules, the calculus also has assumption rules\nto encode the specifics of scenarios (accessibility relations, action\nmodels, preconditions) and reason about each scenario individually.\nThe calculus is cut-free, sound, and complete, and its proof rules\nhave been implemented in Haskell.  It can automatically solve puzzles\nsuch as muddy children and consecutive numbers, and their variants\nwith dishonest public and private announcements.  Time permitting, I\nwill discuss extensions to the full fragment which includes negation.\n\nJoint work with Roy Dyckhoff and Julien Truffaut\n\nhttps://www.csc.liv.ac.uk/research/seminars/abstract.php?id=283
LOCATION:Ashton Lecture Theatre
END:VEVENT
END:VCALENDAR