Aximo: Automated Axiomatic Reasoning for Information Update

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.