#
Hilberticus Help

###
What is Hilberticus?

Hilberticus is an abacus for sets.

Just enter a formula using the well-know logical and set operators and
press "Evaluate". On the basis of an elementary decision algorithm,
Hilberticus
determines whether the formula was true or not. If the formula is not
true, it can either be
satisfiable or inconsistent.

For a satisfiable formula Hilberticus can generate examples and
counter-examples in the form of Venn diagrams. Just press "Example" or
"Counter Ex" after a formula
was found to be satisfiable.

Hilberticus can also be used to decide simple propositional formulas.
Just type a propositional formula and press "Evaluate". The variables
are interpreted as boolean
variables in this case. You can use the buttons on the right to
transform the propositional formulas different
standard forms, e.g., conjunctive normal form (CNF).