Hilberticus is an online abacus for sets

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.
Your browser does not support the |applet| tag.

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.

For further information, please contact info@hilberticus.org.