Hilbert II - Version 0.03.01

Hilbert II

This open source project wants to present mathematical knowledge in a formal correct form.

See:
          Description

Packages
org.qedeq.kernel.base.common Common classes.
org.qedeq.kernel.base.list Descriptions of element list functionalites.
org.qedeq.kernel.base.module The main funtionalities of qedeq modules are described here.
org.qedeq.kernel.bo.control Contains business object controllers.
org.qedeq.kernel.bo.logic Contains the logical abilities of the kernel.
org.qedeq.kernel.bo.module Business objects for qedeq modules.
org.qedeq.kernel.bo.visitor The visitor design pattern allows you to decouple the classes for the data structure and the algorithms used upon them.
org.qedeq.kernel.context Provides access to the kernel.
org.qedeq.kernel.dto.list An element is either a list or an atom.
org.qedeq.kernel.dto.module Value objects for qedeq modules.
org.qedeq.kernel.latex LaTeX export abilities of the kernel.
org.qedeq.kernel.log Logging, trace and journal abilities.
org.qedeq.kernel.parser Parse texts with formulas and terms into parse tree and produce QEDEQ output.
org.qedeq.kernel.rel.test.gui GUI interface to test the kernel.
org.qedeq.kernel.rel.test.text Test access for the kernel.
org.qedeq.kernel.utility Common utilities.
org.qedeq.kernel.xml.handler.list Handler to parse formulas and terms.
org.qedeq.kernel.xml.handler.module Handler to parse qedeq XML modules.
org.qedeq.kernel.xml.handler.parser Functionality to parse XML operator lists.
org.qedeq.kernel.xml.mapper Contains mapper for XML objects.
org.qedeq.kernel.xml.parser Connection to SAX XML parsers.
org.qedeq.kernel.xml.tracker Tracks simple XPath descriptions in XML files.

 

This open source project wants to present mathematical knowledge in a formal correct form. This is only an unstable development release of Hilbert II. It can produce LaTeX files out of qedeq XML files.

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.

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 0.03.01 release was build at 2007-01-15 01:44:43 and is part of the development line with the code name mongaga. Look at the project homepage and the sourceforge project page to get the latest source code and information.


Hilbert II - Version 0.03.01

©left GNU General Public Licence
All Rights Reserved.