Owner: RobArthan

Category: Application

A theorem prover for HOL, Z and a subset of Ada

ProofPower is a suite of tools supporting specification and proof in Higher Order Logic (HOL) and in the Z notation. It includes DAZ, a tool for specifying and verifying programs written in a subset of Ada.

Dependencies: OpenMotif 2.3 or later for the GUI

Platform: Linux, Mac OS, Cygwin

Poly/ML version: 5.7 and later

Licence: GPL v2.

Download link:

Project link: