This is a Model Checker for Propositonal Modal logic(PML), you can easily design models and evaulate modal propositions under different interpretation.
Color of circles represents propositions value in different worlds:
True
False
Note: use parentheses around each subformula with binary operator to disambiguate operator priority, for example use $(p \land (r \lor \Diamond u))$ instead of $ p \land r \lor \Diamond u$.
use :
"[]" for $\Box$
"
<>" for $\Diamond$
"*" for $\land$
"+" for $\lor$
">" for $\supset$
"-" for $\sim$
To add a new world: click the button, then click somewhere on stage.
To remove a world: click the button, then click on the world you want to remove.
To move a world: click the button, then drag the world you want to move.
To link the worlds: click the button, start drag on a world, then connect the arrow to another world. if you want a reflexive world after selecting just click on the world you want.
To remove a link: click the button, then click on the arrow between the worlds, or a world to itself.
To change valuation: click the button, then click the world you want to changse it's propositional values. A box with a list of propostional letters will appear (which occurred in formula), click the variables to change it's value.(before changing valuation make sure the input text field is not empty)
Enter forumla, then click "evaluation", the color of worlds at which the formula is true will be gray, otherwise remains white.
What are possible worlds?
Possible worlds are at the core of Modal logic, they are perhaps some kind of philosophical or logical posit to evaluate certain category of sentences of ordinary lanugage, Modal sentences. They are sentences about possiblity and necessity.
S. Kripke, The guy behind possible world
semantic
These concepts were not so clear until the early 1960s, Soul Kripke introduced Possibe worlds semantic as a mathematical model to study formal structure of such sentences. A Possible World model $M=\langle W,R,V\rangle$ is an ordered triple consisting of a set of possible worlds $W \neq \emptyset$. A two-place relation $R$ called accessibility is a subset of $W \times W$ and a function $V$ which assigns to each atomic proposition a subset of $W$. It can be thought of as a special directed Graph with labelled nodes plus some more information. In above visualization the circles represent the possible worlds in the set $W$. The links between them indicate the relation $R$. Truth of a complex well-formed formula respect to a possible world $\omega$ can be evaluted recursively by these rules:
$(M,\omega)\models p$ iff $\omega$ is a member of $V(p)$, if $p$ is atomic.
$(M,\omega)\models \sim p$ iff not $(M,\omega)\models p$.
$(M,\omega)\models p \supset q$ iff either not $(M,\omega)\models p$ or $(M,\omega)\models q$.
$(M,\omega)\models \Box p $ iff for every $x \in W$ such that $R \omega x$,$(M,x)\models p$.
The operator $\Box$ stands for necessity. Other connectives such $\land $ and $\lor $ can be defined by $\supset$ and $\sim$, for example $(p \lor q) =_{df}(\sim p \supset q)$ and $(p \land q) =_{df}\sim ( p \supset \sim q)$ and the operator possiblity $\Diamond$ can be defined as $\sim \Box \sim$.
