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.
Edsger W. Dijkstra (1989):
On an exercise of Tony Hoare's.
Circulated privately, http://www.cs.utexas.edu/users/EWD/ewd10xx/EWD1062.PDF.
John Harrison (2009):
Handbook of Practical Logic and Automated Reasoning.
Cambridge University Press,
doi:10.1017/CBO9780511576430.
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.
Leslie Lamport (1993):
How to write a proof.
Global Analysis in Modern Mathematics,
pp. 311–321.
Also published in American Mathematical Monthly, 102(7):600-608, August-September 1995.
Leslie Lamport (2012):
How to write a 21st century proof.
Journal of fixed point theory and applications 11(1),
pp. 43–63,
doi:10.1007/s11784-012-0071-6.
Tobias Nipkow, Lawrence C. Paulson & Markus Wenzel (2002):
Isabelle/HOL - A Proof Assistant for Higher-Order Logic.
Lecture Notes in Computer Science 2283.
Springer,
doi:10.1007/3-540-45949-9.
Jørgen Villadsen, Andreas Halkjær From & Anders Schlichtkrull (2017):
Natural Deduction and the Isabelle Proof Assistant.
In: Pedro Quaresma & Walther Neuper: Proceedings 6th International Workshop on Theorem proving components for Educational Software (ThEdu),
EPTCS 267,
pp. 140–155,
doi:10.4204/EPTCS.267.9.
Jørgen Villadsen, Anders Schlichtkrull & Andreas Halkjær From (2018):
A Verified Simple Prover for First-Order Logic.
In: Boris Konev, Josef Urban & Philipp Rümmer: 6th Workshop on Practical Aspects of Automated Reasoning (PAAR),
CEUR Workshop Proceedings 2162,
Aachen,
pp. 88–104.
Available at http://ceur-ws.org/Vol-2162/#paper-08.
eptcs@eptcs.org