|
INSTRUCTIONS Formulas can be put in as updates to eliminate those situations/valuations
which falsify the given formula. They also can be brought in as tests.
If all the situations that
are left over verify such formula the green light starts flashing, which signifies that the
formula is a valid conclusion of the formulas that have been put in as updates before (the premises).
If the red light starts flashing this means that the tested formula is refuted: the negation
of the tested formula is then a valid conclusion. All the situations that are left over after the
updates falsify the input (counter-examples). A falsifying situation is indicated by a red background.
A flashing orange light indicates that neither the formula nor its negation is valid. There
is at least one situation left over that verifies the formula and at least one that falsifies it.
A blue light indicates that the input is not a formula (syntactic error).
|
|
INPUT
Formulas have to be written with the symbol-buttons (with a dark gray background).
For each symbol there is a button (the 'iff'-button represents the equivalence). The 'DEL'-button
is meant for backward deletion of symbols to make adjustments.
After a formula has been typed in the input-buttons can be used (light gray background) to 'execute' updates
and tests. To perform new updates and tests clear the formula-screen by clicking 'NEW'.
If you want to start all over again (initial state) then click 'CLEAR'.
You can start with the 'party'-example from the lecture notes with
p/q/r = 'Mary/Ann/John comes to the party' (page 30).
|
