Job Vacancies
Postdoctoral Research Assistant
Salary: Grade 7 (£29,249 - £35,938
The School of Computing at the University of Dundee invites applications for a postdoctoral researcher to work on an Automated Proof-Pattern Recognition project, entitled Machine-Learning Coalgebraic Automated Proofs (ML-CAP).
This project will run in collaboration with a bigger AI4FM project (http://www.ai4fm.org/), based in the Universities of Edinburgh, Heriot-Watt, Newcastle.
The project is focused on the statistical/inductive aspects of
automated theorem proving ; namely, on applications of proof-pattern recognition in proof-search.
Automated theorem provers of different kinds -- interactive and higher-order
(e.g. HOL or Coq) or automated first-order (Prover9, Event-B) have been
successfully developed into sophisticated environments for mechanised proofs.
Whether these provers are applied to big industrial tasks in software
verification, or to formalisation of mathematical theories, a programmer may
have to tackle thousands of lemmas and theorems of variable sizes and complexities. A proof in such languages is constructed by combining a finite number of tactics. Some proofs may yield the same pattern of tactics, and can be fully automated, and others may require a user's intervention. In this case, manually found proof for one problematic lemma may serve as a template for several other lemmas needing a manual proof. Another issue is that unsuccessful attempts of proofs occurring in the trial-and-error phase of proof-search, are normally discarded once the proof is found. At present, this kind of proof-pattern recognition and recycling is done by hand, and the ML-CAP project will look into methods to automate this.
We are looking for a researcher to spend up to 13 months in the Dundee
team developing ML-CAP techniques. This will involve close
collaboration with the existing group members, as well as interaction
with the project partners in the mentioned UK universities. Research experience in computer science or mathematics is essential, as is some knowledge of either automated theorem provers or the state-of-the art statistical pattern-recognition techniques.
Contact Dr Ekaterina Komendantskaya.
Application Date: 15/04/2012