1. ProofWeb. (ProofWeb is both a system for teaching logic and for using proof assistants through the web).. Available at Accessed December 2017.
  2. Stefan Berghofer (2007): First-Order Logic According to Fitting. Archive of Formal Proofs., Formal proof development.
  3. Jasmin Christian Blanchette, Andrei Popescu & Dmitriy Traytel (2014): Unified Classical Logic Completeness - A Coinductive Pearl. Lecture Notes in Computer Science 8562. Springer, pp. 46–60, doi:10.1007/978-3-319-08587-6_4.
  4. Joachim Breitner (2016): Visual Theorem Proving with the Incredible Proof Machine. In: Interactive Theorem Proving - 7th International Conference, ITP 2016, Nancy, France, August 22-25, 2016, Proceedings, pp. 123–139, doi:10.1007/978-3-319-43144-4_8.
  5. Joachim Breitner & Denis Lohner (2016): The meta theory of the Incredible Proof Machine. Archive of Formal Proofs., Formal proof development.
  6. Krysia Broda, Jiefei Ma, Gabrielle Sinnadurai & Alexander J. Summers (2007): Pandora: A Reasoning Toolbox using Natural Deduction Style. Logic Journal of the IGPL 15(4), pp. 293–304, doi:10.1093/jigpal/jzm020.
  7. Martin Elsman (2011): SMLtoJs: Hosting a Standard ML Compiler in a Web Browser. In: Proceedings of the 1st ACM SIGPLAN International Workshop on Programming Language and Systems Technologies for Internet Clients, PLASTIC '11. ACM, New York, NY, USA, pp. 39–48, doi:10.1145/2093328.2093336.
  8. Melvin Fitting (1996): First-Order Logic and Automated Theorem Proving, Second Edition. Graduate Texts in Computer Science. Springer, doi:10.1007/978-1-4612-2360-3.
  9. Andreas Halkjær From (2017): Formalized First-Order Logic. BSc Thesis, Technical University of Denmark.
  10. Olivier Gasquet, François Schwarzentruber & Martin Strecker (2011): Panda: A Proof Assistant in Natural Deduction for All. A Gentzen Style Proof Assistant for Undergraduate Students. Lecture Notes in Computer Science 6680. Springer, pp. 85–92, doi:10.1007/978-3-642-21350-2_11.
  11. John Harrison (1998): Formalizing Basic First Order Model Theory. In: Theorem Proving in Higher Order Logics, 11th International Conference, TPHOLs'98, Canberra, Australia, September 27 - October 1, 1998, Proceedings. Springer, pp. 153–170, doi:10.1007/BFb0055135.
  12. Michael Huth & Mark Ryan (2004): Logic in Computer Science: Modelling and Reasoning about Systems. Second Edition. Cambridge University Press, doi:10.1017/CBO9780511810275.
  13. Alexander Birch Jensen, Anders Schlichtkrull & Jørgen Villadsen (2017): First-Order Logic According to Harrison. Archive of Formal Proofs., Formal proof development.
  14. Ramana Kumar, Rob Arthan, Magnus O. Myreen & Scott Owens (2014): HOL with Definitions: Semantics, Soundness, and a Verified Implementation. Lecture Notes in Computer Science 8858. Springer, pp. 308–324, doi:10.1007/978-3-319-08970-6_20.
  15. Tobias Nipkow & Gerwin Klein (2014): Concrete Semantics - With Isabelle/HOL. Springer, doi:10.1007/978-3-319-10542-0.
  16. 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.
  17. Daejun Park, Andrei Stefănescu & Grigore Roşu (2015): KJS: A Complete Formal Semantics of JavaScript. In: Proceedings of the 36th ACM SIGPLAN Conference on Programming Language Design and Implementation, PLDI '15. ACM, New York, NY, USA, pp. 346–356, doi:10.1145/2737924.2737991.
  18. Jonathan P. Seldin (1989): Normalization and excluded middle. I. Studia Logica 48(2), pp. 193–217, doi:10.1007/BF02770512.
  19. 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.
  20. Makarius Wenzel (2017): The Isabelle/Isar Reference Manual.

Comments and questions to:
For website issues: