Panda (Proof assistant for natural deduction for all)
Ce
logiciel permet de construire des preuves en déduction naturelle pour
la logique des prédicats. Il s'adresse surtout aux étudiants en
informatique et logique niveau licence. Le but est de sensibiliser les
étudiants à la vérification automatique de preuve.
Ce logiciel
permet d'écrire soi-même des preuves en déduction naturelle pour la
logique des prédicats. La déduction naturelle est un système de preuve
qui correspond à la manière de raisonner d'un humain. Par exemple, de
"il pleut" et "il pleut implique que je prends mon parapluie", je
déduis "je prends mon parapluie". De manière abstraite, de A et "A
implique B", je déduis B. Une autre règle est : de "il pleut" et "il
fait nuit" je déduis "il pleut et il fait nuit". C'est à dire de A et
B, je déduis "A et B". La déduction naturelle propose une série de
règle de ce type qui couvre entièrement le raisonnement. Pour plus de
précision, n'hésitez pas à consulter Wikipedia.
Les preuves sont
présentées sous forme d'arbre de preuve complétement manipulables : on
peut coller des arbres de preuve ensemble, déplacer, supprimer etc.
L'intérêt est de faire comprendre la structure inductive d'une preuve
via une manipulation directe.
Pour toutes les preuves à l'écran,
le logiciel précise si les constructions sont correctes. Par exemple,
si de "A et B" je déduis B, le logiciel assure l'étudiant qu'il a bien
utiliser une règle de la déduction naturelle. Par contre, si l'étudiant
essaie de démontrer B à partir de "A ou B", alors le logiciel surligne
en rouge le passage de la preuve qui est erroné.
Le logiciel est
fourni avec une série d'exercice classé par niveau et est organisé
comme un jeu vidéo : si l'étudiant réussit à former une preuve correcte
pour la formule demandée, alors le logiciel montre qu'il a gagné. Le
premier niveau concerne la rédaction d'arbre de preuve simple en
déduction naturelle de formules de la logique des propositions :
l'étudiant doit normalement pouvoir construire des preuves à partir
d'un ensemble restreint de règles. Le deuxième niveau concerne
également la logique des propositions mais avec l'intervention de la
preuve par l'absurde : si de A je peux déduire la contradiction, alors
on prouve "non A". Les niveaux suivants concernent la déduction
naturelle pour la logique des prédicats dans toute sa généralité.
Le
logiciel permet également d'exporter une preuve écrite dans le langage
LaTEX pour une intégration directe dans un document LaTEX.
La syntaxe des formules est disponible ici.