MRG home page · Research · Publications · Projects · Software · People

Research in the MRG

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.

Mathematical Reasoning Group, Informatics Forum, 10 Crichton Street, Edinburgh, EH8 9AB, Scotland
Tel: +44 (0)131 650 2733      Fax: +44 (0)131 650 6899
Please send corrections and suggestions for this page to the DReaM Support Team
Unless explicitly stated otherwise all material on this web site is copyright © The University of Edinburgh.