This help does not explain the language the applet understands.
If you need help with this go to Help with Language. The sole purpose of
this text is to explain the functions the client-side applet offers.
The client-side applet consists of three areas:
- The input area at the top is the area where one enters a proposition.
Move your mouse to this area and click. A blinking cursor will appear.
Try entering some sentence of the formal language. When you have
finished typing your proposition, either hit the Return key
or click Accept. If your input was in error, you can
restore the last content of the input area by clicking
Reject. A small part of the input area provides for
selecting the notation: Peano-Russell (Infix), strict, or Polish. Strict
notation is the same as Peano-Russell notation except that it does not
omit any brackets.
- The big white area in the middle of the applet is the graphical
output area. Here the applet will show the syntax tree of your
proposition, its alpha graph or its Begriffsschrift
graph as well as any evaluation.
- The area at the bottom of the applet consists of many clickable
buttons. By clicking any of them you tell the applet what to do.
At this time, there are the following buttons:
One button, normally labelled classic logic, has a
special meaning: Here you can select the logical system you want
to use. Besides classic logic, the applet supports several
well-known non-classic, multi-valued systems and even an infinite-valued
system. Note that not every button is available in every system. For
example, the button truth table will be inaccessible
if you choose an infinite-valued system.
- Tree: The syntactical structure of the proposition
entered is shown in the large graphical area. This is the default.
- Alpha graph: The proposition is shown as a
Peirce-style alpha graph. This function is only available if
the selected logical system (see further below) supports the
necessary syntactical operations.
- Frege: shows the notation as presented by
G. Frege in his book "Begriffsschrift".
- DNF: shows the disjunctive normal form (DNF)
of the proposition entered
- step towards DNF
- animated DNF: slowly constructs the DNF
displaying every step of its operation.
- CNF: shows the conjunctive normal form (CNF)
of the proposition entered
- step towards CNF
- animated CNF: slowly constructs the CNF
displaying every step of its operation
- eliminate conditionals: constructs an
equivalent proposition that doesn't contain any conditionals
- atomic negations: constructs an equivalent
proposition where only propositional variables are negated
- optimize: performs some cheap syntactical
optimizations. Note that if you are interested in real
optimization, you should have a look at the
Optimization is one of their strengths.
- user-defined: opens a window where the user
may assign truth-values to all propositional variables occuring
in the proposition. After closing the window, the user is shown
the evaluation of the whole proposition and its sub-expressions
- counter-example: the applet shows a counter-example
to the proposition, i.e. an evaluation that falsifies the
- satisfy: the applet shows an evaluation under
which the proposition happens to be true
- first evaluation: shows the first evaluation
- next evaluation: shows the next evaluation
- animated evaluation: slowly shows the
evaluation of the proposition and its sub-expressions under
every possible assignment of truth-values to propositional
variables occurring in the proposition
- reset: resets the evaluation last shown
© Christian Gottschall / firstname.lastname@example.org / 2012-03-31 01:19:53