The goal of Hilbert II, which is in the traditionof Hilbert's program, is the creation of a systemthat enables a working mathematician to puttheorems and proofs (in the formal language ofpredicate calculus) into it. These proofs areautomatically verified by a proof checker. Becausethis system is not centrally administered andenables references to any location on theInternet, a world wide mathematical knowledge basecould be built. It also contains information in"common mathematical language".
License: GNU General Public License (GPL)
Changes:
Some small but important improvements were made.The error presentation gives the correct URL andthe GUI marks the position of the first error inthe source code of a QEDEQ module. During checkingfor logical correctness, all required QEDEQmodules (as specified in the "IMPORTS" section)are loaded. Beside various refactorings, themodule "qedeq_basic_logic_v1.xml" is a little bitmore formal (that is: has more formal formulas init).
More...
12-24-2007
