Hilbert II

Formal Correct Mathematical Knowledge

Version   0.03.09  
Timestamp   2008-03-31 01:02:27  
Code name   mongaga  

Table of Contents

Overview quick start and feature summary
Project Goals about this project
Release Contents detailed directory description of this release
Further Installation some more or less optional adjustments
Licenses these licenses apply
Future Development short range project plan


This is an unstable development release of Hilbert II. In the tradition of Hilbert's program the project creates a formal correct (checkable by a proof verifier) but readable (like an ordinary LaTeX textbook) mathematical knowledge base which is freely accessible within the internet. The project started with logic and set theory.

This release contains a program suite that can produce LaTeX files out of QEDEQ XML files. The QEDEQ files can be checked for syntactic correctness. In Logical Language more formal details are explained. Samples and a script with the beginning of axiomatic set theory are included. All formulas are written in the formal language. All the axioms, definitions and propositions written in a formal language in it. Still no formal proofs are given. See Elements of Mathematical Logic for the logical background of this project.

You could read the change history to know the difference to the previous release.

A convenient way to start this application is via Java Web Start. Just click on: START. There should be a splash screen for Java Web Start, asking you to trust the signature. Although it will be not recommended you must trust the signature of Hilbert II to start the application. If you already started an older program version via Web Start you should remove the files in the config directory.

Precondition is a Java Runtime Environment, at least version 1.4. From Download Java 2 Platform you could get the Java Runtime Environment J2SE v 1.4.2 JRE.

To start the application call:


The classpath must include the files in the lib directory. A convenient to start the application is the script qedeq_se in the main directory.

Sample XML files can be found in the sample directory. The main structure of an QEDEQ XML file looks like the LaTeX book format. There is a special kind of subsections called node that contain an abbreviation, axiom, definition or proposition. Each node is labeled and could be referenced by that label. Here is the XSD and here it's documentation. The root element is called QEDEQ.

This release includes the source code and the JUnit test classes. The code coverage results of these tests where produced by Clover.

Project Goals

The goal of Hilbert II is decentralised access to verified and readable mathematical knowledge. The knowledge base contains mathematical texts in different languages and detail levels, axioms, definitions, propositions and their proofs. Beside common non formal proofs the system includes formal proofs that were verified by a proof checker.

The mathematical axioms, definitions and propositions are combined to so-called QEDEQ modules. Such a module could be seen as a mathematical textbook. At least all proposition formulas are written in a formal language and each proposition can also have a formal correct proof. The proposition is verified iff it has a formal proof and all required propositions are also verified.

Hilbert II will provide a program suite that enables a mathematician to put data into that knowledge base and retrieve various documents and analyze results out of the system. This includes the generation of LaTeX files that look like a common mathematical textbook and the answer to questions like "assumes this theorem the axiom of choice?" for verified propositions. As it's name already suggests, this project is in the tradition of Hilbert's program.

Because this system is not centrally administrated and references to any location in the internet are possible, a world wide mathematical knowledge base could be build. Any proof of a theorem in this "mathematical web" could be drilled down to the very elementary rules and axioms. Think of an incredible number of mathematical textbooks with hyperlinks and each of its proofs could be verified by Hilbert II. For each theorem the dependency of other theorems, definitions and axioms could be easily derived.

See also under QEDEQ basic concept for more project details. This document was generated out of the following XML file: qedeq_basic_concept.xml.

This release contains also the beginning of a script about axiomatic set theory. This script is also available in German and has this XML source.

The XML files have a formal structure that is defined here or here. The logical language is described in qedeq_logic_language_en.pdf (in development). The mathematical logical propositions are noted in qedeq_logic_v1.pdf.

Release Contents

This release has the following directory structure.
Directory Description
bin executable files, currently empty
config configuration files
  log4j.xml log4j property file, change "fatal" to "debug" to get a log file
  mengenlehreMathOperators.xml LaTeX operator information, used from the parser to transform LaTeX formulas into QEDEQ XML
doc documentation
  project project specific
    qedeq_basic_concept_en.pdf basic concept of Hilbert II
    qedeq_logic_language_en.pdf explanation of the logical language of Hilbert II (in development)
    projektbeschreibung.pdf project description (in German, a little bit outdated)
    changes.txt change history to previous versions
    clover code coverage results of JUnit tests by Code Coverage by Clover
  math mathematical texts
    qedeq_set_theory_v1_en.pdf beginning of axiomatic set theory, this is already a QEDEQ module
    axiomatic_set_theory.txt beginning of set theory as non formal (ascii text) file, it shows the intention of this project (parts in German)
    qedeq_logic_v1_en.pdf logical background
javadoc java documentation of Hilbert II
  gui gui
  kernel kernel
lib libraries
  commons-logging-1.1.jar apache commons logging component
  forms-1.1.0.jar JGoodies Forms GUI support
  log4j-1.2.14.jar log4j logging implementation
  looks-2.1.4.jar JGoodies Looks GUI support
  qedeq_gui_se.jar binary GUI release of Hilbert II
  qedeq_kernel_se.jar binary kernel release of Hilbert II
  xercesImpl.jar apache XML parser xerces
  xml-apis.jar XML standard API definition
license license files
  license/apache_license.txt apache software license
  license/fdl.html GNU Free Documentation License
  license/gpl.html GNU General Public License
  license/forms_license.txt BSD license for JGoodies Forms
  license/looks_license.txt BSD license for JGoodies Looks
  license/tango_license.txt Creative Commons Attribution Share-Alike license for the tango theme
log log files are written herein
sample sample XML files
  qedeq_basic_concept.xml qedeq basic concept as qedeq XML document
  qedeq_set_theory_v1.xml beginning of axiomatic set theory
  qedeq_sample1.xml mathematical sample module
  qedeq_error_sample_00.xml usage of an unkown logical operator
  qedeq_error_sample_01.xml too many arguments for logical implication operator
  qedeq_error_sample_02.xml second quantification over same variable
  qedeq_error_sample_03.xml subject variable occurs free and bound
  qedeq_error_sample_04.xml subject variable occurs bound and free
  qedeq_sample2_error.xml semantic error in QEDEQ file, a node id is used twice
  qedeq_sample3_error.xml syntax error in XML file, violates XML syntax
  qedeq_sample4_error.xml syntax error in XML file, violates XSD
  qedeq_sample5_error.xml logic error in XML file, quantify over already bound subject variable
  qedeq_sample6_error.xml logic error in XML file, "unknown" is an unknown predicate
  qedeq_sample7_error.xml logic error in XML file, a subject variable occurrs free and bound
  qedeq_sample8_error.xml semantic error in XML file, duplicate language entries
src source code of Hilbert II
srcTest source code of JUnit tests
xml XML schemata and their documentation
  qedeq.xsd XSD for QEDEQ format
  qedeq.html documentation of QEDEQ XSD
  parser.xsd XSD for operator definition for text parser
  parser.html documentation of parser XSD
    index.html another documentation of QEDEQ XSD

Further Installation

Beside the steps mentioned in Overview you should install a correction for the buggy LaTeX package longtable. One possiblity is this patch from Chung-chieh Shan. It was used to produce the provided PDF files.


The QEDEQ XML files stand under the GNU Free Documentation License (GFDL), the software of this project under the GNU General Public License (GPL).

For XML parsing the apache parser is used which falls under the apache license. This license applies also to the class com.sun.syndication.io.XmlReader which was taken on 2008-03-06 from project Rome (see https://rome.dev.java.net/../XmlReader.java). The GUI uses the tango theme that is under the Creative Commons Attribution Share-Alike license.

Hilbert II uses JGoodies Looks and JGoodies Forms, distributed by JGoodies under the terms of the BSD License see looks license and forms license for details. Also included are three additional classes (SimpleInternalFrame, Factory and UIFSplitPane) by Karsten Lentzsch, which are distributed under these terms.

Future Development

For the current source code you could browse the subversion or cvs tree.

Here are descriptions of the next minor releases. Subversions 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 axomatic 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.