Requires a Java-enabled browser

The default set of agents are the agents appearing in knowledge operators. If no knowledge operators are present in the formula then set of agents will contain a single agent.
Check Extra Agent to add a new agent (not appearing in the formula) to the default set. From this follows checking Extra Agent guarantees that there are at least two agents in the agent set.

Mac users: You have to reload the page before you can copy from the text fields.

The algorithm presented here is an implementation of the procedure specified in this paper by Valentin Goranko and Dmitry Shkatov. The paper by the same authors which gives a tableau-based decision procedure for the full coalition multi-agent epistemic logic may also be of interest.

Syntax: (White space is ignored)
  • formula => formula - Implication (Extended parser only)
  • formula v formula - Disjunction (Extended parser only)
  • formula & formula - Conjunction
  • K[ agent ] formula - Knowledge
  • ( formula ) - Parenthesis, for grouping
  • ! formula - Not
  • C formula - Common Knowledge
  • D formula - Distributive Knowledge
  • Propositions are words which starts with p,q or r and can optionally have any amount of digits after it. The regular expression [pqr][0-9]* is used. (Case insensitive)
  • Agents are words which starts with a,b or c and can optionally have any amount of digits after it. The regular expression [abc][0-9]* is used. (Case insensitive)
  • Note that to deal with the ambiguities I have made the conjunction rule right associative and let conjunctions have the lowest priority should more rules be applicable. I.e. Cp & q is parsed as ((Cp) & q). To get C(p & q) use C(p & q).

    Note that the extended parser converts implication p => q into !(p & !q) and disjunction p v q into !(!p & !q). It then uses the normal parser for parsing the result.
    Note that & binds more tightly than v and that v bind more tightly than =>, e.g. p v p & p => p is the same as (p v (p & p)) => p.

    You can download mael.jar which you can run like any other executable .jar file. Here is a command-line example using some JVM arguments:

    java -Xmx786m -Xms512m -Xss18m -jar mael.jar

    Version 1.1: Fixed a bug where only a subset of all fully expanded sets would be generated

    Version 1.0:
    - Polished the code and made the .jar file executable
    - Fixed a bug with the fully expanded sets not being calculated properly in the single agent case.
    Version 0.93: Made the OutOfMemory error more clear.
    Version 0.91: Fixed a couple of bugs and changed how the binary operators bind for the extended parser.
    Version 0.9: The applet part is essentially finished. Some internal refactoring and api restructuring is needed before version 1.0
    Update 2010-06-24: Added model extraction.
    Update 2010-06-17: Changed the Hintikka structure to show partitions rather than binary relations and polished the gui.
    Update 2010-06-15: Added the option to extract a Hintikka structure.
    Update 2010-06-03: Updated the tableau to the latest version and added options
    Update 2010-05-27: Experimentally added the implication and disjunction binary operators
    Update 2010-04-13: Fixed an issue where the second elimination (E2) rule did not eliminate states properly.

    Last modified: 2010-08-02
    Contact thesis[at]thomaslyngby.dk