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