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: https://www.github.com/RobArthan/pp
Project link: http://www.lemma-one.com/ProofPower/index/index.html