Hilbert II

English   Deutsch
Hilbert II bei SourceForge
Entwicklung (English)

This page is for people interested in developing Hilbert II.

The mathematical knowledge of this project is organized in XML files that are called QEDEQ modules. Such a QEDEQ module could have references to other QEDEQ modules which are somewhere in the world wide web. It's main structure looks like an LaTeX book file. There exists a special kind of subsections called node that contain an axiom, definition, rule or proposition. Each node is labeled and could be referenced by that label. Here is the current specification and it's documentation.

Our main focus now is work on the script Axiomatic Set Theory. This was generated out of qedeq_set_theory_v1.xml. This script grows and changes as does the relevant software functions.

Currently we expand our formal logic basis documented in Formal Predicate Calculus. Source for this file is qedeq_formal_logic_v1.xml. In this document every proposition has a formal proof.

The QEDEQ modules stand under the GNU Free Documentation License (GFDL), the software of this project under the GNU General Public License (GPL). The reference implementation is programmed in Java. Current development environment is eclipse.

The following tools and libraries are used in the development process.

Eclipse Java IDE
Ant apache build tool
Xerces apache XML parser
Checkstyle coding standard checker
JUnit a simple framework to write repeatable tests
Clover Clover code coverage analysis tool, see this report

You can download the latest release 0.04.07 with unix file format or with windows file format.

You can browse the contents of this release here: release 0.04.07.

For the current source code you could browse or clone the git repository on github.

Here are descriptions of the next minor releases. Preliminary versions are not listed. All these releases are characterised as "unstable" and are only of interest for developers.

First XSD releases. XML could be parsed and value objects are created. Very simple generation of LaTeX files is possible. There are two QEDEQ modules: the project handbook and a mathematical example. Beside the XSD verification no checking is done. The LaTeX generation works directly on the value objects.
Some elements of the BO (business object) layer exist. The script of axiomatic set theory includes at least most of the axioms. First attempts of a small LaTeX to QEDEQ XML converter.
Formal checks for single formulas could be done ("is this formula well formed").
QEDEQ modules and the referenced modules are loaded from the web. The formula checking incorporates also all required QEDEQ modules and handles external definitions. External predicate and function constants are resolved.
Simple formal proofs can be written down in QEDEQ syntax.
Simple formal proofs can be checked.
All needed formal proof methods for Axiomatic Set Theory can be written down in QEDEQ syntax.
All proof methods that can be expressed within the QEDEQ syntax can be checked.

update 1970-01-01 01:00:00+0100