ProofPower
Introduction
 This page provides some information about ProofPower.
 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. ProofPower theory listings 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.
 Famous theorems in ProofPower 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. The ProofPower character set in HTML 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. X-Logic sml xtras This document contains extra sml procedures for use with ProofPower to support the methods adopted at X-Logic.org.
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: I am familiar with it, having been involved in its development and application for many years. It is designed to work with the real logical characters rather then ascii equivalents. 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.
 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.
ProofPower theory listings
 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.
 Listing of Theory min This theory introduces the primitive vocabulary for this variant of higher order logic. There are just three constants and three type constructors. Listing of Theory log The definitions of logical constants in terms of the primitive (undefined) constants. The ones defined are those which are needed to state the axioms. Listing of Theory init The five axioms for the primitive logic. Listing of Theory misc Miscellaneous low level definitions (local definitions, conditionals, unique existence) and theorems. Listing of Theory pair The theory of ordered pairs, including Curry and Uncurry. Listing of Theory %nat% The theory of Natural numbers.
 Listing of Theory list The theory of lists. Listing of Theory char The theory of characters (of which there are only 256). Theory basic_hol No content, parent is char. This is the highest point at which a new theory can be attached. Theory sets The theory of sets. Theory one A type with just one element. Theory sum The theory of disjoint unions.
 Theory hol No content, parents are sets, sum and one. Theory bin_rel The theory of binary relations. Theory %int% The theory of integers. Theory dyadic The theory of dyadic operators. Theory orders The theory of orders. Theory %real% The theory of real numbers. Theory analysis The theory of real numbers.
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.

privacy policy

Created:

\$Id: x005.xml,v 1.2 2008/04/06 13:07:17 rbj01 Exp \$

V