ProofPower and its use at X-Logic.org
Overview
This provides information about ProofPower and the various formal theories developed at X-Logic.org using ProofPower.
Links to some of the theories which come with ProofPower, with brief descriptions. These are the ones above "basic-hol" which is the point at which OpenMind hangs off the tree.
This document contains extra sml procedures for use with ProofPower to support the methods adopted at X-Logic.org.
The formalisation of ZFC in ProofPower HOL and its applications.
Galactic Set Theory and some applications.
ProofPower and its logic
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.
Why ProofPower?

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.

Neither X-Logic nor OpenMind are tied to this particular proof tool, the idea is to be able to mix and match.

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.

ProofPower Documentation
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.
ZFC in HOL
The formalisation of ZFC in ProofPower HOL and its applications.
This document is a literate script containing the axiomatisation in ProofPower HOL of Zermelo-Fraenkel set theory.
This document proves some elementary consequences of the ZFC axioms in HOL, and then introduces further definitions relating to the representation of functions in set theory.
This document defines the concept of a pure function as a preliminary to introducing the type of pure functions.
GST in HOL
Galactic Set Theory and some applications.
This document is an overview of and conclusion to the work in which Galactic set theory is developed, creating the theory gst which should be cited as ancestor by applications of GST and a proof context suitable for applications.
This document defines the concepts "pure category" and "pure functor" as a preliminary to developing a foundation system whose domains of discourse are the pure categories and functors.
Formal Theory of Knowledge in Galactic Set Theory (in ProofPower).
Other documents
ProofPower theory listings
Links to some of the theories which come with ProofPower, with brief descriptions. These are the ones above "basic-hol" which is the point at which OpenMind hangs off the tree.
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.
Listing of Theory nat
The theory of Natural numbers, but sorry, I have an unresolved technical problem webbing this one. You can see it in the reference manual.
The theory of lists.
The theory of characters (of which there are only 256).
Theory basic_hol
This is a "cache" theory, which is a place were certain automatically generated theorems get stored, so the listing is not provided. I mention it because it is a child of all the above, the highest point at which users can hang new theories, and the attachment point for OpenMind/X-Logic theories.
X-Logic sml xtras
This document contains extra sml procedures for use with ProofPower to support the methods adopted at X-Logic.org.
Building Proof Contexts
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.

up quick index © RBJ

$Id: index.xml,v 1.1.1.1 2000/12/04 17:23:28 rbjones Exp $