Mécanisation des preuves (
PPS)
Membres:
Sylvain Baro
(baro@pps.jussieu.fr)
Yves Legrandgérard
(ylg@logique.jussieu.fr)
Pascal Manoury
(Pascal.Manoury@pps.jussieu.fr)
Micaela Mayero
(mayero@pps.jussieu.fr)
Michel Parigot
(parigot@logique.jussieu.fr)
Paul Rozière
(roziere@pps.jussieu.fr)
Marianne Simonot
(simonot@cnam.fr)
Présentation:
Ce groupe de travail concerne l'étude et la conception d'un système d'aide à
la preuve "simple" d'utilisation. On s'intéresse, en particulier, &agreve; l'élaboration
d'un prouveur dédié aux mathématiques et pourvu d'une interface le rendant,
entre autre, accessible à l'enseignement. Le schéma ci-dessous donne l'architecture
globale du système.
L'interface (implantée avec le langage python) communique avec le (les) moteur(s)
de preuve et, à terme, plusieurs sessions indépendantes pourront tourner en
parallèle, grâce à un processus de sauvegarde et de restauration, une session
étant une liste de définitions, déclarations, théorèmes et preuves.
Le prouveur est basé sur une logique classique d'ordre supérieur sans typage, à
la PhoX, contenant des tactiques génériques manipulant les connecteurs de base,
une tactique automatique et des tactiques extensibles par l'utilisateur. L'introduction
de de types inductifs et dépendants est à l'étude.
L'aspect "sortie en langue naturelle" (texte complet incluant des anaphores) est
également pris en compte afin de faciliter l'utilisation du prouveur. Le travail de
Adil El Ghali sur PhoX pourra en être la base.
Actuellement, l'implantation concerne surtout l'interface et une partie du moteur de
preuves. Un éditeur de preuves jouet est à l'étude.
Principales interactions:
Groupes de travail:
- 10/07/2003 à 14h30 en salle 0C6.
Sylvain Baro: soutenance de
thèse: conception et implémentation d'un système d'aide à la spécification
et à la preuve de programmes ML
- 23/06/2003. Pascal Manoury, Paul Rozière:
à propos du système CL de Voda
- 16/06/2003. Klaus Grue: démo de son
système
- 26/05/2003. Adil El Ghali:
propositions/discussion sur l'interface de PhoX
- 03/03/2003. Jean Duprat: formalisation
de la géométrie à la règle et au compas dans Coq
- 17/02/2003. Adil El Ghali: structuration de document à la SDRT pour les preuves mathématiques
- 03/02/2003. discussion au sujet du format d'échange pour les données
- 24/01/2003. Paul Rozière: formalisation
de la géométrie
- 17/01/2003. Micaela Mayero: les types
dépendants
- 10/01/2003. Pascal Manoury: preuve de
terminaison de programmes fonctionnels
- 29/11/2002. Pascal Manoury: EPJ, un
éditeur de preuves jouet
- 15/11/2002. Yves Legrandgérard:
interface
- 25/10/2002. Paul Rozière: organisation
de tactiques dans PhoX
- 18/10/2002. Adil El Ghali: GePhox, un
générateur à la sortie de Phox
- 04/10/2002. Organisation
Page maintenue par Micaela
Mayero
Last modified: June 20 16:30:00 MET DST 2003