@book(van2010modal,
 author       = {Johan van Benthem},
 year         = {2010},
 title        = {Modal logic for open minds},
 publisher    = {CSLI Press, Stanford},
)
@article(FOL-Fitting-AFP,
 author       = {Stefan Berghofer},
 year         = {2007},
 title        = {{F}irst-{O}rder {L}ogic {A}ccording to {F}itting},
 journal      = {Archive of Formal Proofs},
 note         = {\url{http://isa-afp.org/entries/FOL-Fitting.html}, Formal proof development},
)
@book(bertot2013interactive,
 author       = {Yves Bertot and Pierre Cast{\'e}ran},
 year         = {2013},
 title        = {Interactive theorem proving and program development: Coq\IeC{\textquoteright}Art: the calculus of inductive constructions},
 publisher    = {Springer},
)
@book(blackburn2005representation,
 author       = {Patrick Blackburn and Johan Bos},
 year         = {2005},
 title        = {Representation and inference for natural language: A first course in computational semantics},
 publisher    = {CSLI Press, Stanford},
)
@inproceedings(IsaFoL,
 author       = {Jasmin Christian Blanchette},
 year         = {2019},
 title        = {Formalizing the Metatheory of Logical Calculi and Automatic Provers in {Isabelle/HOL} (Invited Talk)},
 booktitle    = {Proceedings of the 8th ACM SIGPLAN International Conference on Certified Programs and Proofs (CPP)},
 pages        = {1--13},
 doi          = {10.1145/3293880.3294087},
)
@book(Church1956,
 author       = {Alonzo Church},
 year         = {1956},
 title        = {Introduction to Mathematical Logic},
 publisher    = {Princeton University Press},
)
@book(d2013handbook,
 author       = {Marcello D'Agostino and Dov M Gabbay and Reiner H{\"a}hnle and Joachim Posegga},
 year         = {2013},
 title        = {Handbook of tableau methods},
 publisher    = {Springer Science \& Business Media},
 doi          = {10.1007/978-94-017-1754-0},
)
@misc(agda,
 author       = {{A}gda {D}evelopers, The},
 year         = {2020},
 title        = {The {A}gda {W}iki},
 note         = {\url{https://wiki.portal.chalmers.se/agda/pmwiki.php}},
)
@inproceedings(secav19,
 author       = {Asta Halkj\IeC{\ae}r From and Alexander Birch Jensen and Anders Schlichtkrull and J\IeC{\o}rgen Villadsen},
 year         = {2020},
 title        = {{T}eaching a {F}ormalized {L}ogical {C}alculus},
 editor       = {Pedro Quaresma and Walther Neuper and Jo\~ao Marcos},
 booktitle    = {Proceedings of the 8th International Workshop on Theorem proving components for Educational software (ThEdu)},
 series       = {{EPTCS}},
 volume       = {313},
 pages        = {73--92},
 doi          = {10.4204/EPTCS.313.5},
)
@book(gardenfors2003belief,
 editor       = {Peter G{\"a}rdenfors},
 year         = {2003},
 title        = {Belief Revision},
 publisher    = {Cambridge University Press},
)
@article(jensen,
 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(FOL-Harrison-AFP,
 author       = {Alexander Birch Jensen and Anders Schlichtkrull and J\IeC{\o}rgen Villadsen},
 year         = {2017},
 title        = {{F}irst-{O}rder {L}ogic {A}ccording to {H}arrison},
 journal      = {Archive of Formal Proofs},
 note         = {\url{http://isa-afp.org/entries/FOL_Harrison.html}, Formal proof development},
)
@book(lakatos2015proofs,
 author       = {Imre Lakatos},
 year         = {1976},
 title        = {Proofs and refutations: The logic of mathematical discovery},
 publisher    = {Cambridge University Press},
 doi          = {10.1017/CBO9781139171472},
)
@article(leslie2013computer,
 author       = {Leslie-Hurd, Joe and Guy Haworth},
 year         = {2013},
 title        = {Computer Theorem Proving and {HoTT}},
 journal      = {ICGA Journal},
 volume       = {36},
 number       = {2},
 pages        = {100--103},
 doi          = {10.3233/ICG-2013-36204},
)
@inproceedings(Nipkow12,
 author       = {Tobias Nipkow},
 year         = {2012},
 title        = {Teaching Semantics with a Proof Assistant: No More {LSD} Trip Proofs},
 editor       = {Viktor Kuncak and Andrey Rybalchenko},
 booktitle    = {Verification, Model Checking, and Abstract Interpretation},
 publisher    = {Springer},
 pages        = {24--38},
 doi          = {10.1007/978-3-642-27940-9_3},
)
@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       = {LNCS},
 volume       = {2283},
 publisher    = {Springer},
 doi          = {10.1007/3-540-45949-9},
)
@article(paulson2019lcf,
 author       = {Lawrence C Paulson and Tobias Nipkow and Makarius Wenzel},
 year         = {2019},
 title        = {From LCF to Isabelle/HOL},
 journal      = {Formal Aspects of Computing},
 volume       = {31},
 number       = {6},
 pages        = {675--698},
 doi          = {10.1007/s00165-019-00492-1},
)
@book(coq811,
 editor       = {P\IeC{\'e}drot, Pierre-Marie},
 year         = {2020},
 title        = {The {C}oq {P}roof {A}ssistant, version 8.11.0 (The Coq Development Team)},
 publisher    = {Zenodo},
 doi          = {10.5281/zenodo.3744225},
)
@book(smullyan1995first,
 author       = {Raymond M Smullyan},
 year         = {1995},
 title        = {First-order logic},
 publisher    = {Dover Publications},
)
@inproceedings(nadea18,
 author       = {J{\o}rgen Villadsen and Andreas Halkj{\ae}r From and Anders Schlichtkrull},
 year         = {2019},
 title        = {{Natural Deduction Assistant (NaDeA)}},
 editor       = {Pedro Quaresma and Walther Neuper},
 booktitle    = {Proceedings 7th International Workshop on Theorem proving components for Educational Software (ThEdu)},
 series       = {{EPTCS}},
 volume       = {290},
 pages        = {14--29},
 doi          = {10.4204/EPTCS.290.2},
)
@inproceedings(proofjudge,
 author       = {J\IeC{\o}rgen Villadsen},
 year         = {2015},
 title        = {{P}roof{J}udge: {A}utomated {P}roof {J}udging {T}ool for {L}earning {M}athematical {L}ogic},
 booktitle    = {Proceedings of the Exploring Teaching for Active Learning in Engineering Education Conference},
 address      = {Copenhagen, Denmark},
 pages        = {39--44},
)
@inproceedings(nadea17,
 author       = {J\IeC{\o}rgen Villadsen and Andreas Halkj\IeC{\ae}r From and Anders Schlichtkrull},
 year         = {2018},
 title        = {{N}atural {D}eduction and the {I}sabelle {P}roof {A}ssistant},
 booktitle    = {Proceedings of the 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\IeC{\o}rgen Villadsen and Alexander Birch Jensen and Anders Schlichtkrull},
 year         = {2017},
 title        = {{NaDeA}: {A} {N}atural {D}eduction {A}ssistant with a {F}ormalization in {I}sabelle},
 journal      = {IFCoLog Journal of Logics and their Applications},
 volume       = {4},
 number       = {1},
 pages        = {55--82},
)
@book(plfa2019,
 author       = {Philip Wadler and Wen Kokke and Jeremy G. Siek},
 year         = {2020},
 title        = {Programming Language Foundations in {A}gda},
 publisher    = {Available at \url{https://plfa.github.io/}},
)
@book(isar-ref,
 author       = {Makarius Wenzel},
 year         = {2020},
 title        = {The {I}sabelle/{I}sar Reference Manual},
 publisher    = {Available at \url{https://isabelle.in.tum.de/doc/isar-ref.pdf}},
)