The Coq mailing list

[Ekaterina Komendantskaya <katya AT computing.dundee.ac.uk>]

 We have a fixed-term position at the School of Computing, Dundee

 for a postdoctoral researcher to  work on automated proof-mining.
More details below and  at
http://www.computing.dundee.ac.uk/staff/katya/mlcap.html

 For further enquiries please email me:
 Katya Komendantskaya 
<katya AT computing.dundee.ac.uk>


                          School of Computing
                        University of Dundee

            Postdoctoral Researcher in Automated Proof-Mining
                 Fixed-term position.

           Start date: between 1 March 2012 and 1 January 2013;

           End date:  28 February 2014.

               Closing Date for applications: 15 April 2012.

 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 (e.g. 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; 
although
this negative information could be re-used as well.
At present, this kind of proof-pattern recognition
and proof-pattern 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/interactive theorem provers or the state-of-the art
statistical
 pattern-recognition techniques.


 Ekaterina Komendantskaya
 Lecturer
 School of Computing
 University of Dundee
 Dundee,
 Scotland
 DD1  4HN
 Tel: (+44) 01382384820