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).