|
Hilbert II - Version 0.03.01 | ||||||||||
PREV NEXT | FRAMES NO FRAMES |
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 | ||||||||||
PREV NEXT | FRAMES NO FRAMES |
©left GNU General Public Licence All Rights Reserved. |