Hilberticus - A Tool Deciding an Elementary Sublanguage of Set Theory

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.

• Type: Conference
• Year: 2001
• Where: CADE
• Authors: Jörg Lücke
• Keywords: Automated Reasoning, CADE 2001, Common Operator Bindings, Implemented Decision Procedure, Self Explaining User