Hilbert II is a free and open source program suite that enables a mathematician to put theorems and proofs into that knowledge base. These proofs are automatically verified by a proof checker.

Also texts in "common mathematical language" can be integrated. The mathematical axioms, definitions and propositions are combined to so called QEDEQ modules. Such a module could be seen as a mathematical textbook which includes formal correct proofs.

Because this system is not centrally administrated and references to any location in the internet are possible, a world wide mathematical knowledge base could be build. Any proof of a theorem in this "mathematical web" could be drilled down to the very elementary rules and axioms.

Think of an incredible number of mathematical textbooks with hyperlinks and each of its proofs could be verified by Hilbert II. For each theorem the dependency of other theorems, definitions and axioms could be easily derived.

Requirements:

· Java

What's New in This Release: [ read full changelog ]

· We have now a parser that can read a propositional calculus proof written in ASCII text format and transform it into a QEDEQ XML NODE element. It was quickly hacked together but enables us to speed up proof integration. It can be accessed via GUI menu entry Tools / Proof Text to QEDEQ.
· A derivation rule has now a version too and name plus version must be unique (which is checked).
· We introduce a "brief" parameter for LaTeX and UTF-8 plugin to produce summary documents.
· And last but not least we included more propositions with formal proofs in qedeq_formal_logic_v1. Now even the tedious proofs for associativity can be found.