The central theme of our research is machine assisted reasoning. We carry out research on the formalisation of mathematics, and the use of proof assistants for the verification and synthesis of software. A large part of our work is in investigating new theorem proving technology, and this is applied in the proof tools we are developing. We also have several other projects related to mathematical reasoning.
The former name of our research group (which still survives in our web address) was the Dream group, standing for Discovery and Reason in Mathematics. The aim was to try and characterise how mathematicians themselves do proofs, and to put this understanding to use in a tool or, to put it another way, to take an `AI approach' to theorem proving. This research is ongoing, and puts into practice the proof planning approach to theorem proving.
Past work in this area has included innovations such as rippling, middle-out-reasoning, critics, as well as work on user interfaces. This research has all fed into the proof planners, IsaPlanner, Lambda Clam, and its predecessor, Clam.
As well as continuing to work on the automated tools, IsaPlanner and Lambda Clam, we also pursue research on interactive theorem proving, using tools developed elsewhere, including Isabelle, Coq and HOL.
Some of the research in the group tackles the problem of formalising certain areas of mathematics, real analysis, in particular, in the Isabelle/HOL theorem prover, and proving substantial amounts of the theory therein. There is also work on using the proof planning paradigm to automate some of these proofs.