www.qedeq.org

 Hilbert II

English   Deutsch
Hilbert II at SourceForge
introduction
news
mathematics
QEDEQ
planning
download
glossary
development
prototype
links
contact
site map
Development

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.

0.01
 brigand
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.
0.02
 moster
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.
0.03
 mongaga
Formal checks for single formulas could be done ("is this formula well formed").
0.04
 gaffsie
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.
0.05
 toffle
Simple formal proofs can be written down in QEDEQ syntax.
0.06
 misabel
Simple formal proofs can be checked.
0.07
 joxter
All needed formal proof methods for Axiomatic Set Theory can be written down in QEDEQ syntax.
0.08
 hodgkins
All proof methods that can be expressed within the QEDEQ syntax can be checked.

update 2016-03-28 01:29:51+0200