Panda : Proof Assistant for Natural Deduction for All

Run / Lancer le logiciel
Write proofs of propositional logic and first order logic in natural deduction
Give exercices to students
Sensibilize students to proof verification
Ecrire des preuves de logique propositionnelle et du premier ordre en déduction naturelle
Donner des exercices aux étudiants
Sensibiliser les étudiants à la vérification automatique de preuves

Panda est utilisée dans le cours d'introduction à la logique au niveau L2 à l'Université Paul Sabatier à Toulouse.

Help / Aide
Download the software / Télécharger le logiciel (dézipper panda.zip, aller dans le dossier dist, puis lancer le fichier panda.jar)
Download sources / Télécharger les sources (pour les connaisseurs, c'est un projet Netbeans)
Download slides of a presentation in Rennes / Télécharger les transparents de la présentation à Rennes






Clean graphical interface with LaTEX quality for rendering formulas...

You can deduce a formula by drawing a line...


You enter formulas though a graphical panel...



You can introduce a temporary hypothesis by clicking on "ghost" formulas on the top...


Buttons for applying rules quickly...