University of Oxford Logo University of OxfordDepartment of Computer Science - Home

Aximo: Automated Axiomatic Reasoning for Information Update

Simon Richards and Mehrnoosh Sadrzadeh

Abstract

We present an algorithm for proving epistemic properties of dynamic scenarios in multi-agent systems and an implementation of it as the C++ program Aximo. The program consists of a rewrite system and a recursive reasoner, and we prove that its decision procedure is sound with regard to the algebraic axiomatics of dynamic epistemic logic. We study the termination and complexity of the program and show its applicability, by proving properties of honest and also newer dishonest versions of the the muddy children puzzle as well as a coin toss scenario.

Details

Journal

Electronic Notes in Theoretical Computer Science (ENTCS)

Year

2009

Links

BibTeX

Download  (pdf)

Related pages

People