The Integration and Interaction of Multiple Mathematical Reasoning Processes

Overview

EPSRC Platform Grant EP/E005713/1 (RA0084)
Duration: 1 April 2007 - 31 March 2011

RA: Lucas Dixon
Grant Holders: David Aspinall, Alan Bundy, Simon Colton (Imperial), Louise Dennis (Liverpool), Jacques Fleuriot, Lilia Georgieva (Heriot Watt), Andrew Ireland (Heriot Watt), Paul Jackson, Alan Smaill, Graham Steel

Abstract from the original proposal:

The proposed platform grant will be used to provide essential infrastructure and exploratory activities that will support a portfolio of projects within the overall aims described below. The research aims of the Mathematical Reasoning Group are the automation of mathematical reasoning processes, including their analysis, development and interaction. These processes will include: concept formation; theory building; conjecture making; proof and counterexample finding the learning of new proof methods and critics; and the refinement, revision and maintenance of conjectures, representations and theories. A major focus will continue to be on mechanisms for guiding proof search, especially the further development of proof planning, and it will include both forma and'informal' reasoning, for instance, diagrammatic reasoning, schematic proof and the use of analogy, abstraction, reflection and symmetry. We expect to find applications of this work in formal methods of system design, commonsense reasoning, the computer-based teaching of mathematics and the provision of computational aids for mathematicians. Our work is a unique blend of the techniques of artificial intelligence and theoretical computer science.

This is a continuation of our previous platform grant (EP/E005713/1).

Related Projects

• A Generic Approach to Proof Planning - development of the IsaPlanner system
• Proof General - a generic interface for proof assistants.
• NuSPADE: Automatic Guidance for the Formal Verification of High Integrity Ada
• The Use of Proof in the Location of Programming Errors
• Theory Formation
• Discovering New Proof-Plans by Data-Mining
• Automated Analysis of Security Critical Systems
• Inferring Quality of Service Properties for Grid Applications
• Deductive Synthesis of Grid Workflows for e-Science
• Mechanising First-Order Temporal Logics
• Formal Verification of Computational Geometry
• Dynamic Ontology Refinement
• Modelling Lakatos-style Reasoning
• Coral - finding counterexamples to false inductive conjectures
• Recommender System for an Interactive Theorem Prover
• Anastasia - a functional programming editor that uses formal verification
• Proof critics
• MATHsAiD - automatically generating mathematical theorems
• Hierarchical Proofs and Graphs
• MathServe - a framework for integrating reasoning systems as Web Services

Related Organisations

The platform grant has supported our participation in the organisation of the following national and international academic meetings:

• The CIAO Series of Workshops
• The Types Project
• Scottish Theorem Provers Meetings
• The Automated Reasoning Workshop
• The Mathematical Knowledge Management Group
• The Calculemus Project

Visitors

Our group continues to attract a wide range and healthy number of visiting researchers, both short and long term. They report finding the environment of our group highly conducive to their research; they have access to a wide range of high-quality expertise and productive interaction in a friendly and constructive atmosphere. They also provide a dissemination route for our own research and tools.