Supported and ongoing software projects: * IsaPlanner - a proof planner for Isabelle * 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. * Quantomatic - a tool for graphically reasoning about quantum computation using models based on compact closed categories. Older software projects (no longer being developed): * 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
IsaPlanner is a generic framework for proof planning in the interactive theorem prover Isabelle. It facilitates the encoding of reasoning techniques, which can be used to conjecture and prove theorems automatically. The system provides an interactive tracing tool that allows you to interact the proof planning attempt. (see the screenshot of IsaPlanner being used with Isabelle and Proof General) It is based on the Isabelle theorem prover and the Isar language. The main proof technique written in IsaPlanner is an inductive theorem prover based on Rippling. This is applicable within Isabelle's Higher Order Logic, and can easily be adapted to Isabelle's other logics. The system now the main platform for proof planning research in the Edinburgh mathematical reasoning group
Vampire is winning at least one division of the world cup in theorem proving CASC since 1999. All together Vampire won 17 titles: more than any other prover. We traditionally take part in the following two divisions of the competition: * The FOF division: unrestricted first-order problems. This division was ranked second in importance after the MIX division before 2007 and is now recognised as the main competition division. * The CNF division: first-order problems in conjunctive normal form. This division was called MIX before 2007 and recognised as the main competition division. We also participate in other, more special competition divisions but Vampire is not specialised for them so our achievements are mostly modest.