Hilbert II 0.03.09 (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:
Now QEDEQ modules may be removed within the GUI, and all dependent modules will change their state accordingly. Within the LaTeX parts, the new command "qref" is supported. It references to a Node from the local or an imported QEDEQ module. UTF-8 and ISO-8859-1 are now correctly parsed, and error lines are translated accordingly. The mathematical XML files have fewer errors and contain more (still informal, but very close to formal) proofs. Under the hood, a lot of refactoring took place.
|
