ProofPower Specifications and Proofs

Contributing Documentation Download Examples Getting Home Mailing List Papers Patches Specifications

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 ProofPower documentation.

Created by Rob Arthan [rda at lemma-one dot com]

Last updated: $Date: 2004/06/28 13:13:54 $