Principia Mathematica II, Version @PMII_VERSION@ ================================================ *pmii* is short hand for the program suite "Principia Mathematica II" Copyright 2000-2004 Michael Meyling . *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