This page contains links to the various software systems we distribute.
If you intend to use any of these you may wish to read
our disclaimer
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
