Hilbert II 0.03.10 (Default branch) |
|
|
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".
License: GNU General Public License (GPL)
Changes:
All error locations of a QEDEQ module are
highlighted in the source viewer now. A click on
the error list jumps to the error position. Only
one application instance can be started. The Java
version is checked during startup and must be at
least 1.4.2. The loading sequence for referenced
modules changed: now modules are tried according
their enumeration. Application for the WebStart
mode is now the subdirectory ".qedeq" within the
home directory.
|