Bienvenue aux Mines Paristech
Bienvenue à MINES ParisTech
Newsletter International
Website
Théorie & Pratique
Vous êtes

webTV

Lecture

Certificat exécutif : digital native, 3 questions à...

Lecture

Certificat exécutif : digital native, 3 questions à...

Lecture

Mastère Spécialisé AIMove: Artificial Intelligence and Movement in Industries and Creation

Lecture

Olivier Remy, third year student of the Corps des Mines

Lecture

Le Forum mécatronique 2019

+ Toutes les vidéos

Partager

Passage à l'échelle pour la théorie modulo déduction polarisée

Passage à l'échelle pour la théorie modulo déduction polarisée

Scaling Up Polarized Deduction Modulo Theory

Proposition de thèse

Spécialité

Informatique temps réel, robotique et automatique - Fontainebleau

Ecole doctorale

Ingénierie des Systèmes, Matériaux, Mécanique, Énergétique

Directeur de thèse

HERMANT Olivier

Unité de recherche

Mathématiques et Systèmes

Contact
Date de validité

01/10/2021

Site Web
Mots-clés

preuve de théorèmes, outils formels

theorem proving, formal tools

Résumé

Voir description en français

The 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.

Contexte

Formal methods aims at ensuring provably bug-free software. An industrial benchmark of ten of thousands of problems has given us the opportunity to jointly develop automated theorem provers and proof checkers.

Encadrement

Voir olivier.hermant@mines-paristech.fr

Profil candidat

Voir description en anglais

An 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.

Références

1. G. Burel, G. Bury, R. Cauderlier, D. Delahaye, P. Halmagrand, and O. Hermant. Automated deduction: When deduction modulo theory meets the practice. Journal of Automated Reasoning 64(6), pp. 1001–1060, 2020.
2. M. Boespflug, Q. Carbonneaux, and O. Hermant. The λΠ-calculus modulo as a universal proof language. In Second Workshop on Proof Exchange for Theorem Proving (PxTP), volume 878, pp. 28–43, CEUR-WS.org, 2012.
3. G. Dowek. Polarized deduction modulo. In IFIP Theoretical Computer Science, 2010.
4. The BWare Project, 2012. http://bware.lri.fr/

Type financement

Concours pour un contrat doctoral

Document PDF

https://www.adum.fr/script/downloadfile.pl?type=78&ID=34166

Retour à la liste des propositions

actualité

EcorcAir et les platanes du Quartier latin

Formation EcorcAir et les platanes du Quartier latin Vendredi 2 avril 2021, dernier jour de cours, en présentiel,…
> En savoir +

Félicitations à Rabab Akkouche

Formation Félicitations à Rabab Akkouche 16 candidats étaient en lice, dont 10 doctorants et docteurs…
> En savoir +

Prix de thèses de prospective de la Fondation 2100

Formation Prix de thèses de prospective de la Fondation… La cérémonie s'est déroulée le 9 février, sous la présidence…
> En savoir +

Femmes de science

Formation Femmes de science   Chercheuses confirmées, doctorantes ou élèves ingénieures, elles font la…
> En savoir +

Quelle empreinte environnementale pour notre avenir énergétique ?

Formation Quelle empreinte environnementale pour notre… Le doctorat est un exercice académique codifié qui aboutit à…
> En savoir +

+ Toutes les actualités

contact

Alexandra BELUS
Direction de l'Enseignement
Service du Doctorat
> envoyer un mail

Plan du site
MINES
ParisTech

60, Boulevard Saint-Michel
75272 PARIS Cedex 06
Tél. : +33 1 40 51 90 00

Implantations
Mentions légales | efil.fr | ©2012 MINES ParisTech | +33 1 40 51 90 00 |