英国邓迪大学计算机学院博士后招聘

Postdoctoral Research Assistant
University of Dundee - Computing
Summary of Job Purpose and Principal Duties

Fixed term 13 months

Salary - Grade 7 point 29, £29,249

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).

Any Additional Information

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.

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.

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.

中国 （海归人才网）//www.baticalc.com为广大海外高层次人才提供回国就业、创业机会，关注海归生活。高层次人才交流QQ群：106247053 微博：http://weibo.com/liuxuehr