Overview | Package | Class | Use | Tree | Deprecated | Index | Help
| Hilbert II - JAVA-Packages - Principia Mathematica II
PREV NEXT | FRAMES NO FRAMES

# PMII - Principia Mathematica II

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

See:
Description

Packages
com.meyling.principia |
com.meyling.principia.argument |
com.meyling.principia.html |
com.meyling.principia.io |
com.meyling.principia.latex |
com.meyling.principia.logic.basic |
com.meyling.principia.logic.paragraph |
com.meyling.principia.logic.rule |
com.meyling.principia.module |

This open source project wants to present mathematical knowledge in a formal correct form. It includes a proof verifier which checks a mathematical proof written in a certain formal language and a HTML converter which produces HTML pages that display mathematical knowledge. These mathematical knowledge is organized in "MODULE"s which could be spread over the whole world wide web.

This program suite is only a working prototype for the main project Hilbert II. It concentrates on the basic logic foundation of mathematics. The software design of the main implementation will be highly different. The following information is only appropriate for this prototype.

Look at http://www.qedeq.org/ or http://sourceforge.net/projects/pmii/ to get the latest source code and information.

If you start the test program "com.meyling.principia.Main" it will try to copy some of the modules from the internet homepage into a new local directory "com/meyling/principia/buffer", then it tries to load and check them.

There are some modules with errors to demonstrate a verify failure. It also tries to "compress" some module files, to "reduce the rule version" and to construct HTML files for some of the modules at the same buffer location.

You could also call the programm "com.meyling.principia.CheckModule" directly. It will copy the needed modules into the local file buffer and will verify the proofs.

With the programm "com.meyling.principia.MakeHtmlModule" you could generate some html files from the given module addresses.

By calling "com.meyling.principia.MakeCompressedModule" principia modules are striped from unnecessary proof lines.

More important is the class "com.meyling.principa.MakeReducedModule". It generates modules that use only basic rules (e.g. rules with rule version 1.00.00).

If you just want to test the tiny converter from LaTeX into HTML just start "com.meyling.principia.html.Latex2Html" with the file names (without ".tex") as arguments. The resulting files are at the same directory position but have the ending ".html".

All project files are published under the GPL see the file http://www.gnu.org/copyleft/gpl.html for further details.

Overview | Package | Class | Use | Tree | Deprecated | Index | Help
| Hilbert II - JAVA-Packages - Principia Mathematica II
PREV NEXT | FRAMES NO FRAMES

©left GNU General Public Licence All Rights Reserved.