@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},
)