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