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):
  • 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.

Comments are closed.