| EPSRC Reference: |
GR/M98012/01 |
| Title: |
AUTOMATIC CONJECTURE MAKING IN MATHEMATICS |
| Principal Investigator: |
Bundy, Professor A |
| Other Investigators: |
|
| Researcher Co-Investigators: |
|
| Project Partners: |
|
| Department: |
Sch of Informatics |
| Organisation: |
University of Edinburgh |
| Scheme: |
Standard Research (Pre-FEC) |
| Starts: |
01 November 1999 |
Ends: |
30 April 2003 |
Value (£): |
142,505
|
| EPSRC Research Topic Classifications: |
| Artificial Intelligence |
Fundamentals of Computing |
|
| EPSRC Industrial Sector Classifications: |
| No relevance to Underpinning Sectors |
|
|
| Related Grants: |
|
| Panel History: |
|
|
Summary on Grant Application Form |
|
Conjecture making is significant activity in mathematics, yet the question of producing mathematical conjectures by computer has only been addressed in isolated domains and with specialised techniques. We propose here to study and implement an important aspect of automatic conjecture making in mathematics: Cross Domain Conjecture making : to determine procedures which, when implemented, will enable a program to make conjectures involving concepts from many different areas of mathematics. We also propose to study and implement an important application of automatic conjecture making: 2Theorem proving by Theory Formation : to determine and exploit the advantages of automatically proving theorems in an environment where new concepts can be introduced and explored, calculations can be made and relevant lemmas can be formed, proved and used.By addressing cross domain conjecture making, we hope to derive techniques which will one day lead to programs able to assist mathematicians by providing useful and intelligent conjectures about objects of interest. Proving a theorem often requires calculations, finding examples, inventing definitions and making conjectures. By integrating mathematical software to enable all of these activities, we hope to demonstrate the advantages of proving theorems in a theory forming environment.
|
|
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 |