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
LambdaCLAM is a tool for automated theorem proving in higher order domains. In particular LambdaCLAM specialises in proof using induction based on the rippling heuristic. LambdaCLAM is a higher-order version of CLAM. Both CLAM and LambdaCLAM use proof planning to guide the search for a proof A proof plan is a proof of a theorem at some level of abstraction presented as a tree. Each node in this tree is justified by a tactic. The exact nature of these tactics is unspecified, they may be sequences of inference rules, programs for generating sequences of inferences or a further proof plan at some lower level of abstraction. In principle while the generation of the proof tree may have involved heuristics and (possibly) unsound inference steps, it can be justified by executing the tactics attached to the nodes.
Despite Prolog's logic heritage and its use of theorem-proving unification and resolution operations, Prolog fails to qualify as a full general-purpose theorem-proving system. There are three main reasons: (1) many Prolog systems use an unsound unification algorithm, (2) Prolog's unbounded depth-first search strategy is incomplete, and (3) Prolog's inference system is not complete for non-Horn clauses. Nevertheless, Prolog is quite interesting from a theorem-proving standpoint because of its very high inference rate as compared to conventional theorem-proving programs. The objective of the Prolog Technology Theorem Prover (PTTP) is to overcome the deficiencies while retaining as fully as possible the high performance of well-engineered Prolog systems.
A. Kabbaj, B. Moulin, J. Gancet, D. Nadeau, and O. Rouleau. Proceedings of the 9th International Conference on Conceptual Structures (ICCS 2001), volume 2120 of Lecture Notes in Computer Science, page 346-359. Springer, (2001)
A. Kabbaj. Proceedings of the 14th International Conference on Conceptual Structures (ICCS 2006), volume 4068 of Lecture Notes in Computer Science, page 286-299. Springer, (2006)