Panda

Site officiel
screenshot_panda
Bookmark and Share

Ce logiciel s’adresse surtout aux étudiants en informatique et logique niveau licence. Il permet de construire des preuves mathématiques, en déduction naturelle, pour la logique des prédicats. Le but est de sensibiliser les étudiants à la vérification automatique de preuves : « oui, un ordinateur peut vérifier qu’une preuve mathématique est correcte. »

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”. J’en déduis que “je prends mon parapluie”. De manière abstraite, si A et “A implique B”, alors je déduis B. La déduction naturelle propose une série de règles de ce type qui couvre entièrement le champ du raisonnement. Pour plus de précision, n’hésitez pas à consulter Wikipédia.

Les preuves sont présentées sous forme d’arbres de preuves complètement manipulables : on peut coller des arbres de preuve ensemble, les déplacer, les 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 utilisé 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’exercices classés par niveaux 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.

Contexte

Panda est un logiciel qui permet aisément de construire des arbres de preuve en déduction naturelle. Il existe d’autres assistants permettant de réaliser cette tâche : Pandora, Jape etc. Les autres assistants sont plus complets concernant la diversité des logiques traitées. Panda se cantonne à la logique des prédicats classique. Par contre, Panda offre une interface agréable et assure que l’étudiant ne se noie pas dans les concepts plus compliqués des autres assistants. Il existe également de “vrais” assistants de preuve comme Coq, Isabelle… qui sont hors propos pour des étudiants débutants en logique, car difficile à utiliser (nécessite un apprentissage du langage similaire à CaML adapté aux preuves etc., utilisation de la ligne de commande).

Commentaire

Panda a permis aux étudiants de L2 informatique de s’initier à la déduction naturelle de manière ludique. Panda a également permis à un étudiant à mobilité réduite (et qui ne pouvait pas écrire) d’établir des preuves en déduction naturelle.

Merci à François Schwarzentruber pour la rédaction originale de cette notice dans notre wiki.

Tags:
Ajouter des tags (séparés par des virgules ou des espaces) :
 
Attention: tous les caractères spéciaux sont interdits (sauf le .). Les tags n'apparaîtront qu'au prochain rafraichissement du cache (dans plusieurs heures).

<< Mettre à jour >>
:: lien mort :: orthographe :: nouveauté :: mise à jour ::

Vous souhaitez mettre à jour la notice ? La première chose à faire est de déterminer s'il s'agit d'une mise à jour mineure ou d'une mise à jour majeure Icone d'aide.

  • Mineure : un lien mort, des fautes d'orthographe, un lien à ajouter ou encore une petite précision.

    Veuillez renseigner les champs ci dessous :

  • Majeure : une nouvelle version avec des nouveautés, des changements majeurs.

    En cochant cette case, vous allez créer une page sur le wiki afin de mettre à jour la notice.

Commentaires

<< Poster un message >>
:: question :: précision :: avis :: commentaire :: bug ::

Informations complémentaires

Faire un don ? (défiscalisé)

Faire un DON

Aidez-nous à atteindre notre objectif de 800 donateurs récurrents pour assurer notre pérennité et notre développement ! (nous n’y sommes plus très loin).

Je soutiens Framasoft pour 10€/mois

Framasoft needs you !

 Vous trouverez ici une liste de logiciels qui ont fait acte de candidature et qui n’attendent que vous pour réussir avec brio l’examen d’entrée dans notre annuaire.

Informations générales

Juste une image

shut up you white bitch shut up you white bitch
Creative Commons BY

Sur Framabook.org

Atelier Drupal 7
« Atelier Drupal 7 » par Cyprien ROUDET.
Option Libre
« Option Libre. Du bon usage des licences libres » par Benjamin Jean.

Tous nos Framabooks