Details of Grant 

EPSRC Reference:	EP/F033559/1
Title:	Automated Theorem Discovery
Principal Investigator:	Bundy, Professor A
Other Investigators:	Smith, Professor PF
Researcher Co-Investigators:	Dr RL McCasland
Project Partners:
Department:	Sch of Informatics
Organisation:	University of Edinburgh
Scheme:	Standard Research
Starts:	01 November 2007	Ends:	31 December 2011	Value (£):	413,817
EPSRC Research Topic Classifications:	Fundamentals of Computing
EPSRC Industrial Sector Classifications:	No relevance to Underpinning Sectors
Related Grants:
Panel History:	Panel Date Panel Name Outcome 18 Oct 2007 ICT Prioritisation Panel (Technology) Announced
Summary on Grant Application Form
This project represents the second stage of a multi-stage project, the long-term goal of which is to emulate a large portion of the human mathematical discovery process. The focus of this particular stage is on fully developing and deploying an Automated Theorem Discovery (ATD) system. By ATD system we mean a system that automatically generates, proves and identifies a significant number of mathematical results which mathematicians are likely to recognize as Theorems, Lemmas, Corollaries, etc. (as opposed to the sorts of results which, true though they might be, would probably not be deemed worthy of recording).Generations of mathematicians have appreciated the benefits of building a mathematical knowledge base bit by bit, Theorem by Theorem, in that previously discovered results often prove quite useful -- perhaps even necessary -- in the discovery and the proof of subsequent results. Moreover, since the advent of the modern computer, it has become increasingly apparent that automated reasoning (AR) systems can likewise benefit from a similar incremental build-up of Theorems. This is especially true for certain formal verification problems, in which state-of-the-art automated theorem provers can dispatch some -- but not all -- of the generated proof obligations. The remaining proofs can only be achieved once certain Lemmas have been discovered; at present, this discovery must be done by hand.We therefore anticipate that an effective and practical ATD system would be very useful, not only to mathematicians, but to computer scientists as well -- particularly those who work in formal verification. Indeed, in the latter case, we have supporting evidence (in the form of letters of support) that the potential payoff for such a system is huge.
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