Hilbert II
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".
| Tags | Text Processing Markup TeX/LaTeX education Documentation Scientific/Engineering Mathematics Internet HTML/XHTML |
|---|---|
| Licenses | GPL |
| Operating Systems | OS Independent |
| Implementation | Java |
Recent releases
- 08 Aug 2008 21:45
Changes: After a huge amount of refactoring, the application is reorganized and the build process is new. Ant is still used, but Maven POMs are also provided. The Eclipse project directories are also included in the magnified src directory, as well as various reports. The Apache Commons library is used (e.g. for thread safe date formatting). The reorganized build process and new package subdivision have lead to a new project structure.
- 17 May 2008 21:08
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.
- 31 Mar 2008 13:08
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.
- 29 Jan 2008 00:46
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.
- 24 Dec 2007 03:08
Changes: Some small but important improvements were made. The error presentation gives the correct URL and the GUI marks the position of the first error in the source code of a QEDEQ module. During checking for logical correctness, all required QEDEQ modules (as specified in the "IMPORTS" section) are loaded. Beside various refactorings, the module "qedeq_basic_logic_v1.xml" is a little bit more formal (that is: has more formal formulas in it).
