References

  1. Stefan Berghofer (2007): First-Order Logic According to Fitting. Archive of Formal Proofs. http://isa-afp.org/entries/FOL-Fitting.shtml, Formal proof development.
  2. Jasmin Christian Blanchette (2019): Formalizing the Metatheory of Logical Calculi and Automatic Provers in Isabelle/HOL (Invited Talk). In: Proceedings of the 8th ACM SIGPLAN International Conference on Certified Programs and Proofs (CPP), pp. 1–13, doi:10.1145/3293880.3294087.
  3. Jasmin Christian Blanchette & Andrei Popescu (2013): Mechanizing the Metatheory of Sledgehammer. In: Frontiers of Combining Systems - 9th International Symposium, FroCoS 2013, Nancy, France, September 18-20, 2013. Proceedings, pp. 245–260, doi:10.1007/978-3-642-40885-4_17.
  4. Jasmin Christian Blanchette, Andrei Popescu & Dmitriy Traytel (2017): Soundness and Completeness Proofs by Coinductive Methods. Journal of Automated Reasoning 58(1), pp. 149–179, doi:10.1007/s10817-016-9391-3.
  5. Patrick Braselmann & Peter Koepke (2005): Gödel's Completeness Theorem. Formalized Mathematics 13(1), pp. 49–53.
  6. Patrick Braselmann & Peter Koepke (2005): A Sequent Calculus for First-Order Logic. Formalized Mathematics 13(1), pp. 33–39.
  7. Hugo Herbelin, Sun Young Kim & Gyesik Lee (2017): Formalizing the meta-theory of first-order predicate logic. Journal of the Korean Mathematical Society 54(5), pp. 1521–1536, doi:10.4134/JKMS.j160546.
  8. Danko Ilik (2010): Constructive Completeness Proofs and Delimited Control. École Polytechnique. https://tel.archives-ouvertes.fr/tel-00529021/document.
  9. Danko Ilik, Gyesik Lee & Hugo Herbelin (2010): Kripke models for classical logic. Annals of Pure and Applied Logic 161(11), pp. 1367–1378, doi:10.1016/j.apal.2010.04.007.
  10. 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.
  11. James Margetson & Tom Ridge (2004): Completeness theorem. Archive of Formal Proofs. http://isa-afp.org/entries/Completeness.html, Formal proof development.
  12. Lawrence C. Paulson (2013): Gödel's Incompleteness Theorems. Archive of Formal Proofs. http://isa-afp.org/entries/Incompleteness.html, Formal proof development.
  13. Nicolas Peltier (2016): A Variant of the Superposition Calculus. Archive of Formal Proofs. http://isa-afp.org/entries/SuperCalc.shtml, Formal proof development.
  14. Henrik Persson (1996): Constructive completeness of intuitionistic predicate logic. Chalmers University of Technology. http://web.archive.org/web/20001011101511/http://www.cs.chalmers.se/~henrikp/Lic/.
  15. Christophe Raffalli (2005, possibly earlier): Krivine's abstract completeness proof for classical predicate logic. https://github.com/craff/phox/blob/master/examples/complete.phx.
  16. Tom Ridge (2004): A Mechanically Verified, Efficient, Sound and Complete Theorem Prover For First Order Logic. Archive of Formal Proofs. http://isa-afp.org/entries/Verified-Prover.shtml, Formal proof development.
  17. Tom Ridge & James Margetson (2005): A Mechanically Verified, Sound and Complete Theorem Prover for First Order Logic. In: Theorem Proving in Higher Order Logics, 18th International Conference, TPHOLs 2005, Oxford, UK, August 22-25, 2005, Proceedings, pp. 294–309, doi:10.1007/11541868_19.
  18. Anders Schlichtkrull (2018): Formalization of the Resolution Calculus for First-Order Logic. Journal of Automated Reasoning 61(1), pp. 455–484, doi:10.1007/s10817-017-9447-z.
  19. Anders Schlichtkrull, Jasmin Christian Blanchette, Dmitriy Traytel & Uwe Waldmann (2018): Formalizing Bachmair and Ganzinger's Ordered Resolution Prover. In: Didier Galmiche, Stephan Schulz & Roberto Sebastiani: Automated Reasoning. Springer, pp. 89–107, doi:10.1007/978-3-319-94205-6_7.
  20. Anders Schlichtkrull, Jørgen Villadsen & Andreas Halkjær From (2019): Students' Proof Assistant (SPA). In: Pedro Quaresma & Walther Neuper: Proceedings 7th International Workshop on Theorem proving components for Educational Software (ThEdu), EPTCS 290, pp. 1–13, doi:10.4204/EPTCS.290.1.
  21. Julian J. Schlöder & Peter Koepke (2012): The Gödel completeness theorem for uncountable languages. Formalized Mathematics 20(3), pp. 199–203, doi:10.2478/v10037-012-0023-z.
  22. Jørgen Villadsen, Andreas Halkjær From, Alexander Birch Jensen & Anders Schlichtkrull: NaDeA: A Natural Deduction Assistant with a Formalization in Isabelle. https://nadea.compute.dtu.dk.
  23. Jørgen Villadsen, Andreas Halkjær From & Anders Schlichtkrull (2019): Natural Deduction Assistant (NaDeA). In: Pedro Quaresma & Walther Neuper: Proceedings 7th International Workshop on Theorem proving components for Educational Software (ThEdu), EPTCS 290, pp. 14–29, doi:10.4204/EPTCS.290.2.
  24. Jørgen Villadsen, Anders Schlichtkrull & Andreas Halkjær From (2018): A Verified Simple Prover for First-Order Logic. In: Boris Konev, Josef Urban & Philipp Rümmer: 6th Workshop on Practical Aspects of Automated Reasoning (PAAR), CEUR Workshop Proceedings 2162, Aachen, pp. 88–104. Available at http://ceur-ws.org/Vol-2162/.
  25. Markus Wenzel (1999): Isar - A Generic Interpretative Approach to Readable Formal Proof Documents. In: Theorem Proving in Higher Order Logics, 12th International Conference, TPHOLs'99, Nice, France, September, 1999, Proceedings, pp. 167–184, doi:10.1007/3-540-48256-3_12.
Comments and questions to: eptcs@eptcs.org
For website issues: webmaster@eptcs.org