swMATH ID: 6339
Software Authors: Roger Jones; Arthan, R.D.; Dave King; Lemma 1 Ltd
Description: ProofPower is a specification and proof tool based on an implementation of Higher Order Logic (HOL), following the LCF paradigm, in Standard ML. ProofPower provides support for specification and proof in Z using a semantic embedding of Z into HOL. The DAZ tool supporting refinement of Z to the SPARK subset of Ada is also available.
Homepage: http://www.lemma-one.com/ProofPower/index/
Keywords: theorem prover
Related Software: Circus; Z; HOL; Isabelle/HOL; HOL Light; Isabelle; PVS; Coq; ML; ClawZ; ArcAngel; Z/EVES; Isabelle/Circus; ZRC; OpenTheory; ArcAngelC; seL4; Mizar; Isabelle/UTP; HOL Zero
Cited in: 52 Documents
Further Publications: http://www.lemma-one.com/ProofPower/papers/papers.html

Citations by Year