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