@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},
)