×

Hilberticus – a tool deciding an elementary sublanguage of set theory. (English) Zbl 0988.68591

Goré, Rajeev (ed.) et al., Automated reasoning. 1st international joint conference, IJCAR 2001, Siena, Italy, June 18-22, 2001. Proceedings. Berlin: Springer. Lect. Notes Comput. Sci. 2083, 690-695 (2001).
Summary: We present a tool deciding a fragment of set theory. It is designed to be easily accessible via the internet and intuitively usable by anyone who is working with sets to describe and solve problems. The tool supplies features which are well-suited for teaching purposes as well. It offers a self explaining user interface, a parser reflecting the common operator bindings, parse tree visualization, and the possibility to generate Venn diagrams as examples or counterexamples for a given formula. The implemented decision procedure which is based on the semantics of class theory is particularly suitable for this.
For the entire collection see [Zbl 0968.00052].

MSC:

68T15 Theorem proving (deduction, resolution, etc.) (MSC2010)
03B25 Decidability of theories and sets of sentences
03E99 Set theory

Software:

Hilberticus
PDFBibTeX XMLCite
Full Text: Link