Kripke Model

Fast start

For quick start just press generate button. An example kripke model graph will be created. And in input box an example sentence will be added. Just go to the input box and press [enter] to check this sentence for each world.
Each sentence start after a colon (:).Before colon there can be : for n , which means that the sentence will be checked for world with number n, or there can be find, which will check sentence for all worlds. For example:

for 1:p and q 
for 2:(p and q)->r
find:(p and q) -> (p or r) and all ex q
for 3: p and 0.3q

p -> q	simply implication between p and q, implemented on fuzzy values p->q = min(1.0f,1.0f-p+q)
p or q	alternative, implemented in following way p or q = max(p,q)
p and q	conjunction, implemented in following way p and q = min(p,q)
!p	negation, !p = 1.0f-p
all p	for all, checks all surrounding worlds for p (p must be true in all world) if fuzzy values are used then value returned is a conjunction of p's in all surrounding worlds
ex p	for all, checks all surrounding worlds for existence of p (p must be true in at least one world),if fuzzy values are used then value returned is an alternative of p's in all surrounding worlds
0.5p 0.5(p and q)	is also acceptable, value on the right will be multiplied by floating value

User manual

To add new node simply press [add node] button and then click on main panel. To change variables of the node press modify button and click on any node to be changed. A textbox will appear, then simply modify : node name (its a first number), variable names or fuzzy values, you can also remove all variables or add new ones.After doing all modificatons press [enter] to accept them.

To remove node press on "Remove node" and click on any node on main panel. To move node press "Move node" button and drag and drop any node.

To add new edge you have to have at least two nodes. Firstly press "Add edge" button then press on first node, from which edge will originate and then press on the second node. To modify fuzzy value of the node press "Modify" button and click on black rectangle, that indicates arrow directions. A textbox will appear , after making changes press [enter]. To remove edge just press "Remove edge", then click on first node and then on the second node of that edge.

Erase button simply erases all the nodes and edges.

Some inner workings

Program is divided into 3 parts. First one is the main class (MLogic) where all user interactions are handled. This class communicates with RoughMain class, which analyzes sentences inputed by user. This class parses sentence with the help of JavaCC that is located in Parser package. Sentence parsed by JavaCC cames back in the form of a tree, which is then recursively analyzed by analyze_recurs() method located in RoughMain class.

All nodes are stored in one vector. Each node stores all edges that have arrows directing to other nodes.

Known issues

After reloding page, applet will not work, you will have to restart your browser (at least IE).

References

plato.stanford.edu/entries/logic-modal great introduction to modal logic.
www.webgain.com/products/java_cc Java Compiler Compiler - a free parser generator for java

Marcin Jędrzejewski, 2002