Details of Grant 

EPSRC Reference:	GR/M45030/01
Title:	COMPUTATIONAL MODELLING OF MATHEMATICAL REASONING
Principal Investigator:	Bundy, Professor A
Other Investigators:	Lowe, Dr H Fleuriot, Dr J Jackson, Dr PB Colton, Professor S Smaill, Dr A Ireland, Professor A Fleuriot, Professor J Dennis, Dr L
Researcher Co-Investigators:
Project Partners:	Ifad A/S
Department:	Sch of Informatics
Organisation:	University of Edinburgh
Scheme:	Standard Research (Pre-FEC)
Starts:	01 October 1998	Ends:	30 June 2003	Value (£):	914,659
EPSRC Research Topic Classifications:	Artificial Intelligence
EPSRC Industrial Sector Classifications:	Information Technologies
Related Grants:
Panel History:
Summary on Grant Application Form
We propose to continue our study of mathematical reasoning processes and their interaction. In particular, we propose to continue our exploration of the central role played by the explicit representation of proof plans in a meta-theoretical calculus. Our main application will continue to be inductive proofs, in general, and the application of these proofs to formal methods of system development. These proof plans will be implemented in our CLaM, LambdaClaM and XBarnacle systems.
Key Findings
This information can now be found on Gateway to Research (GtR) http://gtr.rcuk.ac.uk
Potential use in non-academic contexts
This information can now be found on Gateway to Research (GtR) http://gtr.rcuk.ac.uk
Impacts
Description This information can now be found on Gateway to Research (GtR) http://gtr.rcuk.ac.uk Summary Date Materialised
Sectors submitted by the Researcher
This information can now be found on Gateway to Research (GtR) http://gtr.rcuk.ac.uk
Project URL:
Further Information:
Organisation Website:	http://www.ed.ac.uk