'HR Excellence in Research' logo awarded to institutions actively implementing the European Charter and Code for Researchers.
Please note that the job is no longer active!
In this model we advance a theorem-proving method named DPLL (Gamma+T), that combines the strenghts of inference systems for first-order logic with equality and SMT-solvers, where SMT means satisfiability modulo theories. This method was already shown to yield decision procedures. One of its key properties is that it works by building a tenative model, and its deductions are guided by the existing candidate model. In this project we plan to work towards three objectives: developing a general methodology for model-based deduction; obtaining new decision procedures from DPLL (Gamma+T); and improving the DPLL (Gamma+T)'s capability of deciding unsatisfiability by detecting the absence of models of a given finite cardinality.
Please note that the full description may be available in the national language since some job boards have their own publication policy. Thank you for your understanding!
The competition will be carried out by an evaluation of titles and examination by means of an interview.
To better plan and organise their stay in a foreign European country, researchers and their families can also benefit of the free and personalised assistance offered by the EURAXESS Services Centres, a network of more than 200 centres located in 40 different European countries.