Instructions
Make a model, specify a formula and let the machine do the
evaluation!
Creating Models
A model can be made by clicking the buttons on the upper righthand
part of the 'dashboard'. The management of possible worlds is
divided into four different
columns (four worlds is the maximum). Click +x in column number x
and world x appears on the screen (model), click
-x in column x and world x disappears
again.
Every world contains the evaluation of two propostional variables p and
q. The machine takes those propositions to be false, but they can be
made true by the user by clicking p and/or q,
respectively. This is made visible on the screen by changing colors of
the variables:
green = true,
red = false.
A world y can be made accessible from a world x by clicking
>y in column x.
Tired of creating worlds? Let the machine do it for you.
A model can be generated by clicking random model. Unhappy with
the chosen model? Click clear model, and repeat.
Partial random generation is also possible. If you have a set of worlds in
your model, then you can let the machine decide on the truth-value
assignments by clicking the upper random button. The second
randombutton (yellow background)
picks an arbitrary accessibility configuration. Clearing the accessibility
is also possible.
Writing formulas
Specifying a formula can be done by the buttons in the lowest part. The
formula appears step by step on the lower longer screen. A faster way of
writing a formula is to specify in the text window by using your keyboard:
B = box, D = diamond, &
= conjunction,
v = disjunction, - = negation, > = implication,
= = equivalence. Put the formula on the display by clicking
PUT.
Evaluation of the formula can then be accomplished by clicking ENT.
A small flashing light at every world's horizont appears. The color
indicates the truth-value at the given world:
green = true,
red = false.
Modifying formulas and models
A formula can be replaced by clicking CLR and filling in a new formula.
Backward deletion step by step is possible by clicking DEL.
A model can be modified by adding worlds, choosing new truth-value assignments
for p and q or a new accessibility relation. Remember that
after modifications, a new evaluation takes another click on ENT.
