Postdoctoral position on first-order theory of rewriting, Innsbruck (Austria)

The Computational Logic research group is looking for a postdoctoral researcher in connection with the FWF (Austrian Science Fund) project "FORTissimo: Automating the First-Order Theory of Rewriting". The project runs for 3 years starting from 1 September 2017. The main task of a successful applicant will be to collaborate with other project members in order to extend the Isabelle Formalization of Rewriting with the decision procedure for the first-order theory of rewriting for left-linear and right-ground rewrite systems.

Candidates must hold a PhD degree in computer science or mathematics. Knowledge of automata theory and rewriting is helpful, experience with and a liking of working with proof assistants (preferably Isabelle/HOL) is desirable. Candidates close to obtaining a PhD degree are also invited to apply. Knowledge of German is not required.