ProofPower is a specification and proof development and checking tool developed by ICL and now owned by Lemma-1. It is an intellectual descendent of Cambridge HOL, and implements in Standard ML following the LCF paradigm, proof support for exactly the same polymorphic higher order logic as that in Cambridge HOL.

Links to listings of some of the theories which come with ProofPower, with brief descriptions. These are the ones used by the theories at RBJones.com, though at present I am not able to convert them all into HTML.

Freek Wiedijk is tracking progress on automated proofs of a list of "100 greatest theorems". This page lists the statements of the theorems on the list that have been proved in ProofPower.

ProofPower uses an extended character set so that logic and mathematics comes out a bit nicer. This page has some tables showing how these render in HTML.

This document contains extra sml procedures for use with ProofPower to support the methods adopted at X-Logic.org.

I am using ProofPower for the following reasons:

1. I am familiar with it, having been involved in its development and application for many years.
2. It is designed to work with the real logical characters rather then ascii equivalents.
3. I like higher order logic, especially this variant.

The main claim to fame of ProofPower is its support for the Z specification language and the DERA compliance notation (for refining Z to Ada), however, I'm not making any use of these.

For a full understanding of the specifications in ProofPower HOL you need to look at the semantics of HOL and at the theories in the ancestry of the specification. For the semantics of the language you can either look at the informal mathematical semantics which is available from Cambridge for their system, or else at the formal specifications of ProofPower at the Lemma-1 site. For links to listings of the theories, see below. This is a simple language, but precise semantics is never easy.

This theory introduces the primitive vocabulary for this variant of higher order logic. There are just three constants and three type constructors.

The definitions of logical constants in terms of the primitive (undefined) constants. The ones defined are those which are needed to state the axioms.

The five axioms for the primitive logic.

Miscellaneous low level definitions (local definitions, conditionals, unique existence) and theorems.

The theory of ordered pairs, including Curry and Uncurry.

The theory of Natural numbers.

The theory of lists.

The theory of characters (of which there are only 256).

No content, parent is char. This is the highest point at which a new theory can be attached.

The theory of sets.

A type with just one element.

The theory of disjoint unions.

No content, parents are sets, sum and one.

The theory of binary relations.

The theory of integers.

The theory of dyadic operators.

The theory of orders.

The theory of real numbers.

The theory of real numbers.

The available proof context facilities are a bit cumbersome if you want to build up a proof context incrementatlly as you work your way through a theory. Here are some hacks to make that easier.