European Companies Search Engine
UK funding (£413,817): Automated Theorem Discovery Ukri1 Nov 2007 UK Research and Innovation, United Kingdom
Overview
Text
Automated Theorem Discovery
| Abstract | 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. |
| Category | Research Grant |
| Reference | EP/F033559/1 |
| Status | Closed |
| Funded period start | 01/11/2007 |
| Funded period end | 31/12/2011 |
| Funded value | £413,817.00 |
| Source | https://gtr.ukri.org/projects?ref=EP%2FF033559%2F1 |
Participating Organisations
| University of Edinburgh |
The filing refers to a past date, and does not necessarily reflect the current state. The current state is available on the following page: University OF Edinburgh CHARITY, Edinburgh.
The visualizations for "University of Edinburgh - UK funding (£413,817): Automated Theorem Discovery"
are provided by
North Data
and may be reused under the terms of the
Creative Commons CC-BY license.
