@article(berghofer,
 author       = {Stefan Berghofer},
 year         = {2007},
 title        = {First-Order Logic According to {Fitting}},
 journal      = {Archive of Formal Proofs},
 note         = {\url{http://isa-afp.org/entries/FOL-Fitting.shtml}, Formal proof development},
)
@book(church1956introduction,
 author       = {A. Church},
 year         = {1956},
 title        = {Introduction to Mathematical Logic},
 publisher    = {Princeton University Press},
)
@article(geuvers,
 author       = {H. Geuvers},
 year         = {2009},
 title        = {Proof Assistants: History, Ideas and Future},
 journal      = {Sadhana},
 volume       = {34},
 number       = {1},
 pages        = {3--25},
 doi          = {10.1007/s12046-009-0001-5},
)
@article(jensen2018,
 author       = {Alexander Birch Jensen and John Bruntse Larsen and Anders Schlichtkrull and J{\o}rgen Villadsen},
 year         = {2018},
 title        = {Programming and verifying a declarative first-order prover in {Isabelle/HOL}},
 journal      = {{AI} Communications},
 volume       = {31},
 number       = {3},
 pages        = {281--299},
 doi          = {10.3233/AIC-180764},
)
@article(PropositionalProofSystemsAFP,
 author       = {Julius Michaelis and Tobias Nipkow},
 year         = {2017},
 title        = {Propositional Proof Systems},
 journal      = {Archive of Formal Proofs},
 note         = {\url{http://isa-afp.org/entries/Propositional_Proof_Systems.shtml}, Formal proof development},
)
@book(nipkow+02,
 author       = {Tobias Nipkow and Lawrence C. Paulson and Markus Wenzel},
 year         = {2002},
 title        = {Isabelle/HOL - {A} Proof Assistant for Higher-Order Logic},
 series       = {Lecture Notes in Computer Science},
 volume       = {2283},
 publisher    = {Springer},
 doi          = {10.1007/3-540-45949-9},
)
@inproceedings(DBLP:journals/corr/abs-1803-01473,
 author       = {J{\o}rgen Villadsen and Andreas Halkj{\ae}r From and Anders Schlichtkrull},
 year         = {2017},
 title        = {Natural Deduction and the {I}sabelle Proof Assistant},
 editor       = {Pedro Quaresma and Walther Neuper},
 booktitle    = {Proceedings 6th International Workshop on Theorem proving components for Educational Software (ThEdu)},
 series       = {{EPTCS}},
 volume       = {267},
 pages        = {140--155},
 doi          = {10.4204/EPTCS.267.9},
)
@article(IfCoLog,
 author       = {J{\o}rgen Villadsen and Alexander Birch Jensen and Anders Schlichtkrull},
 year         = {2017},
 title        = {{NaDeA}: {A} Natural Deduction Assistant with a Formalization in Isabelle},
 journal      = {IFCoLog Journal of Logics and their Applications},
 volume       = {4},
 number       = {1},
 pages        = {55--82},
)