English
Integrating the Metis automatic theorem prover into the Coq proof assistant
Some automatic theorem provers like Metis not only proves theorems but also produces a trace that explains
why a given theorem holds.
This provides a simple and safe way of integrating them into other proof systems: one just needs to be capable of replaying traces.
Coq is a proof assistant with a higher-order logic with dependent types.
The goal of the internship is to automatise a subset of the logic
(first-order plus equality) by integrating the Metis automatic theorem
prover.
The requirements for this internship are an interest in logic and in
functional programming.
Français
Intégration du démontrateur automatique Metis à l'assistant de preuve Coq
Des systèmes de preuve automatique comme Metis non seulement prouvent des théorèmes mais aussi fournissent
une trace qui explique pourquoi le théorème prouvé est vrai. Ceci permet
un moyen sur et simple de les intégrer dans d'autres systèmes: il suffit
d'être capable de rejouer la trace.
Le système Coq est un assistant à la preuve
avec une logique d'ordre supérieure avec types dépendants.
L'objectif de ce stage est l'automatisation d'un sous-ensemble de cette
logique (la logique du premier ordre plus égalité) par l'intégration du système
de preuve automatique Metis.
Les prérequis pour ce stage sont un intérêt pour la logique et la programmation
fonctionnelle.
Laurent Théry