Johan van Benthem (2010):
Modal logic for open minds.
CSLI Press, Stanford.
Stefan Berghofer (2007):
First-Order Logic According to Fitting.
Archive of Formal Proofs.
http://isa-afp.org/entries/FOL-Fitting.html, Formal proof development.
Yves Bertot & Pierre Castéran (2013):
Interactive theorem proving and program development: CoqArt: the calculus of inductive constructions.
Springer.
Patrick Blackburn & Johan Bos (2005):
Representation and inference for natural language: A first course in computational semantics.
CSLI Press, Stanford.
Jasmin Christian Blanchette (2019):
Formalizing the Metatheory of Logical Calculi and Automatic Provers in Isabelle/HOL (Invited Talk).
In: Proceedings of the 8th ACM SIGPLAN International Conference on Certified Programs and Proofs (CPP),
pp. 1–13,
doi:10.1145/3293880.3294087.
Alonzo Church (1956):
Introduction to Mathematical Logic.
Princeton University Press.
Marcello D'Agostino, Dov M Gabbay, Reiner Hähnle & Joachim Posegga (2013):
Handbook of tableau methods.
Springer Science & Business Media,
doi:10.1007/978-94-017-1754-0.
The Agda Developers (2020):
The Agda Wiki.
https://wiki.portal.chalmers.se/agda/pmwiki.php.
Asta Halkj\IeCæ r From, Alexander Birch Jensen, Anders Schlichtkrull & J\IeCø rgen Villadsen (2020):
Teaching a Formalized Logical Calculus.
In: Pedro Quaresma, Walther Neuper & João Marcos: Proceedings of the 8th International Workshop on Theorem proving components for Educational software (ThEdu),
EPTCS 313,
pp. 73–92,
doi:10.4204/EPTCS.313.5.
Peter Gärdenfors (2003):
Belief Revision.
Cambridge University Press.
Alexander Birch Jensen, John Bruntse Larsen, Anders Schlichtkrull & Jørgen Villadsen (2018):
Programming and verifying a declarative first-order prover in Isabelle/HOL.
AI Communications 31(3),
pp. 281–299,
doi:10.3233/AIC-180764.
Alexander Birch Jensen, Anders Schlichtkrull & J\IeCø rgen Villadsen (2017):
First-Order Logic According to Harrison.
Archive of Formal Proofs.
http://isa-afp.org/entries/FOL_Harrison.html, Formal proof development.
Imre Lakatos (1976):
Proofs and refutations: The logic of mathematical discovery.
Cambridge University Press,
doi:10.1017/CBO9781139171472.
Joe Leslie-Hurd & Guy Haworth (2013):
Computer Theorem Proving and HoTT.
ICGA Journal 36(2),
pp. 100–103,
doi:10.3233/ICG-2013-36204.
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.
Tobias Nipkow, Lawrence C. Paulson & Markus Wenzel (2002):
Isabelle/HOL — A Proof Assistant for Higher-Order Logic.
LNCS 2283.
Springer,
doi:10.1007/3-540-45949-9.
Lawrence C Paulson, Tobias Nipkow & Makarius Wenzel (2019):
From LCF to Isabelle/HOL.
Formal Aspects of Computing 31(6),
pp. 675–698,
doi:10.1007/s00165-019-00492-1.
Pierre-Marie Pédrot (2020):
The Coq Proof Assistant, version 8.11.0 (The Coq Development Team).
Zenodo,
doi:10.5281/zenodo.3744225.
Raymond M Smullyan (1995):
First-order logic.
Dover Publications.
Jørgen Villadsen, Andreas Halkjær From & Anders Schlichtkrull (2019):
Natural Deduction Assistant (NaDeA).
In: Pedro Quaresma & Walther Neuper: Proceedings 7th International Workshop on Theorem proving components for Educational Software (ThEdu),
EPTCS 290,
pp. 14–29,
doi:10.4204/EPTCS.290.2.
J\IeCø rgen Villadsen (2015):
ProofJudge: Automated Proof Judging Tool for Learning Mathematical Logic.
In: Proceedings of the Exploring Teaching for Active Learning in Engineering Education Conference,
Copenhagen, Denmark,
pp. 39–44.
J\IeCø rgen Villadsen, Andreas Halkj\IeCæ r From & Anders Schlichtkrull (2018):
Natural Deduction and the Isabelle Proof Assistant.
In: Proceedings of the 6th International Workshop on Theorem proving components for Educational software (ThEdu),
EPTCS 267,
pp. 140–155,
doi:10.4204/EPTCS.267.9.
J\IeCø rgen Villadsen, Alexander Birch Jensen & Anders Schlichtkrull (2017):
NaDeA: A Natural Deduction Assistant with a Formalization in Isabelle.
IFCoLog Journal of Logics and their Applications 4(1),
pp. 55–82.
Philip Wadler, Wen Kokke & Jeremy G. Siek (2020):
Programming Language Foundations in Agda.
Available at https://plfa.github.io/.
Makarius Wenzel (2020):
The Isabelle/Isar Reference Manual.
Available at https://isabelle.in.tum.de/doc/isar-ref.pdf.