EPSRC Reference: 
EP/F033559/1 
Title: 
Automated Theorem Discovery 
Principal Investigator: 
Bundy, Professor A 
Other Investigators: 

Researcher CoInvestigators: 

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 multistage project, the longterm 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 buildup of Theorems. This is especially true for certain formal verification problems, in which stateoftheart 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 nonacademic 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 