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é)

Aidez-nous à atteindre notre objectif de 1080 donateurs récurrents pour assurer notre pérennité et notre développement !

Je soutiens Framasoft
pour 10€/mois

Dégooglisons Internet, l’an 2

Les services en ligne de géants tentaculaires comme Google, Apple, Facebook, Amazon ou Microsoft (GAFAM) mettent en danger nos vies numériques.

Pour cette 2e année, nous continuons le défi de vous proposer une alternative Libre, Éthique, Décentralisée et Solidaire à chacun de ces services.

Découvrez notre campagne
« Dégooglisons Internet »

Informations générales

Juste une image

Fly 1-PW Fly 1-PW
Creative Commons BY-SA