--- apologies for multiple postings --- The mathematical reasoning research group in the School of Informatics at the University of Edinburgh is advertising for a PhD funded by the EPSRC project "AI4FM: Using AI to aid automation of proof search in Formal Methods". The proposed topic of the PhD is "The Productive Use of Failure in Formal Methods". ** DESCRIPTION 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 (a) the data from the toolset of Rodin formal methods system, (b) the manual, expert proof attempts on source theorems and (c) 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 (b) and (c). This work will enhance the abilities of our prototype so it can benefit from initially failed proof attempts as well as successful ones. ** DEGREE OF DIFFICULTY A challenging project that requires mathematical sophistication, analytic skills and creativity in constructing the strategy language. ** BACKGROUND NEEDED A background in mathematics, logic or formal methods is required to provide the necessary mathematical maturity to undertake this project. ** CONTACT If you have any queries, please contact: - Gudmund Grov: ggrov@inf.ed.ac.uk , or - Alan Bundy: bundy@inf.ed.ac.uk. Please use our Schools PhD application page (see below) for applications. ** SOME LINKS - A description of the proposed PhD project: http://wcms.inf.ed.ac.uk/pgrguide/prospectus/projects-container/the-producti... - The web page for the AI4FM project: http://www.ai4fm.org/ - Our School's PhD application page: http://www.inf.ed.ac.uk/postgraduate/phd.html ** IMPORTANT DATES There is no deadline for this application, but we do recommended candidates to apply as soon as possible since the position may be allocated without further notice. We are fairly flexible on the starting date, but would ideally like it to start between October 2010 and April 2011. ** ABOUT THE RESEARCH INSTITUTION AND RESEARCH GROUP The Edinburgh School of Informatics obtained the highest volume of 4* activity in its unit of assessment in RAE 2008. It contains world-class research groups in the areas of theoretical computer science, artificial intelligence and cognitive science. The Mathematical Reasoning Group in the School of Informatics has been engaged on the computational analysis, development and application of mathematical reasoning processes and their interactions since the mid 1970s (http://dream.inf.ed.ac.uk/). Its work is characterised by its unique blend of computational theory with artificial intelligence. It has pioneered work on proof planning, tactic learning, and ontology construction and evolution. -- The University of Edinburgh is a charitable body, registered in Scotland, with registration number SC005336.