InstructionsThis possible world calculator evaluates a modal formula with respect to a Kripke model that can be constructed by the user himself. The machine requires a netscape 4.x or internet explorer 4.x browser.
Creating a modelThe model will be depicted in the yellow field, while the buttons on the right hand side can be used to perform the construction.
Making worldsClick WORLDS and select by clicking numbers 1 ... 4. The worlds appear in the yellow field. A world can be removed by clicking -WORLD and then the number of the world which you want to remove.
Filling in propositionsYou can now fill in worlds by assigning truth-values to propositional variables p and q. If nothing is changed then the machine takes the propositional variables to be false. If you want to change the values, then click PROP_VARS, and then pick the world of your choice 1 ... 4, and continue by choosing either p or q. The value of that propositional variable is then changed with respect to the selected world. This is depicted in the model by the color of the propositional variable which is turned from red into green, which represents that this proposition is true at the selected world.
Making worlds accessibleAn accessibility between worlds can be created by clicking first ACCS, and then click the number of the world that you want to have access from and click another number to specify which world you want to be accessible.
Random automatic constructionYou can also let the machine pick a model for you by clicking RANDOM MODEL. You can also let the machine choose the value of the propositional variables freely, by clicking first PROP_VARS and then RANDOM. The same is possible for construction of the accessibility relation, first click ACCS, and then RANDOM.
Clearing parts of the modelYou can remove a model by choosing CLEAR MODEL. You can also remove the propositional information or the accessibilities by first clicking PROP_VARS or ACCS and then CLEAR.
Entering a formulaIf a model has been constructed, you can make a formula with the buttons ( ... dmd. They represent the obvious symbols. After clicking, the symbol appears on the screen. If you are ready, you can ask the machine to start the computation by pushing ent. The machine starts the computation, and shows the result in the model. Worlds which reject the formula turn red, while the worlds which support the formula turn green. If you want to remove a formula, click cl.
Entering a formula without using the mouse After a while, entering a formula by clicking gets somewhat tiring. You can use the text input window below the machine for a faster formula input. Use the following symbols: parentheses, p, q, and -,&,v,>,= for negation, conjunction, disjunction, implication and equivalence, respectively, and B and D for the necessity and possibility operator, respectively. Push PUT, the formula appears in standard notation on the screen. Then click ent, and the evaluation takes place.