Hilbert II 0.03.08 (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:
External QEDEQ module references are resolved, so predicate and function constants can be defined outside the current module and simply be used by referencing them. Formal checking is now also applied recursive to all required modules. To resolve external references for the LaTeX generation the module is also checked. However if checking errors occur the generation of LaTeX is continued.
|
440Forums |
MacMusic.org |
PcMusic.org |
440tv |
Zicos |
AudioLexic
