How to apply: The application forms should be submitted on-line; the job reference is ASE0120.
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, 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.
For further enquiries please email me: katya@computing.dundee.ac.uk