This page contains links to the various software systems we distribute.
If you intend to use any of these you may wish to read
Supported and ongoing software projects:
- Proof General - a generic front-end for proof assistants (also known as interactive theorem provers).
- Victor - A SPARK Verification Condition Translator and Prover Driver
- IsaPlanner - a proof planner for Isabelle
- Quantomatic - a tool for graphically reasoning about quantum computation using models based on compact closed categories.
Older software projects (no longer being developed):
- HiGraph - a system for presenting and manipulating hierarchical proofs/graphs generated by proof planning in IsaPlanner. Currently just an editor/drawing tool for the graphs.
- Lambda Clam - a proof planner written in lambda prolog.
- HR - an automated theory formation system
- Clam proof planner with oyster - a proof planner written in prolog
- Clam version 3.2
- HOL-Clam - a link up between the HOL proof assistant and the Clam proof planner.
- Anastasia - a structural program editor
- Press - a prolog based system for solving symbolic, transcendental, non-differential equations