@book(wffn1966,
 author       = {Layman E. Allen},
 year         = {1966},
 title        = {WFF 'N PROOF : the game of modern logic},
 publisher    = {Autotelic Instructional Materials Publishers},
)
@book(Baader:1998:TR:280474,
 author       = {Franz Baader and Tobias Nipkow},
 year         = {1998},
 title        = {Term Rewriting and All That},
 publisher    = {Cambridge University Press},
 address      = {New York, NY, USA},
 doi          = {10.1017/CBO9781139172752},
)
@book(DBLP:books/daglib/0032840,
 author       = {Hendrik Pieter Barendregt and Wil Dekkers and Richard Statman},
 year         = {2013},
 title        = {Lambda Calculus with Types},
 series       = {Perspectives in logic},
 publisher    = {Cambridge University Press},
 doi          = {10.1017/CBO9781139032636},
 url          = {http://www.cambridge.org/de/academic/subjects/mathematics/logic-categories-and-sets/lambda-calculus-types},
)
@proceedings(DBLP:conf/ticttl/2011,
 editor       = {Patrick Blackburn and Hans van Ditmarsch and Mar{\'{\i}}a Manzano and Soler{-}Toscano, Fernando},
 year         = {2011},
 title        = {Tools for Teaching Logic - Third International Congress, {TICTTL} 2011, Salamanca, Spain, June 1-4, 2011. Proceedings},
 series       = {Lecture Notes in Computer Science},
 volume       = {6680},
 publisher    = {Springer},
 doi          = {10.1007/978-3-642-21350-2},
)
@inproceedings(Breitner2016,
 author       = {Joachim Breitner},
 year         = {2016},
 title        = {Visual Theorem Proving with the Incredible Proof Machine},
 editor       = {Jasmin Christian Blanchette and Stephan Merz},
 booktitle    = {Interactive Theorem Proving},
 publisher    = {Springer International Publishing},
 address      = {Cham},
 pages        = {123--139},
 doi          = {10.1007/978-3-319-43144-4\_8},
)
@inproceedings(Pandora,
 author       = {K. Broda and J. Ma and G. Sinnadurai and A. Summers},
 year         = {2006},
 title        = {Friendly e-tutor for Natural Deduction},
 booktitle    = {BCS-FACS},
 series       = {Practice and Experience},
 doi          = {10.5555/2228206.2228208},
)
@article(JFR4568,
 author       = {Bruno Buchberger and Tudor Jebelean and Temur Kutsia and Alexander Maletzky and Wolfgang Windsteiger},
 year         = {2016},
 title        = {Theorema 2.0: Computer-Assisted Natural-Style Mathematics},
 journal      = {Journal of Formalized Reasoning},
 volume       = {9},
 number       = {1},
 pages        = {149--185},
 doi          = {10.6092/issn.1972-5787/4568},
 url          = {https://jfr.unibo.it/article/view/4568},
)
@inproceedings(Carter2014UsingTP,
 author       = {Nathan C. Carter and Kenneth G. Monks},
 year         = {2014},
 title        = {Using the Proof-Checking Word Processor Lurch to Teach Proof-Writing},
)
@techreport(Survey,
 author       = {David M. Cerna},
 year         = {2019},
 title        = {{Evaluation of the VL Logic (342.208-9) 2018W End of Semester Questionnaire}},
 type         = {RISC Report Series},
)
@unpublished(DanDC,
 author       = {Dan Christensen},
 year         = {2010},
 title        = {DC Proof},
 note         = {Need: Available at https://www.dcproof.com/},
)
@(COQ,
 author       = {Thierry Coquand and G\IeC{\'e}rard Huet.},
 year         = {2019},
 title        = {The Coq Proof Assistant},
 url          = {https://coq.inria.fr/},
)
@inbook(DAgostino1999,
 author       = {Marcello D'Agostino},
 year         = {1999},
 title        = {Tableau Methods for Classical Propositional Logic},
 pages        = {45--123},
 publisher    = {Springer Netherlands},
 address      = {Dordrecht},
 doi          = {10.1007/978-94-017-1754-0\_2},
)
@(spoon2018,
 author       = {Spoon Developers},
 year         = {2018},
 title        = {{QUANTIFIERS}! - A Mathematical Logic Game},
 url          = {https://play.google.com/store/apps/details?id=spoon.quantifiers},
)
@incollection(Dowek:2001:HUM:778522.778525,
 author       = {Gilles Dowek},
 year         = {2001},
 editor       = {Alan Robinson and Andrei Voronkov},
 booktitle    = {Handbook of Automated Reasoning},
 chapter      = {Higher-order Unification and Matching},
 publisher    = {Elsevier Science Publishers B. V.},
 address      = {Amsterdam, The Netherlands, The Netherlands},
 pages        = {1009--1062},
 doi          = {10.1016/B978-044450813-3/50018-7},
 url          = {http://dl.acm.org/citation.cfm?id=778522.778525},
)
@article(Silva2008,
 author       = {V. {D'Silva} and D. {Kroening} and G. {Weissenbacher}},
 year         = {2008},
 title        = {A Survey of Automated Techniques for Formal Software Verification},
 journal      = {IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems},
 volume       = {27},
 number       = {7},
 pages        = {1165--1178},
 doi          = {10.1109/TCAD.2008.923410},
)
@inproceedings(Ehle2017,
 author       = {Arno Ehle and Norbert Hundeshagen and Martin Lange},
 year         = {2017},
 title        = {The Sequent Calculus Trainer with Automated Reasoning - Helping Students to Find Proofs},
 booktitle    = {Proceedings 6th International Workshop on Theorem proving components for Educational software, ThEdu@CADE 2017, Gothenburg, Sweden, 6 Aug 2017.},
 pages        = {19--37},
 doi          = {10.4204/EPTCS.267.2},
)
@inproceedings(10.1007/978-3-642-21350-2,
 author       = {Olivier Gasquet and Fran{\c{c}}ois Schwarzentruber and Martin Strecker},
 year         = {2011},
 title        = {Panda: A Proof Assistant in Natural Deduction for All. A Gentzen Style Proof Assistant for Undergraduate Students},
 editor       = {Patrick Blackburn and Hans van Ditmarsch and Mar{\'i}a Manzano and Soler-Toscano, Fernando},
 booktitle    = {Tools for Teaching Logic},
 publisher    = {Springer Berlin Heidelberg},
 address      = {Berlin, Heidelberg},
 pages        = {85--92},
 doi          = {10.1093/jigpal/jzm026},
)
@book(Girard:1989:PT:64805,
 author       = {Jean-Yves Girard and Paul Taylor and Yves Lafont},
 year         = {1989},
 title        = {Proofs and Types},
 publisher    = {Cambridge University Press},
 address      = {New York, NY, USA},
)
@(Jukka2018,
 author       = {Jukka H\"{a}kkinen},
 year         = {2018},
 title        = {Natural Deduction. Proof generator. Proof checker.},
 url          = {http://naturaldeduction.org/},
)
@(Haustein2017,
 author       = {Stefan Haustein},
 year         = {2017},
 title        = {Emojic},
 url          = {https://play.google.com/store/apps/details?id=org.flowgrid.emojic},
 note         = {Repository location: https://github.com/stefanhaustein/EmojiC},
)
@inproceedings(Huertas:2011:TYC:2021573.2021589,
 author       = {Antonia Huertas},
 year         = {2011},
 title        = {Ten Years of Computer-based Tutors for Teaching Logic 2000-2010: Lessons Learned},
 booktitle    = {Proceedings of the Third International Congress Conference on Tools for Teaching Logic},
 series       = {TICTTL'11},
 publisher    = {Springer-Verlag},
 address      = {Berlin, Heidelberg},
 pages        = {131--140},
 doi          = {10.1093/jigpal/jzm019},
 url          = {http://dl.acm.org/citation.cfm?id=2021573.2021589},
)
@(Andor2018,
 author       = {Matthias Jenny},
 year         = {2018},
 title        = {Andor: Learn Logic},
 url          = {https://play.google.com/store/apps/details?id=io.cordova.andor},
)
@inproceedings(fFBK17,
 author       = {Maria Knobelsdorf and Christiane Frede and Sebastian B{\"{o}}hne and Christoph Kreitz},
 year         = {2017},
 title        = {Theorem Provers as a Learning Tool in Theory of Computation},
 booktitle    = {Proceedings of the 2017 {ACM} Conference on International Computing Education Research, {ICER} 2017, Tacoma, WA, USA, August 18-20, 2017},
 pages        = {83--92},
 doi          = {10.1145/3105726.3106184},
)
@inproceedings(Krouse2017,
 author       = {Leach{-}Krouse, Graham},
 year         = {2017},
 title        = {Carnap: An Open Framework for Formal Reasoning in the Browser},
 editor       = {Quaresma and Neuper},
 pages        = {70--88},
 doi          = {10.4204/EPTCS.267.5},
 url          = {http://arxiv.org/abs/1803.00722},
)
@book(Leitsch:1997:RC:260906,
 author       = {Alexander Leitsch},
 year         = {1997},
 title        = {The Resolution Calculus},
 publisher    = {Springer-Verlag},
 address      = {Berlin, Heidelberg},
 doi          = {10.1007/978-3-642-60605-2},
)
@article(Makowsky2017,
 author       = {J. A. Makowsky and A. Zamansky},
 year         = {2017},
 title        = {Keeping Logic in the Trivium of Computer Science: A Teaching Perspective},
 journal      = {Form. Methods Syst. Des.},
 volume       = {51},
 number       = {2},
 pages        = {419--430},
 doi          = {10.1007/s10703-017-0301-z},
)
@book(ScratchMarji,
 author       = {Majed Marji},
 year         = {2014},
 title        = {Learn to Program with Scratch: A Visual Introduction to Programming with Games, Art, Science, and Math},
 publisher    = {No Starch Press},
)
@book(Monk1976,
 author       = {J.D. Monk},
 year         = {1976},
 title        = {Mathematical Logic},
 series       = {Graduate Texts in Mathematics,},
 volume       = {37},
 doi          = {10.1007/978-1-4684-9452-5},
)
@inproceedings(moura2008,
 author       = {Leonardo de Moura and Bj{\o}rner, Nikolaj},
 year         = {2008},
 title        = {Z3: An Efficient SMT Solver},
 editor       = {C. R. Ramakrishnan and Jakob Rehof},
 booktitle    = {Tools and Algorithms for the Construction and Analysis of Systems},
 publisher    = {Springer Berlin Heidelberg},
 address      = {Berlin, Heidelberg},
 pages        = {337--340},
 doi          = {10.1109/MS.2006.117},
)
@book(Nipkow02,
 author       = {Tobias Nipkow and Lawrence C. Paulson and Markus Wenzel},
 year         = {2002},
 title        = {Isabelle/HOL - {A} Proof Assistant for Higher-Order Logic},
 series       = {Lecture Notes in Computer Science},
 volume       = {2283},
 publisher    = {Springer},
 doi          = {10.1007/3-540-45949-9},
)
@proceedings(DBLP:journals/corr/abs-1803-00722,
 editor       = {Pedro Quaresma and Walther Neuper},
 year         = {2018},
 title        = {Proceedings 6th International Workshop on Theorem proving components for Educational software, ThEdu@CADE 2017, Gothenburg, Sweden, 6 Aug 2017},
 series       = {{EPTCS}},
 volume       = {267},
 url          = {http://arxiv.org/abs/1803.00722},
)
@inproceedings(Schlichtkrull2018,
 author       = {Anders Schlichtkrull and J{\o}rgen Villadsen and Andreas Halkj{\ae}r From},
 year         = {2019},
 title        = {Students' Proof Assistant (SPA)},
 editor       = {Pedro Quaresma and Walther Neuper},
 booktitle    = {{\rm Proceedings 7th International Workshop on} Theorem proving components for Educational software, {\rm Oxford, United Kingdom, 18 july 2018}},
 series       = {Electronic Proceedings in Theoretical Computer Science},
 volume       = {290},
 publisher    = {Open Publishing Association},
 pages        = {1--13},
 doi          = {10.4204/EPTCS.290.1},
)
@inproceedings(DBLP:journals/corr/abs-1202-4834,
 author       = {Wolfgang Schreiner},
 year         = {2011},
 title        = {Computer-Assisted Program Reasoning Based on a Relational Semantics of Programs},
 booktitle    = {Proceedings First Workshop on {CTP} Components for Educational Software, THedu'11, Wroclaw, Poland, 31th July 2011.},
 pages        = {124--142},
 doi          = {10.4204/EPTCS.79.8},
)
@inproceedings(DBLP:journals/corr/abs-1904-00620,
 author       = {Wolfgang Schreiner},
 year         = {2018},
 title        = {Theorem and Algorithm Checking for Courses on Logic and Formal Methods},
 booktitle    = {Proceedings 7th International Workshop on Theorem proving components for Educational software, THedu@FLoC 2018, Oxford, United Kingdom, 18 july 2018.},
 pages        = {56--75},
 doi          = {10.4204/EPTCS.290.5},
)
@(Lewis2012,
 author       = {Terry Tao},
 year         = {2012},
 title        = {Lewis Carroll},
 url          = {https://scratch.mit.edu/projects/2486639/},
)
@(QED2018,
 author       = {Terry Tao},
 year         = {2018},
 title        = {QED},
 url          = {https://teorth.github.io/QED/},
)
@misc(Peanoware,
 author       = {Th\IeC{\'e}ry, Laurent},
 title        = {Peanoware-Natural Deduction},
 howpublished = {Google Play},
)
@inproceedings(Villadsen2018,
 author       = {J{\o}rgen Villadsen and Andreas Halkj{\ae}r From and Anders Schlichtkrull},
 year         = {2019},
 title        = {Natural Deduction Assistant (NaDeA)},
 editor       = {Pedro Quaresma and Walther Neuper},
 booktitle    = {{\rm Proceedings 7th International Workshop on} Theorem proving components for Educational software, {\rm Oxford, United Kingdom, 18 july 2018}},
 series       = {Electronic Proceedings in Theoretical Computer Science},
 volume       = {290},
 publisher    = {Open Publishing Association},
 pages        = {14--29},
 doi          = {10.4204/EPTCS.290.2},
)
@article(Visser2003,
 author       = {Willem Visser and Klaus Havelund and Guillaume Brat and SeungJoon Park and Flavio Lerda},
 year         = {2003},
 title        = {Model Checking Programs},
 journal      = {Automated Software Engineering},
 volume       = {10},
 number       = {2},
 pages        = {203--232},
 doi          = {10.1023/A:1022920129859},
)
@(logic2016,
 author       = {Yale Weiss},
 year         = {2016},
 title        = {LOGIC++},
 url          = {https://yaleweiss.commons.gc.cuny.edu/logic/},
)