|
Hilbert II - JAVA-Packages - Principia Mathematica II | ||||||||||
PREV NEXT | FRAMES NO FRAMES |
See:
Description
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.
|
Hilbert II - JAVA-Packages - Principia Mathematica II | ||||||||||
PREV NEXT | FRAMES NO FRAMES |
©left GNU General Public Licence All Rights Reserved. |