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.

Comments are closed.