Projects / Hilbert II

Hilbert II

The goal of Hilbert II, which is in the tradition of Hilbert's program, is the creation of a system that enables a working mathematician to put theorems and proofs (in the formal language of predicate calculus) into it. These proofs are automatically verified by a proof checker. Because this system is not centrally administered and enables references to any location on the Internet, a world wide mathematical knowledge base could be built. It also contains information in "common mathematical language".

Operating Systems

Recent releases

  •  24 May 2013 18:11

    Release Notes: This release concentrates on stabilizing the processing structure, increasing the test coverage, and bugfixes. It reworks "Process / View Processes": now all modules it tries to work on within a process are listed. "Details" shows more useful information. There is an XSD change: the element BIBLIOGRAPHY is allowed to have no ITEM sub elements.

    •  10 Apr 2013 22:00

      Release Notes: The icon for QEDEQ module status display now has different colors to represent different stages. Errors and warnings are visualized by decorator icons. Modules which are in progress are represented by animated icons. The clover and findbugs tools were updated. Process synchronization and process control were reorganized. This work is not finished yet, but nearly all module status changes are now caused by plugins. The process view shows more detail, and the chances for user interrupts were increased.

      •  10 Feb 2013 21:21

        Release Notes: The context menu of text area fields include now "find": one can search for strings. The initial window size for text viewing was optimized; now the window should fit the screen more likely. Various test classes and tests were added. The test coverage percentage is now at 78.6%. A positive side effect was the discovery of some minor bugs, which were directly fixed. A few formal proofs were added to qedeq_formal_logic_v1.xml.

        •  30 Jul 2011 13:14

          Release Notes: There is now a parser that can read a propositional calculus proof written in ASCII text format and transform it into a QEDEQ XML NODE element. This helps speed up proof integration. It can be accessed via GUI menu entry "Tools / Proof Text to QEDEQ". A derivation rule now also has a version, and the combination of name and version must be unique. A "brief" parameter was introduced for the LaTeX and UTF-8 plugin to produce summary documents. More propositions with formal proofs are included.

          •  13 Jun 2011 23:08

            Release Notes: This release introduced a new proof method: conditional proof. Based on the deduction theorem, you can make an assumption and draw conclusions from it. It shows the unfolding of formal logic from axioms and inference rules to propositions of propositional calculus with formal proofs within qedeq_formal_logic_v1. The new proof method is also integrated in the proof checker. In the log output pane, messages are now better structured and more readable.


            Project Spotlight


            A Fluent OpenStack client API for Java.


            Project Spotlight

            TurnKey TWiki Appliance

            A TWiki appliance that is easy to use and lightweight.