The Coq mailing list

[Gudmund Grov <ggrov AT staffmail.ed.ac.uk>]

--- 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 AT inf.ed.ac.uk
 , or
- Alan Bundy: 
bundy AT 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-productive-use-of-failure-in-formal-methods
- 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.