MRG Projects

Approaches to Reasoning

• The Integration and Interaction of Multiple Mathematical Reasoning Processes
• A Cognitively Based Model of Theory Formulation and Reformulation
• Dynamic Ontology Refinement
• Theory Formation
• Distributed Theorem Proving
• Ontology Evolution in Physics
• A Category-Theoretic Framework for Ontology Management
• Proof Engineering: Refactoring Proof: developing refactoring techniques for proof scripts.
• Proof Guided Ontology Development

Proof Planning

• A Generic Approach to Proof Planning - development of the IsaPlanner system
• Automated Discovery of Inductive Lemmas

Applications and Case Studies

• Security and Verification:
  • Automated Analysis of Security Critical Systems
  • Coral - finding counterexamples to false inductive conjectures
  • NuSPADE: Automatic Guidance for the Formal Verification of High Integrity Ada
  • The Use of Proof in the Location of Programming Errors
• Mathematics and Formalisation:
  • Formal Verification of Computational Geometry
  • Isabelle Projects
  • MATHsAiD - Automatically generating mathematical theorems
  • Quantomatic - Automated Reasoning for Quantum Computations
• the Grid, E-Science, Web Services and Beyond:
  • Inferring Quality of Service Properties for Grid Applications
  • Deductive Synthesis of Grid Workflows for e-Science
  • MathServe - a framework for integrating reasoning systems as Web Services
  • Open Knowledge Project - a unifying framework for Web service composition

User Interfaces for Reasoning Systems

• PolyML - Our various Standard ML/PolyML projects
• Recommender System for an Interactive Theorem Prover
• Anastasia - a functional programming editor that uses formal verification
• Hierarchical Proofs and Graphs (HiProofs and HiGraphs)
• Proof General - a generic interface for proof assistants.