Listings of some theories built into ProofPower
Overview
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.

up quick index © RBJ

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