Boosting Automated Reasoning

A project which aims to use Machine Learning techniques to assist Automated Reasoning.

The use of theorem proving technology has become increasingly widespread, especially within the areas of software and hardware verification. However, often a considerable amount of human effort is required to guide theorem provers towards a proof, which means that the technology is only viable for relatively narrow families of systems that are particularly business or safety critical. To broaden their applicability, we have developed novel techniques that are able to learn successful proof patterns from existing corpora of proofs, and can apply these to automatically prove theorems at the push of a button.

For further information, Tom Gransden has produced a short video, which has been chosen as a finalist for the EPSRC 2015 ICT Young Pioneers competition.

 


People

Tom Gransden (Ph.D. Student)

Prof. Rajeev Raman

Dr. Neil Walkinshaw

Share this page: