Aximo
Overview
Aximo is a tool for verifying knowledge in dynamic multi-agent scenarios. The underlying engine is based on the algebraic axiomatics of dynamic epistemic logic. It is the work of Simon Richards and Mehrnoosh Sadrzadeh.

Our paper on the system, 'Aximo: automated axiomatic reasoning for information update', is set to debut in November 2007 at the 5th Methods for Modalities (M4M) conference at the Ecole Normale Superieure de Cachan in France.
Updates
11th Feb 2008: Another update to the M4M5 conference paper has been uploaded.

30th Nov 2007: The M4M5 conference paper has been updated, and I've also uploaded the demonstration version of Aximo used at the conference (which has assumptions for the muddy children problem built in).

6th Nov 2007: Uploaded a version of the paper which is to be presented at M4M5 later this month.

14th Sept 2007: Appearance evaluation has been fixed to prevent duplicate states/actions from appearing, improving overall system performance. The input parser has been updated such that all input is now case insensitive and 'help' can be typed in most places to gain a quick reference of what needs to be inputted (syntax etc.). All builds have been updated with the changes.

13th Sept 2007: Fixed a bug which was preventing multiple nested parenthesis to be parsed properly. Additionally, the input checking has been improved to detect when a starting state/ending fact is not present in all decompositions of the inequality. Error messages for bad user input have been updated to reflect this addition. All builds have been updated with the changes.

7th Sept 2007: Compiles for Linux (x86) and Windows are added.
Downloads
Aximo has been developed primarily on OSX (on an Intel-based machine), so updates for this platform will usually appear first. Windows and Linux versions should work fine, but the OSX build has been more thoroughly tested.

Current Issues
Aximo is an ongoing development, so although it is in a working state, there are still a number of issues to be aware of: