
Hilbert II  Version 0.03.04  
PREV NEXT  FRAMES NO FRAMES 
See:
Description
Packages  
org.qedeq.kernel.base.list  Descriptions of element list functionalites. 
org.qedeq.kernel.base.module  The main functionalities of qedeq modules are described here. 
org.qedeq.kernel.bo.control  Contains business object controllers. 
org.qedeq.kernel.bo.load  Load QEDEQ module files from local system or from the internet. 
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.common  Common classes. 
org.qedeq.kernel.config  Herein is the configuration for the kernel. 
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, 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.trace  Trace abilities, for debugging purpose only. 
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.04 release was build at 20070510 04:03:33 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.04  
PREV NEXT  FRAMES NO FRAMES 
©left GNU General Public Licence All Rights Reserved. 