Hilbert II

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. The prototype presents the logic foundation of this project. It works with (prototype) QEDEQ module files located anywhere in the internet. The protocols http and ftp are used, also local files can be specified. After the input of an URL of a QEDEQ module the local file buffer is searched. If the requested QEDEQ file was not found, a download of the file specified by the URL is started and the result is saved in the local file buffer. Afterwards the QEDEQ module is loaded and checked for formal correctness. If other QEDEQ modules are referenced these are also loaded. Not until all necessary QEDEQ modules were successfully loaded and checked the originally specified QEDEQ module gets it's "green correctness point". In case of an error a detailed problem description is given and the problematic position in the corresponding module is shown.

Other documents can be generated out of successfully loaded and checked QEDEQ modules. The prototype can produce HTML and LaTeX files. The prototype also can automatically eliminate all used meta rules and change the proofs that only basis rules occur. For this each application of a meta rule is replaced by a sequence of basic rules. The newly generated QEDEQ module is saved separately. Also duplicate proof lines can be eliminated.

Since version 0.00.53 the prototype has a GUI. It is even possible to start it from the page Java Web Start if your browser supports this. Furthermore the executable prototype and it's source code can be downloaded.

With the prototype you could create and edit your own QEDEQ modules. However each simple text editor can be used. The file format is described in section QEDEQ. In the web already existing QEDEQ modules could be used just by referencing them.

The main project will not need the extreme detail deepness of the mathematical proofs in the prototype, but this detailed form should still be generable with the main program suite.