Just start the applet and type in a set-theoretic formula.
Press "Evaluate" and Hilberticus will compute whether the formula you
typed in is true or not.
Use the "Example" and
"Counter-Ex." buttons to generate examples and counter-examples
in the form of Venn diagrams.
Hilberticus uses a newly developed constructive decision
algorithm
for an elementary sublanguage of set (or more precisely class) theory.
For details see the
documentation
or the
publication
of the algorithm.
Re-implementation of the tool by the SLDecider group started in the
year 2001.
Credits go to the members of the SLDecider group:
J. Lücke, J. D. Bouecke, M. Benzke, A. Dimek, A. Mitchkowski
and S. Muras.
Last update of the beta-version on this site: May 2007.