UTP and Circus Theories in ProofPower-Z

ProofPower is a suite of tools supporting specification and proof in Higher order Logic (HOL) and in the Z notation. By means of embedding the theories (relations, designs, reactive processes) of UTP in the theorem prover ProofPower-Z, formal proofs can be mechanically constructed. This work also provides a fundamental support for the refinement of Circus specifications.

• UTP and Circus Theories in ProofPower-Z (Version 2.7.6) - Download
• UTP and Circus Theories in ProofPower-Z (Version 2.7.5) - Download

ProofPower Theories for SBMF 2008 Paper

• ProofPower Theories with Definitions and Proofs presented in the Paper (proto-typical version)
• ProofPower Theories with Definitions and Proofs presented in the Paper (amended version)

The differences between the proto-typical and amended version are:

1. A wider selection of theorems and proofs in the amended version.
2. The representation of alphabetised predicates and UTP theories, which in the amended version do not record alphabets anymore but infer them dynamically from the universe where required.

To compile the SBMF 2008 theories, simply use the the command ‘make db’. ProofPower version 2.7.6 is required.

To generate an overview of documentation, the command ‘make doc’ can be used; PDF files for all theories are subsequently generated in the docs subdirectory.

Publications: