The open source parts of ProofPower and all the documentation may be obtained from this site. The documentation covers the following packages:
The ProofPower packages are copyright © Lemma 1 Ltd. All the ProofPower packages except PPDaz are free, open-source, software made available under the terms of the GNU General Public License.
The PDF documentation for PPDaz is freely available to anyone who is interested and the PPDaz software is available under a free licence for non-profit use.
The stable version of the open source distribution is working version 2.9.1w8. It is available here. Before downloading the distribution, you may like to read the description of the changes in this release and the read-me file. This version works with Poly/ML 5.3 and later and should be compatible with most C/C++ developer kits (including those that default to 32-bit architecture and those like Apple's Xcode tools that default to 64-bit architecture). Some earlier versions are available here. Working snapshots of the latest version under development are filed here from time to time.
OpenProofPower has been built and tested by Lemma 1 using: Poly/ML version 5.3 and 5.4; Standard ML of New Jersey (SML/NJ) version 110.54; x86 PC hardware, and Apple PowerPC and Intel hardware; Linux; OpenSolaris; Mac OS X with Apple's X11 distribution; Cygwin. For building and running ProofPower, Poly/ML is typically two to four times faster than SML/NJ and is the recommended compiler.
If you use SML/NJ, you must use version 110.54 or later. If you use Poly/ML, then you must use version 5.3 or later.
PPXpp requires OpenMotif 2.3 or later. As OpenMotif is not available on Cygwin, PPXpp is not currently supported on Cygwin.
If you are using Mac OS X, then there are some keyboard configuration files that you can download to make working with PPXpp (and other Motif applications) easier.
Patches to fix problems or make minor upgrades for ProofPower are posted from time to time on this web-site. The available patches and information about how to use them are here.
If you are signing on behalf of academic or commercial institution, please enclose a covering letter on your institution's headed notepaper. We will return the signed licence and instructions for downloading the software.
Dr. R.D. Arthan,
Lemma 1 Ltd.
2nd Floor, 31A Chain Street
If you have any problems with ProofPower, please feel free to discuss them on the ProofPower mailing list.
If you're interested in a support contract, then please contact, Rob Arthan, by e-mail , or by post at the address given above, or by phone on +44 118 958 4409.