Principia Mathematica II, Version 0.00.53
================================================
*pmii* is short hand for the program suite "Principia Mathematica II"
Copyright 2000-2004 Michael Meyling <mime@qedeq.org>.

*pmii* is free software; you can redistribute it and/or modify
it under the terms of the GNU General Public License as published by
the Free Software Foundation; either version 2 of the License, or
(at your option) any later version.

This program is distributed in the hope that it will be useful,
but WITHOUT ANY WARRANTY; without even the implied warranty of
MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
GNU General Public License under "doc/gpl.txt" for more details.

This program suite is only a working prototype for the main project
*Hilbert II*. This open source project wants to present mathematical
knowledge in a formal correct form. It includes a proof verifier 
which checks mathematical proofs written in a certain formal 
language called "qedeq format". The mathematical knowledge is 
organized in qedeq module files that could be spread over the whole 
world wide web.

There are HTML and LaTeX converters which produce HTML pages and
LaTeX files for an easier reading.

This prototype *pmii* concentrates on the basic logic foundation of 
mathematics. The software design of the main implementation will be 
highly different. Look at 
 http://www.qedeq.org/
 http://sourceforge.net/projects/pmii/
to get the latest source code and information. People to join in 
are very welcome.


Installation
============
To start the prototype simply call "run.bat" or "run.sh".

If the bin path of the Java Runtime Environment has no entry in the 
executable path or a proxy is used for the internet access the files 
"run.bat" or "run.sh" must be edited. The necessary adaptations are 
described in comments of those files.
Precondition for a working prototype is a Java Runtime Environment, 
at least version 1.4. From
  http://java.sun.com/j2se/1.4.2/download.html
you could get the Java Runtime Environment  J2SE v 1.4.2 JRE.

Further information can be found at
  http://qedeq.org/installation.html


Description
===========
The prototype is fully capable of first order predicate logic and 
shows the main features and functionality of *Hilbert II*. 
It works with (prototype) qedeq module files located anywhere in the
internet. The protocols http and ftp are supported, also local files 
can be specified.
After the input of an URL of a qedeq module the local file buffer is 
searched. If the requested qedeq file was not found, a download of 
the file specified by the URL is started and the result is saved in 
the local file buffer. Afterwards the qedeq module is loaded and 
checked for formal correctness. If other qedeq modules are referenced
these are also loaded. Not until all necessary qedeq modules were 
successfully loaded and checked the originally specified qedeq module
gets it's "green correctness point". In case of an error a detailed 
problem description is given and the problematic position in the 
corresponding module is shown.

Other documents can be generated out of successfully loaded and 
checked qedeq modules. The prototype can produce HTML and LaTeX 
files. The prototype also can automatically eliminate all used meta 
rules and change the proofs that only basis rules occur. For this 
each application of a meta rule is replaced by a sequence of basic 
rules. The newly generated qedeq module is saved separately. 
Also duplicate proof lines can be eliminated.

Since version 0.00.53 the prototype has a GUI. It is even possible to 
start it with Java Web Start from the project homepage if your browser 
supports this.

With the prototype you could create and edit your own qedeq modules. 
However each other simple text editor can be used. The file format is 
described in file "module.txt" and "module.pdf". In the web already 
existing  qedeq modules could be used just by referencing them.

The main project will not need the extreme detail deepness of the 
mathematical proofs in the prototype, but this detailed form should 
still be generable with the main program suite.

Further information can be found at these web pages
  http://qedeq.org/manual.html
  http://qedeq.org/pmii_bugs.html


Author
======
Michael Meyling <mime@qedeq.org>