Vacancies within AI4FM

• PhD student position in Edinburgh (filled 20 September 2010)

  A PhD student position is available within the AI4FM project. The position will be within the Mathematical Reasoning Group at the School of Informatics in University of Edinburgh. The student will be supervised by Alan Bundy and Gudmund Grov. Apply here.
  View proposed PhD project description | Apply for PhD

  Details: The task allocated to this PhD will be to analyse ways in which proof attempts fail and are subsequently repaired. This analysis will be realised in a generic, strategy language for describing and classifying common forms of failure and repair. The strategy language will, in turn, be used, firstly, to describe how experts recover from failure and, secondly, to guide recovery during automated proof search of related proofs. Example failed proofs will be harvested from:

  1. the data from the toolset of Rodin formal methods system,
  2. the manual, expert proof attempts on source theorems,
  3. failed applications to target theorems of proof strategies abstracted from manual expert proofs of source theorems.

  Examples of repaired proof attempts will be harvested from the expert's work on failures of both types (1) and (2). This work will enhance the abilities of our prototype so it can benefit from initially failed proof attempts as well as successful ones.