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.