Email Gateway (Aug 18 2022 at 15:22): Email Gateway (Aug 18 2022 at 15:22):From: Gudmund Grov <ggrov@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:
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.
Last updated: Nov 21 2024 at 12:39 UTC