ProofPower Specifications and Proofs
This directory contains a selection of documents containing formal specifications or proofs.
These include some of the formal specifications of ProofPower,
those concerned with the Logic implemented in ProofPower and high level
aspects of ProofPower itself.
The papers are supplied as PDF files.
- spc001.pdf - HOL Formalised: Language and Overview
- spc002.pdf - HOL Formalised: Semantics
- spc003.pdf - HOL Formalised: Deductive System
- spc004.pdf - HOL Formalised: Proof Development System
- spc005.pdf - HOL Formalised: Formal Design of the Logical Kernel
- wrk022.pdf - A generic treatment of modal logic in ProofPower HOL
- wrk043.pdf - Ramsey's Theorem in ProofPower (HOL)
- wrk044.pdf - Theorems on Finiteness (in HOL, for use in wrk043)
Some scripts which used to be on a predecessor of this page are now incorporated in the
ProofPower system, so you may like to read some of the
Copyright © Lemma 1 Ltd.
Created by Rob Arthan
Last updated: $Date: 2004/06/28 13:13:54 $