Hilbert II 0.04.06
The Goal of Hilbert II is the creation of a system that enables a working mathematician to put theorems into it.
Hilbert II wants to become a free, world wide mathematical knowledge base that contains mathematical theorems and proofs in a formal correct form. All belonging documents are published under the GNU Free Documentation License.
We aim to adapt the common mathematical argumentation to a formal syntax. That means, whenever in mathematics a certain kind of argumentation is often used we will look forward to integrate it into the formal language of Hilbert II. This formal language is called the qedeq format.
Hilbert II provides a 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.
The basic concept of this project is published as PDF document: basic concept. This document is already generated out of the following XML file: qedeq_basic_concept.xml. The main project is in the first develompment phase, see under development.
There exists a working prototype called Principia Mathematica II. It is fully capable of first order predicate logic and shows the main features and functionality of Hilbert II. It can verify (prototype) qedeq module files located anywhere in the internet.
The prototype has a GUI and can transfer qedeq modules into HTML and LaTeX files. You can create and edit your own new qedeq module and publish it in the internet. In the web already existing qedeq modules could be used just by referencing them.
What's New in This Release:
· After a huge amount of refactoring, the application is reorganized and the build process is new.
· Ant is still used, but Maven POMs are also provided.
· The Eclipse project directories are also included in the magnified src directory, as well as various reports.
· The Apache Commons library is used (e.g. for thread safe date formatting).
· The reorganized build process and new package subdivision have lead to a new project structure.
In a hurry? Add it to your Download Basket!
What's New in This Release:
- Most visual change is the icon usage for QEDEQ module status display.
- We use gray for not yet worked on modules, purple for loaded modules, cyan for loaded all required modules, red orange for all well formed modules and yellow for all fully proved modules.
- Errors and warnings are visualized by decorator icons.
- Modules which are in progress are represented by animated icons.