site perso d’Emmanuel Dieul contact
plan du site
Photos
Expériences professionnelles
Logiciels
CV et références

PROSE : prouveur de séquent

lundi 16 novembre 2009

PROSE, pour PROuveur de SEquents, est un prouveur basé sur la logique du premier ordre (calcul des prédicats avec égalité). Il sert donc à prouver, automatiquement (dans la mesure du possible) ou manuellement, des propriétés assez simples.

JPEG - 46 ko
modification manuelle d’une preuve générée automatiquement

Le développement de PROSE ne suivant pas les règles d’un développement sécuritaire, il ne peut garantir la preuve fournie. Toutefois, il fournira une suffisamment bonne vision de la preuve globale à réaliser dans un prouveur (atelier B, Coq, PVS...).

Fonctionnalites

- la preuve interactive de sequent en logique des prédicats avec égalité
- la gestion complète des preuves en librairies
- l’impression de preuves dans un fichier ASCII ou sur imprimante
- la possibilité de passer interactivement du mode automatique en mode manuel et réciproquement
- l’affichage des règles de preuves appliquées sous forme d’arbre
- la possibilité de changer, à tout point de l’arbre, la règle de logique appliquée
- un mode console automatique

Origine

Ce projet vient d’un projet du DESS de Développement de Logiciels Sûrs que j’ai suivi à Paris VI et au CNAM (diplôme cautionné conjointement par les deux centres). Ce projet était à faire en 2-3 mois.

Au départ, il fonctionnait en mode automatique uniquement (au moment où il a reçu la note de 18/20). Je crois bien d’ailleurs que nous étions les seuls du DESS à faire un mode automatique...

Je l’ai augmenté, par la suite, d’un mode manuel. C’est la version qui vous est proposée ici.

Documentation

La documentation de ce petit outil à été rédigée dans le cadre du projet de DESS. Elle est disponible via l’icône ci-dessous.

PDF - 480 ko
prose-documentation.pdf

Exécutable

Zip - 2.6 Mo
prose-windows.zip

Le seul exécutable accessible ici est un exécutable pour windows.

Il est livré avec les librairies GTK et Cygwin pourqu’il puisse fonctionner de manière autonome. Il suffit de le décompresser dans un dossier et de lancer l’exécutable tel quel.

Dans une future version, je prévois de remettre PROSE au goût des nouvelles interfaces de GTK, de rapprocher sa syntaxe à celle du B et de rendre l’outil plus indépendant des règles de preuve, un peu à la manière de l’atelier B.