PhD opportunities

Polarized Deduction Modulo Theory

Thesis proposal

Area of expertiseReal-time computer science, robotics, systems and control - Fontainebleau
Doctoral SchoolSMI - Sciences des Mtiers de l'Ingnieur
SupervisorM. Olivier HERMANT
Research unitMathematics and Systems
Keywordslogic, specifications
AbstractThe gist of Deduction Modulo Theory is to embed computation within proof
systems, by the means of rewrite rules. This speeds up theorem provers by
avoiding the need for axioms and emphasizing the computational and deter-
ministic nature of parts of proofs. It also offers a versatile and efficient way to
express proof assistants in a shallow way, when combined with a type system like
LF.

Polarized Deduction Modulo Theory [Dow10] is an improvement over De-
duction Modulo Theory [DHK03], that allows rewrite rules to be selectively
applied to the hypothesis or to conclusion side of proofs.

Currently, it has been successfully implemented in a resolution-based prover
[Bur11] and has given very promising results [BBC+17]. One of the advantages
of this approach is the possibility to express asymetric axioms. Moreover, the
generated rewrite system lends itself well to Skolemization, in particular in
classical logic, which further speeds up proof-seach.
ProfileAn M.Sc. specialization in computer science or in mathematics is a strong
requirement. A few basic courses either on logics (proof systems, proof assis-
tants), rewrite systems, or on functional programming, are recommended.
FundingConcours pour un contrat doctoral