Panda: A Proof Assistant in Natural Deduction for All. A Gentzen Style Proof Assistant for Undergraduate Students

We present a proof assistant in Natural Deduction 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.
 

Online Copy

Conference version: PDF

BibTeX Entry

@inproceedings{gasquet11:_panda,
  author    = {Olivier Gasquet and
               Fran\c{c}ois Schwarzentruber and
               Martin Strecker},
  title     = {Panda: A Proof Assistant in Natural Deduction for All. A
               Gentzen Style Proof Assistant for Undergraduate Students},
  booktitle = {Tools for Teaching Logic - Third International Congress,
               TICTTL 2011, Salamanca, Spain, June 1-4, 2011. Proceedings},
  year      = 2011,
  pages     = {85-92},
  doi        = {http://dx.doi.org/10.1007/978-3-642-21350-2_11},
  publisher = {Springer},
  series    = {Lecture Notes in Computer Science},
  volume    = 6680
}