Over the past few years I have been involved in the creation of a number of systems/frameworks/mechanized theories for automated reasoning in a range of domains. These include:
- Formalized theories of Real and Complex analysis in Isabelle/HOL.
- The formalization of Nonstandard Analysis in Isabelle/HOL.
- A theorem proving framework for rigorous Web-Services composition (ongoing work with P. Papapanagiotou in HOL Light).
- Idle-time Discovery Engines for Interactive Theorem Provers (ongoing work with P. Scott in HOL Light).
- Isabelle Light, an Isabelle-like procedural language/framework for HOL Light (with P. Papapanagiotou).
- Boyer-Moore Inductive Proof Tool for HOL-Light (with P. Papapanagiotou).
- The Prover’s Palette: An Eclipse IDE for Isabelle that integrates external tools around the user (with L. Meikle).
- Geometry Explorer, a system that combines dynamic geometry, automated geometry theorem proving, and diagrammatic proofs (with S. Wilson).
- IsaPlanner, a proof-planning system implemented as part of Isabelle. The project was initiated under my EPSRC Grant GR/N37414 and is now supported by the Mathematical Reasoning Group Platform Grant.