Stefan Berghofer (2007):
First-Order Logic According to Fitting.
Archive of Formal Proofs.
http://isa-afp.org/entries/FOL-Fitting.shtml, Formal proof development.
A. Church (1956):
Introduction to Mathematical Logic.
Princeton University Press.
H. Geuvers (2009):
Proof Assistants: History, Ideas and Future.
Sadhana 34(1),
pp. 3–25,
doi:10.1007/s12046-009-0001-5.
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.
Julius Michaelis & Tobias Nipkow (2017):
Propositional Proof Systems.
Archive of Formal Proofs.
http://isa-afp.org/entries/Propositional_Proof_Systems.shtml, Formal proof development.
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, 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.
eptcs@eptcs.org