References

  1. Johan van Benthem (2010): Modal logic for open minds. CSLI Press, Stanford.
  2. Stefan Berghofer (2007): First-Order Logic According to Fitting. Archive of Formal Proofs. http://isa-afp.org/entries/FOL-Fitting.html, Formal proof development.
  3. Yves Bertot & Pierre Castéran (2013): Interactive theorem proving and program development: CoqArt: the calculus of inductive constructions. Springer.
  4. Patrick Blackburn & Johan Bos (2005): Representation and inference for natural language: A first course in computational semantics. CSLI Press, Stanford.
  5. 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.
  6. Alonzo Church (1956): Introduction to Mathematical Logic. Princeton University Press.
  7. Marcello D'Agostino, Dov M Gabbay, Reiner Hähnle & Joachim Posegga (2013): Handbook of tableau methods. Springer Science & Business Media, doi:10.1007/978-94-017-1754-0.
  8. The Agda Developers (2020): The Agda Wiki. https://wiki.portal.chalmers.se/agda/pmwiki.php.
  9. Asta Halkj\IeCæ r From, Alexander Birch Jensen, Anders Schlichtkrull & J\IeCø rgen Villadsen (2020): Teaching a Formalized Logical Calculus. In: Pedro Quaresma, Walther Neuper & João Marcos: Proceedings of the 8th International Workshop on Theorem proving components for Educational software (ThEdu), EPTCS 313, pp. 73–92, doi:10.4204/EPTCS.313.5.
  10. Peter Gärdenfors (2003): Belief Revision. Cambridge University Press.
  11. 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.
  12. Alexander Birch Jensen, Anders Schlichtkrull & J\IeCø rgen Villadsen (2017): First-Order Logic According to Harrison. Archive of Formal Proofs. http://isa-afp.org/entries/FOL_Harrison.html, Formal proof development.
  13. Imre Lakatos (1976): Proofs and refutations: The logic of mathematical discovery. Cambridge University Press, doi:10.1017/CBO9781139171472.
  14. Joe Leslie-Hurd & Guy Haworth (2013): Computer Theorem Proving and HoTT. ICGA Journal 36(2), pp. 100–103, doi:10.3233/ICG-2013-36204.
  15. Tobias Nipkow (2012): Teaching Semantics with a Proof Assistant: No More LSD Trip Proofs. In: Viktor Kuncak & Andrey Rybalchenko: Verification, Model Checking, and Abstract Interpretation. Springer, pp. 24–38, doi:10.1007/978-3-642-27940-9_3.
  16. Tobias Nipkow, Lawrence C. Paulson & Markus Wenzel (2002): Isabelle/HOL — A Proof Assistant for Higher-Order Logic. LNCS 2283. Springer, doi:10.1007/3-540-45949-9.
  17. Lawrence C Paulson, Tobias Nipkow & Makarius Wenzel (2019): From LCF to Isabelle/HOL. Formal Aspects of Computing 31(6), pp. 675–698, doi:10.1007/s00165-019-00492-1.
  18. Pierre-Marie Pédrot (2020): The Coq Proof Assistant, version 8.11.0 (The Coq Development Team). Zenodo, doi:10.5281/zenodo.3744225.
  19. Raymond M Smullyan (1995): First-order logic. Dover Publications.
  20. 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.
  21. J\IeCø rgen Villadsen (2015): ProofJudge: Automated Proof Judging Tool for Learning Mathematical Logic. In: Proceedings of the Exploring Teaching for Active Learning in Engineering Education Conference, Copenhagen, Denmark, pp. 39–44.
  22. J\IeCø rgen Villadsen, Andreas Halkj\IeCæ r From & Anders Schlichtkrull (2018): Natural Deduction and the Isabelle Proof Assistant. In: Proceedings of the 6th International Workshop on Theorem proving components for Educational software (ThEdu), EPTCS 267, pp. 140–155, doi:10.4204/EPTCS.267.9.
  23. J\IeCø rgen Villadsen, Alexander Birch Jensen & Anders Schlichtkrull (2017): NaDeA: A Natural Deduction Assistant with a Formalization in Isabelle. IFCoLog Journal of Logics and their Applications 4(1), pp. 55–82.
  24. Philip Wadler, Wen Kokke & Jeremy G. Siek (2020): Programming Language Foundations in Agda. Available at https://plfa.github.io/.
  25. Makarius Wenzel (2020): The Isabelle/Isar Reference Manual. Available at https://isabelle.in.tum.de/doc/isar-ref.pdf.

Comments and questions to: eptcs@eptcs.org
For website issues: webmaster@eptcs.org