Projects per year
Abstract / Description of output
The aim of the MATHsAiD project is to build a tool for automated theoremdiscovery; to design and build a tool to automatically conjecture and prove theorems (lemmas, corollaries, etc.) from a set of usersupplied axioms and definitions. No other input is required. This tool would, for instance, allow a mathematician to try several versions of a particular definition, and in a relatively small amount of time, be able to see some of the consequences, in terms of the resulting theorems, of each version. Moreover, the automatically discovered theorems could perhaps help the users to discover and prove further theorems for themselves. The tool could also easily be used by educators (to generate exercise sets, for instance) and by students as well. In a similar fashion, it might also prove useful in enabling automated theorem provers to dispatch many of the more difficult proof obligations arising in software verification, by automatically generating lemmas which are needed by the prover, in order to finish these proofs.
Original language  English 

Pages (fromto)  585606 
Number of pages  22 
Journal  Applied Intelligence 
Volume  47 
Issue number  3 
Early online date  23 Jun 2017 
DOIs  
Publication status  Published  Oct 2017 
Keywords / Materials (for Nontextual outputs)
 Automated theory exploration
 Mathematics
 Automated theorem proving
Fingerprint
Dive into the research topics of 'MATHsAiD: Automated Mathematical Theory Exploration'. Together they form a unique fingerprint.Projects
 2 Finished

The integration and interaction of multiple mathematical reasoning processes
Bundy, A., Aspinall, D., Fleuriot, J., Jackson, P., Smaill, A., Colton, S., Ireland, A. & Michaelson, G.
1/08/11 → 31/07/15
Project: Research
