PhD opportunities

Polarized Deduction Modulo Theory

Area of expertise Real-time computer science, robotics, systems and control - Fontainebleau
Doctoral School SMI - Sciences des Mtiers de l'Ingnieur
Title Polarized Deduction Modulo Theory
Supervisor M. Olivier HERMANT
Research unit Mathematics and Systems
CRI - Centre de Recherche en Informatique
Keywords logic, specifications
Abstract The 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

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.
Funding Concours pour un contrat doctoral
Starting date October 1st 2017
Date of first publication May 16th 2017