PhD opportunities

Scaling Up Polarized Deduction Modulo Theory

Thesis proposal

Area of expertiseReal-time computer science, robotics, systems and control - Fontainebleau
Doctoral SchoolSystems Engineering, Materials, Mechanics, Energy
SupervisorM. Olivier HERMANT
Research unitMathematics and Systems
Starting dateOctober 1st 2021
Keywordstheorem proving, formal tools
AbstractThe research subject aims at extending those tools and their logical foundations in the direction of polarized rewriting, where conditional computation steps are embedded into reasoning step, a feature that gave excellent preliminary results on the benchmark.
Our tools are also critically dependent on the strategy adopted. As this strategy is dependent on the shape of the problem, another part of the research subject is to learn automatically how to trigger the best heuristics.
ProfileAn M.Sc.-level specialization in any field of computer science or in the foundations of mathematics. More specialized courses, among which machine learning, compilers, logics, theoretical computer science, or functional programming are a plus.
FundingConcours pour un contrat doctoral