Hilbert II 
Formal Correct Mathematical Knowledge 

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 starts with logic and set theory.
This release contains a specification of XML files that can have mathematical content. It can also produce LaTeX files out of QEDEQ XML files, samples and a script with the beginning of axiomatic set theory are included. See Elements of Mathematical Logic for the logical background of this project (parts in German). In Logical Language more formal details are explained.
You could read the change history to know the difference to the previous release.
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.Xml2Other
The classpath must include the files in the lib directory.
You can also simply start the textual or GUI version by starting the batch scripts in directory bin.
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 .
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 socalled 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).
Directory  Description 

bin 
executable files 
xml2othergui.bat 
batch file to start the application with GUI 
xml2othergui.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 
config 
configuration files 
log4j.properties 
log4j property file, change "FATAL" to "DEBUG" to get a log file 
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 
math 
mathematical texts 
qedeq_set_theory_v1_en.pdf 
beginning of axiomatic set theory, this is already a QEDEQ module 
qedeq_sample1_en.pdf 
mathematical sample: small 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 (parts in German) 
javadoc 
java documentation of Hilbert II 
lib 
libraries 
commonslogging1.1.jar 
apache commons logging component 
log4j1.2.14.jar 
log4j logging implementation 
qedeq_se.jar 
binary release of Hilbert II 
xercesImpl.jar 
apache XML parser xerces 
xmlapis.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 
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 
qedeq 

index.html 
another documentation of QEDEQ XSD 
Beside the steps mentioned in Overview you should install a correction for the buggy LaTeX package longtable. One possiblity is this patch from Chungchieh 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.
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.
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 axomatic 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. 
0.05 toffle 
Simple formal proofs can be written down. 