Panda
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.
- Logique des prédicats ;
- Déduction naturelle sur Wikipédia
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 .
- Mineure : un lien mort, des fautes d'orthographe, un lien à ajouter ou encore une petite précision.
- Majeure : une nouvelle version avec des nouveautés, des changements majeurs.
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 !
Autres logiciels
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.
Autres rubriques
Libre : agenda
- Nantes: Atelier de contribution à Wikipédia, On Wednesday 30 January 2019 from 18h30 to 21h30.
- Nantes: Atelier de contribution à Wikipédia, On Monday 30 January 2017 from 18h30 to 21h30.
- Nantes: Atelier de contribution à Wikipédia, On Wednesday 21 December 2016 from 18h30 to 21h30.
- Nantes: Atelier de contribution à Wikipédia, On Monday 5 December 2016 from 18h30 to 21h30.
- Nantes: Atelier de contribution à Wikipédia, On Saturday 19 November 2016 from 18h30 to 21h30.
Informations générales
Sur le Framablog
Sur Framagora
- Disque externe hfs en lecture seule
- Problème de couleur
- Changer la langue d'un clavier sous xubuntu
- LibreOfficePortable : décimales
- au sujet de mon netbook gdium
- framabag certificat SSL revoqué
- rendre vierge ma clé
- Soumettre une notice pour un logiciel dont on est l'auteur
- Blender - Projet Gooseberry
- Bonjour
Juste une image
- Fly 1-PW
- Creative Commons BY-SA