@book(BenAri2001,
 author       = {Ben{-}Ari, Mordechai},
 year         = {2012},
 title        = {Mathematical Logic for Computer Science},
 publisher    = {Springer},
 doi          = {10.1007/978-1-4471-4129-7},
)
@inproceedings(Breitner16,
 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 - 7th International Conference, {ITP} 2016, Nancy, France, August 22-25, 2016, Proceedings},
 series       = {Lecture Notes in Computer Science},
 volume       = {9807},
 publisher    = {Springer},
 pages        = {123--139},
 doi          = {10.1007/978-3-319-43144-4\_8},
)
@article(Incredible-Proof-Machine-AFP,
 author       = {Joachim Breitner and Denis Lohner},
 year         = {2016},
 title        = {The meta theory of the Incredible Proof Machine},
 journal      = {Archive of Formal Proofs},
 note         = {\url{https://isa-afp.org/entries/Incredible_Proof_Machine.html}, Formal proof development},
)
@inproceedings(Axolotl19,
 author       = {David M. Cerna and Rafael P. D. Kiesel and Alexandra Dzhiganskaya},
 year         = {2019},
 title        = {A Mobile Application for Self-Guided Study of Formal Reasoning},
 editor       = {Pedro Quaresma and Walther Neuper and Jo{\~{a}}o Marcos},
 booktitle    = {Proceedings 8th International Workshop on Theorem Proving Components for Educational Software, ThEdu@CADE 2019, Natal, Brazil, 25th August 2019},
 series       = {{EPTCS}},
 volume       = {313},
 pages        = {35--53},
 doi          = {10.4204/EPTCS.313.3},
)
@inproceedings(CernaSSWB20,
 author       = {David M. Cerna and Martina Seidl and Wolfgang Schreiner and Wolfgang Windsteiger and Armin Biere},
 year         = {2020},
 title        = {Aiding an Introduction to Formal Reasoning Within a First-Year Logic Course for {CS} Majors Using a Mobile Self-Study App},
 editor       = {Michail N. Giannakos and Guttorm Sindre and Luxton{-}Reilly, Andrew and Monica Divitini},
 booktitle    = {Proceedings of the 2020 {ACM} Conference on Innovation and Technology in Computer Science Education, ITiCSE 2020, Trondheim, Norway, June 15-19, 2020},
 publisher    = {{ACM}},
 pages        = {61--67},
 doi          = {10.1145/3341525.3387409},
)
@inproceedings(SCT17,
 author       = {Arno Ehle and Norbert Hundeshagen and Martin Lange},
 year         = {2017},
 title        = {The Sequent Calculus Trainer with Automated Reasoning - Helping Students to Find Proofs},
 editor       = {Pedro Quaresma and Walther Neuper},
 booktitle    = {Proceedings 6th International Workshop on Theorem proving components for Educational software, ThEdu@CADE 2017, Gothenburg, Sweden, 6 August 2017},
 series       = {{EPTCS}},
 volume       = {267},
 pages        = {19--37},
 doi          = {10.4204/EPTCS.267.2},
)
@inproceedings(ThEdu19,
 author       = {Asta Halkj{\ae}r From and Alexander Birch Jensen and Anders Schlichtkrull and J{\o}rgen Villadsen},
 year         = {2019},
 title        = {Teaching a Formalized Logical Calculus},
 editor       = {Pedro Quaresma and Walther Neuper and Jo{\~{a}}o Marcos},
 booktitle    = {Proceedings 8th International Workshop on Theorem Proving Components for Educational Software, ThEdu@CADE 2019, Natal, Brazil, 25th August 2019},
 series       = {{EPTCS}},
 volume       = {313},
 pages        = {73--92},
 doi          = {10.4204/EPTCS.313.5},
)
@inproceedings(ThEdu20,
 author       = {Asta Halkj{\ae}r From and J{\o}rgen Villadsen and Patrick Blackburn},
 year         = {2020},
 title        = {Isabelle/{HOL} as a Meta-Language for Teaching Logic},
 editor       = {Pedro Quaresma and Walther Neuper and Jo{\~{a}}o Marcos},
 booktitle    = {Proceedings 9th International Workshop on Theorem Proving Components for Educational Software, ThEdu@IJCAR 2020, Paris, France, 29th June 2020},
 series       = {{EPTCS}},
 volume       = {328},
 pages        = {18--34},
 doi          = {10.4204/EPTCS.328.2},
)
@article(FOL-Seq-Calc1-AFP,
 author       = {Asta Halkj\IeC{\ae}r From},
 year         = {2019},
 title        = {A Sequent Calculus for First-Order Logic},
 journal      = {Archive of Formal Proofs},
 note         = {\url{https://isa-afp.org/entries/FOL_Seq_Calc1.html}, Formal proof development},
)
@inproceedings(CILC,
 author       = {Asta Halkj\IeC{\ae}r From and Anders Schlichtkrull and J\IeC{\o}rgen Villadsen},
 year         = {2021},
 title        = {A Sequent Calculus for First-Order Logic Formalized in Isabelle/{HOL}},
 editor       = {Stefania Monica and Federico Bergenti},
 booktitle    = {Proceedings of the 36th Italian Conference on Computational Logic - {CILC} 2021, Parma, Italy, September 7-9, 2021},
 series       = {{CEUR} Workshop Proceedings},
 volume       = {3002},
 publisher    = {CEUR-WS.org},
 pages        = {107--121},
 url          = {http://ceur-ws.org/Vol-3002/paper7.pdf},
)
@inproceedings(Carnap17,
 author       = {Leach{-}Krouse, Graham},
 year         = {2017},
 title        = {Carnap: An Open Framework for Formal Reasoning in the Browser},
 editor       = {Pedro Quaresma and Walther Neuper},
 booktitle    = {Proceedings 6th International Workshop on Theorem proving components for Educational software, ThEdu@CADE 2017, Gothenburg, Sweden, 6 August 2017},
 series       = {{EPTCS}},
 volume       = {267},
 pages        = {70--88},
 doi          = {10.4204/EPTCS.267.5},
)
@inproceedings(MichaelisN2017,
 author       = {Julius Michaelis and Tobias Nipkow},
 year         = {2018},
 title        = {Formalized Proof Systems for Propositional Logic},
 editor       = {A. Abel and F. Nordvall Forsberg and A. Kaposi},
 booktitle    = {23rd International Conference on Types for Proofs and Programs (TYPES 2017)},
 series       = {LIPIcs},
 volume       = {104},
 publisher    = {Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik},
 pages        = {6:1--6:16},
 doi          = {10.4230/LIPIcs.TYPES.2017.5},
)
@inproceedings(Nipkow12,
 author       = {Tobias Nipkow},
 year         = {2012},
 title        = {Teaching Semantics with a Proof Assistant: No More {LSD} Trip Proofs},
 editor       = {Viktor Kuncak and Andrey Rybalchenko},
 booktitle    = {Verification, Model Checking, and Abstract Interpretation},
 publisher    = {Springer},
 pages        = {24--38},
 doi          = {10.1007/978-3-642-27940-9_3},
)
@inproceedings(ReisNH20,
 author       = {Giselle Reis and Zan Naeem and Mohammed Hashim},
 year         = {2020},
 title        = {Sequoia: {A} Playground for Logicians - (System Description)},
 editor       = {Nicolas Peltier and Sofronie{-}Stokkermans, Viorica},
 booktitle    = {Automated Reasoning - 10th International Joint Conference, {IJCAR} 2020, Paris, France, July 1-4, 2020, Proceedings, Part {II}},
 series       = {Lecture Notes in Computer Science},
 volume       = {12167},
 publisher    = {Springer},
 pages        = {480--488},
 doi          = {10.1007/978-3-030-51054-1_32},
)
@inproceedings(SPA18,
 author       = {Anders Schlichtkrull and J{\o}rgen Villadsen and Andreas Halkj{\ae}r From},
 year         = {2018},
 title        = {{Students' Proof Assistant (SPA)}},
 editor       = {Pedro Quaresma and Walther Neuper},
 booktitle    = {Proceedings 7th International Workshop on Theorem proving components for Educational software, ThEdu@FLoC 2018, Oxford, United Kingdom, 18 July 2018},
 series       = {{EPTCS}},
 volume       = {290},
 pages        = {1--13},
 doi          = {10.4204/EPTCS.290.1},
)
@book(Smullyan1995,
 author       = {Raymond M. Smullyan},
 year         = {1995},
 title        = {First-Order Logic},
 publisher    = {Dover Publications},
)
@inproceedings(Villadsen20,
 author       = {J{\o}rgen Villadsen},
 year         = {2020},
 title        = {{Tautology Checkers in Isabelle and Haskell}},
 editor       = {Francesco Calimeri and Simona Perri and Ester Zumpano},
 booktitle    = {Proceedings of the 35th Italian Conference on Computational Logic - {CILC} 2020, Rende, Italy, October 13-15, 2020},
 series       = {{CEUR} Workshop Proceedings},
 volume       = {2710},
 publisher    = {CEUR-WS.org},
 pages        = {327--341},
 url          = {http://ceur-ws.org/Vol-2710/paper21.pdf},
)
@inproceedings(NaDeA18,
 author       = {J{\o}rgen Villadsen and Andreas Halkj{\ae}r From and Anders Schlichtkrull},
 year         = {2018},
 title        = {{Natural Deduction Assistant (NaDeA)}},
 editor       = {Pedro Quaresma and Walther Neuper},
 booktitle    = {Proceedings 7th International Workshop on Theorem proving components for Educational software, ThEdu@FLoC 2018, Oxford, United Kingdom, 18 July 2018},
 series       = {{EPTCS}},
 volume       = {290},
 pages        = {14--29},
 doi          = {10.4204/EPTCS.290.2},
)
@inproceedings(FMTea,
 author       = {J\IeC{\o}rgen Villadsen and Frederik Krogsdal Jacobsen},
 year         = {2021},
 title        = {Using Isabelle in Two Courses on Logic and Automated Reasoning},
 editor       = {Jo\IeC{\~a}o F. Ferreira and Alexandra Mendes and Claudio Menghi},
 booktitle    = {Formal Methods Teaching},
 publisher    = {Springer International Publishing},
 address      = {Cham},
 pages        = {117--132},
 doi          = {10.1007/978-3-030-91550-6_9},
)
@article(Wenzel2007,
 author       = {Makarius Wenzel},
 year         = {2007},
 title        = {Isabelle/{I}sar - a generic framework for human-readable proof documents},
 journal      = {From Insight to Proof - Festschrift in Honour of Andrzej Trybulec, Studies in Logic, Grammar, and Rhetoric. University of Bia\IeC{\l}ystok},
 volume       = {10},
 number       = {23},
 pages        = {277--298},
)