1. Stefan Berghofer (2007): First-Order Logic According to Fitting. Archive of Formal Proofs., Formal proof development.
  2. A. Church (1956): Introduction to Mathematical Logic. Princeton University Press.
  3. H. Geuvers (2009): Proof Assistants: History, Ideas and Future. Sadhana 34(1), pp. 3–25, doi:10.1007/s12046-009-0001-5.
  4. 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.
  5. Julius Michaelis & Tobias Nipkow (2017): Propositional Proof Systems. Archive of Formal Proofs., Formal proof development.
  6. Tobias Nipkow, Lawrence C. Paulson & Markus Wenzel (2002): Isabelle/HOL - A Proof Assistant for Higher-Order Logic. Lecture Notes in Computer Science 2283. Springer, doi:10.1007/3-540-45949-9.
  7. Jørgen Villadsen, Andreas Halkjær From & Anders Schlichtkrull (2017): Natural Deduction and the Isabelle Proof Assistant. In: Pedro Quaresma & Walther Neuper: Proceedings 6th International Workshop on Theorem proving components for Educational Software (ThEdu), EPTCS 267, pp. 140–155, doi:10.4204/EPTCS.267.9.
  8. Jø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.

Comments and questions to:
For website issues: