Didaktický software a webové aplikace pro výuku dedukce:

PANDA

Francois SCHWARZENTRUBER
Universität Trier
www.irit.fr/panda



Abstrakt

Panda is a Proof Assistant for Natural Deduction for All, which has been designed for undergraduate students. The system is interactive: you can combine, delete, modify proofs with a easy-to-use graphical interface. We discuss the pedagogical benefit of this tool. The system allows to write proofs of propositional logic and first order logic in natural deduction; to give exercices to students and to sensibilize students to proof verification.˙Many courses of logic include an introduction to some proof systém often based on some variant of natural deduction among the following three main approaches (according to the thorough review of natural deduction systems of [5]): Fitchťs diagrams, Suppesťannotated proofs and Gentzenťs trees. Any of them of course could help students in gaining rigour in reasoning by the use of formal systems of deduction. ˙We want here to argue in favor of Gentzenťs tree. We believe that one reason of their less frequent use w.r.t. the other systems is purely technical: they are more difficult to typeset (and hence it is more difficult to implement a friendly interface for them) when compared with Fitchťs and Suppesťsytems. But it seems to us that Gentzenťs style proofs are more readable because the tree-like strukture od proofs (which is linked to their inductive construction) is more evident.

Prezentace

Článek ve sborníku