Hilbert II

Table of Contents

Overview

This is an unstable development release of Hilbert II.

Contains specification of XML files that have mathematical content. This release can produce LaTeX files out of qedeq XML files, samples are included.

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:

  org.qedeq.rel.test.text.Xml2Latex <xmlFile>

or for an interactive swing window:

  org.qedeq.rel.test.gui.Xml2Latex

The classpath must include the files in the lib 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 .

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.

Release Contents

Directory	Description
bin	executable files
xml2latexgui.bat	batch file to start the application with GUI
xml2latexgui.sh	unix script to start the application with GUI
xml2latex.bat	batch file to start the application in text mode
xml2latex.sh	unix script to start the application in text mode
doc	documentation
qedeq_basic_concept_en.pdf	basic concept of Hilbert II
clover	code coverage results of JUnit tests by
xml
qedeq.xsd	XSD for qedeq format
qedeq.html	documentation of qedeq XSD
javadoc	java documentation of Hilbert II
lib	libraries
qedeq_se.jar	binary 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
sample	sample XML files
qedeq_basic_concept.xml	qedeq basic concept as qedeq XML document
qedeq_sample1.xml	mathematical sample module
src	source code of Hilbert II
srcTest	source code of JUnit tests

Licenses

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.

Future Development

For the current source code you can browse the cvs tree at sourceforge.

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.