Epistemic Logic Suite

Syntax

• When entering a formula:
  • use ~A for $\lnot{}A$
  • use (A & B) for $(A\land{}B)$
  • use (A | B) for $(A\lor{}B)$
  • use (A -> B) for $(A\rightarrow{}B)$
  • use K{a,b,c}A for $K_{a,b,c}A$
  • use D{a,b,c}A for $D_{a,b,c}A$
  • use C{a,b,c}A for $C_{a,b,c}A$
  • use [A]B for $[A]B$

Editing Instructions

• Click in the open space to add a world
• Drag between worlds to add a transition for the current agent
• Ctrl-drag a world to move graph layout
• Click a world or a transition to select it
• When a world is selected:
  • R toggles reflexivity for the current agent
  • Delete removes the world
• When a transition is selected:
  • L (eft), R (ight), B (oth) change direction
  • Delete removes the transition
• Copy the URL from your browser's URL bar to share your model!

About this project

Epistemic Model Suite is being developed by Carlos Aguilera Ventura. The model-checking part, as well as the main interface, is a fork of the open source project Dynamic Epistemic Logic by Elliot Evans (which is instead based on Modal Logic Playground, by Ross Kirsling).