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