ProofWeb. (ProofWeb is both a system for teaching logic and for using proof assistants through the web)..
Available at http://proofweb.cs.ru.nl/login.php.
Accessed December 2017.
Stefan Berghofer (2007):
First-Order Logic According to Fitting.
Archive of Formal Proofs.
http://isa-afp.org/entries/FOL-Fitting.html, Formal proof development.
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.
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.
Joachim Breitner & Denis Lohner (2016):
The meta theory of the Incredible Proof Machine.
Archive of Formal Proofs.
http://isa-afp.org/entries/Incredible_Proof_Machine.html, Formal proof development.
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.
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.
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.
Andreas Halkjær From (2017):
Formalized First-Order Logic.
BSc Thesis, Technical University of Denmark.
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.
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.
Michael Huth & Mark Ryan (2004):
Logic in Computer Science: Modelling and Reasoning about Systems. Second Edition.
Cambridge University Press,
doi:10.1017/CBO9780511810275.
Alexander Birch Jensen, Anders Schlichtkrull & Jørgen Villadsen (2017):
First-Order Logic According to Harrison.
Archive of Formal Proofs.
http://isa-afp.org/entries/FOL_Harrison.html, Formal proof development.
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.
Tobias Nipkow & Gerwin Klein (2014):
Concrete Semantics - With Isabelle/HOL.
Springer,
doi:10.1007/978-3-319-10542-0.
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.
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.
Jonathan P. Seldin (1989):
Normalization and excluded middle. I.
Studia Logica 48(2),
pp. 193–217,
doi:10.1007/BF02770512.
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.
Makarius Wenzel (2017):
The Isabelle/Isar Reference Manual.
http://isabelle.in.tum.de/dist/doc/isar-ref.pdf.
eptcs@eptcs.org