Over the years I have been involved in the creation of a number of AI reasoning systems and frameworks, and mechanized theories. These include (note: not up-to-date, see also our AIML web page):
- Digiflow Tool (work with the WorkflowFM/Digiflow team that includes P. Papapanagiotou, James Vaughan and Filip Smola). Following this project, we have recently released the following components of WorkfloFM as open source software (2021):
- WorkflowFM Reasoner/Logic Engine for correct-by-construction reasoning (in HOL Light).
- WorkflowFM Visual Composer.
- Archive of Formal Proof submission on mechanising Schutz’ Independent Axioms for Minkowski Spacetime in Isabelle/HOL. (2021)
- An unofficial version of the Archive of Formal Proof (which is currently being incorporated into the official AFP) (2021).
- Source code available here.
- Formalized theories of Real and Complex analysis in Isabelle/HOL.
- The formalization of standard and Nonstandard Analysis in Isabelle/HOL.
- A theorem proving framework for rigorous process modelling (ongoing work with P. Papapanagiotou in HOL Light).
- Idle-time Discovery Engines for Interactive Theorem Provers (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 then supported by the Mathematical Reasoning Group Platform Grant.