@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},
)
@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},
)
@inproceedings(blanchettepopescu,
 author       = {Jasmin Christian Blanchette and Andrei Popescu},
 year         = {2013},
 title        = {Mechanizing the Metatheory of Sledgehammer},
 booktitle    = {Frontiers of Combining Systems - 9th International Symposium, FroCoS 2013, Nancy, France, September 18-20, 2013. Proceedings},
 pages        = {245--260},
 doi          = {10.1007/978-3-642-40885-4_17},
)
@article(blanchettepopescutraytel,
 author       = {Jasmin Christian Blanchette and Andrei Popescu and Dmitriy Traytel},
 year         = {2017},
 title        = {Soundness and Completeness Proofs by Coinductive Methods},
 journal      = {Journal of Automated Reasoning},
 volume       = {58},
 number       = {1},
 pages        = {149--179},
 doi          = {10.1007/s10817-016-9391-3},
)
@article(braselmanncomplete,
 author       = {Patrick Braselmann and Peter Koepke},
 year         = {2005},
 title        = {{G{\"o}del}'s Completeness Theorem},
 journal      = {Formalized Mathematics},
 volume       = {13},
 number       = {1},
 pages        = {49--53},
)
@article(braselmanncalc,
 author       = {Patrick Braselmann and Peter Koepke},
 year         = {2005},
 title        = {A Sequent Calculus for First-Order Logic},
 journal      = {Formalized Mathematics},
 volume       = {13},
 number       = {1},
 pages        = {33--39},
)
@article(herbelinkimlee,
 author       = {Hugo Herbelin and Sun Young Kim and Gyesik Lee},
 year         = {2017},
 title        = {Formalizing the meta-theory of first-order predicate logic},
 journal      = {Journal of the Korean Mathematical Society},
 volume       = {54},
 number       = {5},
 pages        = {1521--1536},
 doi          = {10.4134/JKMS.j160546},
)
@phdthesis(ilik,
 author       = {Danko Ilik},
 year         = {2010},
 title        = {Constructive Completeness Proofs and Delimited Control},
 school       = {{\'E}cole Polytechnique},
 note         = {\url{https://tel.archives-ouvertes.fr/tel-00529021/document}},
)
@article(ilikleeherbelin,
 author       = {Danko Ilik and Gyesik Lee and Hugo Herbelin},
 year         = {2010},
 title        = {Kripke models for classical logic},
 journal      = {Annals of Pure and Applied Logic},
 volume       = {161},
 number       = {11},
 pages        = {1367--1378},
 doi          = {10.1016/j.apal.2010.04.007},
)
@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(Completeness-AFP,
 author       = {James Margetson and Tom Ridge},
 year         = {2004},
 title        = {Completeness theorem},
 journal      = {Archive of Formal Proofs},
 note         = {\url{http://isa-afp.org/entries/Completeness.html}, Formal proof development},
)
@article(Incompleteness-AFP,
 author       = {Lawrence C. Paulson},
 year         = {2013},
 title        = {G{\"o}del's Incompleteness Theorems},
 journal      = {Archive of Formal Proofs},
 note         = {\url{http://isa-afp.org/entries/Incompleteness.html}, Formal proof development},
)
@article(peltier,
 author       = {Nicolas Peltier},
 year         = {2016},
 title        = {A Variant of the Superposition Calculus},
 journal      = {Archive of Formal Proofs},
 note         = {\url{http://isa-afp.org/entries/SuperCalc.shtml}, Formal proof development},
)
@phdthesis(persson,
 author       = {Henrik Persson},
 year         = {1996},
 title        = {Constructive completeness of intuitionistic predicate logic},
 school       = {Chalmers University of Technology},
 note         = {\url{http://web.archive.org/web/20001011101511/http://www.cs.chalmers.se/~henrikp/Lic/}},
)
@misc(raffalli,
 author       = {Christophe Raffalli},
 year         = {2005, possibly earlier},
 title        = {{Krivine's} abstract completeness proof for classical predicate logic},
 howpublished = {\url{https://github.com/craff/phox/blob/master/examples/complete.phx}},
)
@article(ridge,
 author       = {Tom Ridge},
 year         = {2004},
 title        = {A Mechanically Verified, Efficient, Sound and Complete Theorem Prover For First Order Logic},
 journal      = {Archive of Formal Proofs},
 note         = {\url{http://isa-afp.org/entries/Verified-Prover.shtml}, Formal proof development},
)
@inproceedings(Ridge05,
 author       = {Tom Ridge and James Margetson},
 year         = {2005},
 title        = {A Mechanically Verified, Sound and Complete Theorem Prover for First Order Logic},
 booktitle    = {Theorem Proving in Higher Order Logics, 18th International Conference, TPHOLs 2005, Oxford, UK, August 22-25, 2005, Proceedings},
 pages        = {294--309},
 doi          = {10.1007/11541868_19},
)
@article(schlichtkrull,
 author       = {Anders Schlichtkrull},
 year         = {2018},
 title        = {Formalization of the Resolution Calculus for First-Order Logic},
 journal      = {Journal of Automated Reasoning},
 volume       = {61},
 number       = {1},
 pages        = {455--484},
 doi          = {10.1007/s10817-017-9447-z},
)
@inproceedings(schlichtkrullblanchettetraytelwaldmann,
 author       = {Anders Schlichtkrull and Jasmin Christian Blanchette and Dmitriy Traytel and Uwe Waldmann},
 year         = {2018},
 title        = {Formalizing {Bachmair} and {Ganzinger's} Ordered Resolution Prover},
 editor       = {Didier Galmiche and Stephan Schulz and Roberto Sebastiani},
 booktitle    = {Automated Reasoning},
 publisher    = {Springer},
 pages        = {89--107},
 doi          = {10.1007/978-3-319-94205-6_7},
)
@inproceedings(spa19,
 author       = {Anders Schlichtkrull and J{\o}rgen Villadsen and Andreas Halkj{\ae}r From},
 year         = {2019},
 title        = {{Students' Proof Assistant (SPA)}},
 editor       = {Pedro Quaresma and Walther Neuper},
 booktitle    = {Proceedings 7th International Workshop on Theorem proving components for Educational Software (ThEdu)},
 series       = {{EPTCS}},
 volume       = {290},
 pages        = {1--13},
 doi          = {10.4204/EPTCS.290.1},
)
@article(schloder,
 author       = {Julian J. Schl{\"o}der and Peter Koepke},
 year         = {2012},
 title        = {The {G{\"o}del} completeness theorem for uncountable languages},
 journal      = {Formalized Mathematics},
 volume       = {20},
 number       = {3},
 pages        = {199--203},
 doi          = {10.2478/v10037-012-0023-z},
)
@misc(nadea,
 author       = {J\o{}rgen Villadsen and Andreas Halkj{\ae}r From and Alexander Birch Jensen and Anders Schlichtkrull},
 title        = {{NaDeA}: A Natural Deduction Assistant with a Formalization in {Isabelle}},
 howpublished = {\url{https://nadea.compute.dtu.dk}},
)
@inproceedings(nadea19,
 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(VilladsenEtAl:PAAR2018,
 author       = {J\o{}rgen Villadsen and Anders Schlichtkrull and Andreas Halkj\ae{}r From},
 year         = {2018},
 title        = {A Verified Simple Prover for First-Order Logic},
 editor       = {Boris Konev and Josef Urban and Philipp R\"ummer},
 booktitle    = {6th Workshop on Practical Aspects of Automated Reasoning (PAAR)},
 series       = {CEUR Workshop Proceedings},
 volume       = {2162},
 address      = {Aachen},
 pages        = {88--104},
 url          = {http://ceur-ws.org/Vol-2162/},
)
@inproceedings(wenzel99,
 author       = {Markus Wenzel},
 year         = {1999},
 title        = {Isar - {A} Generic Interpretative Approach to Readable Formal Proof Documents},
 booktitle    = {Theorem Proving in Higher Order Logics, 12th International Conference, TPHOLs'99, Nice, France, September, 1999, Proceedings},
 pages        = {167--184},
 doi          = {10.1007/3-540-48256-3_12},
)