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.
Olivier Gasquet, François Schwarzentruber, Martin Strecker. Panda:
a Proof Assistant in Natural Deduction for All. A Gentzen style proof
assistant for undergraduate students} (regular paper). Dans : Third International Congress on Tools for Teaching Logic, Salamanca (Spain), 01/06/2011-04/06/2011, Springer,, 2011.
BibTeX
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...
