Resources on Logic Education

In this page, you can find a compilation of resources on logic education that are available on the internet. Some of the resources were previously compiled on other websites created with this purpose (e.g., tools-for-teaching-logic) and others were found on the web.

! If you would like to suggest a resource on logic education, send an email to logic-education.component319@passfwd.com and we would be happy to add it! Thank you for your contributions 🙂

A portion of these resources were compiled in Summer 2023 as an effort to provide a comprehensive list of the current state of educational logic resources available on the web.

The aim of this compilation is:

• to serve as a first place where students and academics can access and share resources.
• to be an interactive and collaborative space! 🙂
  • Anyone can suggest to add a new resource that they create or they find on the internet, and anyone can suggest to remove a link that has become deprecated over time.
  • We highly encourage you to do this by sending an email! logic-education.component319@passfwd.com

Each resource has the following characteristics listed in the first row of each table:

• URL of the resource.
• Resource type (website, solver, etc).
• About (a few sentences on the basic characteristics of the resource).
• External Software? (Is it necessary to download an external software?)
• Features (Main features of the resource)
• Author(s)
• Notes (e.g., is there a broken link, etc)

Click on these to access different kind of resources!

La Universidad de Salamanca has compiled logic resources in a new website! Summa Logicae, a digital library for students and researchers.

tools-for-teaching-logic

Logic software and logic education

URL	Type	About	Features	External Software?	Author(s)	Notes
Logic software and logic education HTML download website	HTML Website	Commenced in 1996. Last updated 23 May 2007. It currently has some broken links. Those which are not broken are listed below.	These pages contain a pretty comprehensive, alphabetically ordered: list of educational logic software as well as additional, very incomplete, information on that subject in the form of links to: the theorem proving community, other lists of educational logic software, logic education projects .	Yes	Maintained by Hans van Ditmarsch . Comments appreciated: hans@cs.otago.ac.nz
AproS	Online CourseProof Search		The broadened project has now three separate parts. (1) At its center is the automated proof search engine AProS. It provides the computational core for all our efforts to enhance logic learning and teaching through excellent technological support. (2) These efforts have resulted in the development of sophisticated, interactive Labs that are incorporated in web-based Courses featuring the LogicLab Software Suite, in particular, in the introductory course Logic & Proofs. (3) The novel logical calculus NIC (normal intercalation calculus) reflects informal bi-directional reasoning and allows the formulation of efficient strategies for proof search. These strategies are implemented in AProS which, in turn, is the logical backbone for the Dynamic Proof Tutor.	Yes	Project Director: Wilfried Sieg, Research Staff: Dawn McLaughlin, Michael Ringenberg, Research Collaborators: Joseph Ramsey, Research Associates (current): Patrick Walsh, Paulo Santos	The new AProS Application will soon be available! Stay tuned for the first release version in Fall 2023!
Athena Programming Language (Old version with exercises: Athena)	Programming LanguageProver	Athena is a programming language and an interactive theorem proving environment rolled in one. (1) As a programming language, Athena is a higher-order functional language in the tradition of Scheme and ML: strict and lexically scoped. (2) As a theorem proving system, Athena is based on many-sorted first-order logic.	Combining expressivity and simplicity. True natural-deduction style. Conditional and Equational Rewriting. Built-in Proof Automation. Proof Reuse and Custom Tactics. Flexible Module System. Extensible notation. Abstract-level proofs and structured theories	NoYes	Created by Konstantine Arkoudas, and Mantained by AthenaFoundation	New version has in-website playground but can also download. There are three available courses for learning Athena. The material for these courses consists of thoughtfully curated excerpts from the Athena book. There is User’s Guide for old version.
Linear Logic Prover	Prover	This small program searches a cut-free proof of the given two-sided sequent of first-order linear logic.	The proof search of linear logic is undecidable. Therefore, this program limits the number of contraction rules for each path of the proof at most three (this threshold value can be changed).	Yes	Naoyuki Tamura	There are further links in the website for resources. Some of these are likely broken. Also, more on linear logic: http://www.lcc.uma.es/~lopez/linear.html Site includes user’s guide
Sequent Prover	Prover	This small program seqprover.pl (written in Prolog) searches a cut-free proof of the given sequent of first-order logic.		Yes	Naoyuki Tamura	Please refer to guide.pdf for notations and inference rules.
An Introduction to Teaching Logic as a Tool	Website	Contains links to different resources both educational and for teaching.		No	David Gries and Fred B. Schneider
Summa Logicae (Spanish & English)	Website	Digital library, a reference book for logic students and researchers alike, specially Spanish speakers, overtly involved in innovation and paedagogical systematization. We also include software, a selection of links and a glossary. There is a page in the site under the heading working groups, specifically devised for students.	Fundamentals. This heading unifies a series of basic content and the fundamentals of our discipline, alternatively it could have been called “Mathematical Logic”, o simply, “Logic”. Under this category we find the following sub-branches: Elementary Logic, Proof Theory, Model Theory, Computational Theory and Set Theory. Logical Systems. The greater part of our research activity involves devising logical systems of diverse nature. Traditionally they have been called non-classical logics, many of them were extensions of classical logic. We have decided to call them simply “logical systems”. Those materials, headings and subheadings displayed in this branch are so numerous that our only alternative was to resort to an open list which shall grow with time. Applications. Under this heading we have included all possible applications of logic, or logical systems, in different fields, such as: Computer Science, Linguistics, Economics or Science. Studies on Logic. Under this heading you will find a great variety of external studies which have logic as their main subject: History of Logic, Bibliography, Philosophy of Logic and Paedagogy of Logic.	NoYes	María Manzano, et al.	User Guides (in Spanish) under:: Library :: Applications :: Comentario Software
Taller de Didáctica de la Lógica (Spanish)	Website	Historical website from Academia Mexicana de Lógica	It contains links to various websites with variety of resources, some of which are broken	No	Academia Mexicana de Lógica	Will try out the links to discover more educational logic resources.
Theorem Proving System (TPS) and the Educational Theorem Proving System (ETPS)	Prover	The Theorem Proving System (TPS) is an automated theorem-prover for first-order logic and type theory. The Educational Theorem Proving System (ETPS) is a cut-down version of TPS intended for use by students; it contains only commands relevant to proving theorems interactively	Potential applications of automated theorem proving include hardware and software verification, partial automation of various mathematical activities, promoting development of formal theories in a wide variety of disciplines, deductive information systems for these disciplines, expert systems which can reason, and certain aspects of artificial intelligence.	Yes	[Peter Andrews] [Matthew Bishop] [Chad E. Brown] [Rémy Chrétien] [Eve Cohen] [Sunil Issar] [Dan Nesmith] [Frank Pfenning] [Hongwei Xi]	TPS and ETPS run in Common Lisp, and can be used on any system where Common Lisp runs. TPS and ETPS have been used extensively under Unix and Linux systems, and to some extent under Windows.
Tree Proof Generator	Prover	Enter a formula of standard propositional, predicate, or modal logic. The page will try to find either a countermodel or a tree proof (a.k.a. semantic tableau).		No	Wolfgang Schwarz	User guide is given in the webpage with syntax and instructions on how to use the tool.
Mechanized Reasoning	Website	Variety of links related to Automated Reasoning	This page contains the following items: • What is Automated Reasoning, • Existing systems, related fields/pages, archives, … • Research groups and projects, • Discussion forums, • Journals, • Organizations, • An annotated reading list	No	Michael Kohlhase and Carolyn Talcott.	[Last updated 2 September 1996.] This page is still under construction, so it is by no means complete. For better service to the Mechanized Reasoning community we will need your help. Please contribute!. Send links, material to fill in blanks, suggestions, encouragement, or donations by clicking here.
Introduction to Logic	Website	This website provides, through a range of materials and tools, an introduction to the study of elementary logic covering propositional and predicate calculus. It is hoped that the site may be useful more widely, for anyone who would like to investigate the subject. The material here is intended to be used in conjunction with Wilfrid Hodges’ Logic. This text was used for the Introduction to Logic course until 2008, when Hodges’ text was replaced with the Logic Manual as set text.		No	The Logic Web project has been directed by Hugh Rice at the Faculty of Philosophy.This site has been developed by the Academic Computing Development TeamInitial development and design carried out by Martin Rhys Jones..Acknowledgements	These webpages are no longer maintained and appear here as an unsupported resource only.
Tableau3	Website	Tableau3 has been written in Java and in order to run properly has two main requirements: a program that can interpret the Java program (called a Java Runtime Environment) and the ability to display mathematical symbols through the provision of appropriate fonts.	The instructions on this Help Page are designed to provide assistance in getting Tableau3 to work in a selection of environments.	Yes	Tableau3 has been developed by Nik Roberts	The Tableau3 program has been written in Java and requires some configuration in order to get it working properly.
Power of Logic	Website	The Power of Logic Web Tutor is a free tutorial to accompany the sixth edition of The Power of Logic by Frances Howard-Snyder, Daniel Howard-Snyder, and Ryan Wasserman.	This internet-based study guide provides you with numerous ways to check your understanding of logic and to independently check your work and receive feedback.	No	Website produced by Logic Pedallersfor McGraw-Hill   © 2012 – 2023
DN-FN	Educational Program	Program to learn Natural Deduction in Gentzen-Kleene’s style	The disk contains two programs, DN and FN, intended to provide some help in teaching Natural Deduction (in Gentzen’s style) and Normal Forms calculation. They are written in Pascal for PC computers. The primitive idea was to have at disposal a true and intelligent deriver, being able to calculate and provide (on a printer) fair copies for exercises carried out for a long time at the University of Nantes.	Yes	Patrice Bailhache, Université de Nantes
Logic-Toolbox	Educational Program	Categorical Logic (Seems to not be working properly), Propositional Logic, Formal Proofs		No	Update:4/9/13Please send questions, feedback, suggestions, and bug reports to:john.saetti@gmail.comCopyright ©2007 by John Saetti – ALL RIGHTS RESERVEDLast update: 6-1-18	This material is provided with the hope that it may be useful to students- but WITHOUT ANY WARRANTY – even an implied warranty of its fitness for a particular purpose.
The Logic Machine	BookEducational Program	The Logic Machine, originally developed and hosted at Texas A&M University, provides interactive logic software used for teaching introductory formal logic. The Daemon Proof Checker checks proofs and can provide hints for students attempting to construct proofs in a natural deduction system for sentential (propositional) and first-order predicate (quantifier) logic. The Quizmaster provides a variety of exercises, from questions about basic concepts such as validity, to wff construction and translation, to proofs, truth tables, and countermodels. The system and exercises are based on Logic Primer (MIT Press, 2000) but the exercises are also suitable for use with other texts, such as E.J. Lemmon’s Beginning Logic.		Yes	Colin Allen and Chris Menzel ©2006-2022
Jape	Proof Calculator	Jape is a configurable proof calculator and supports the interactive discovery of formal proofs in inference systems. It is distributed with a number of example logic encodings: in particular a natural deduction, several sequent calculi, a treatment of Burroughs-Abadi-Newman protocols, a Hindley-Milner typing mechanism, and various others including even Aristotlean syllogisms.	A manual (Roll your own Jape logic) is available for those who would like to experiment with their own encodings. Get releases via  the release page, and please report problems via the issues page.	Yes	Richard Bornat

University of Michigan Library – Philosophy – Logic Resources

URL	Type	About	Features	External Software?	Author(s)	Notes
University of Michigan Library – Philosophy – Logic Resources	Collection of ResourcesWebsite	Selected resources useful for philosophical research.	Online Logic Resources, Logic Blogs, Online Courses for Logic	No	University of Michigan
Blogic	Book	This book explores the deep structure of thought and language. It will not teach you how to think or how to speak, but it will teach you how to think and speak about thinking and speaking — how to analyze and discuss them in terms of universal principles by which they are governed. These principles play an especially important role in reasoning — the reasoning that we do in our heads, when we think, and the reasoning that we do aloud when we argue for a conclusion.		No	David Velleman
Latex-for-logicians	ArticleWebsite	These pages give a brief guide to resources of interest to logicians, philosophers and others using LaTeX to produce papers or presentations, teaching materials, theses or books, and perhaps wanting to include logical matter such as natural deduction proofs.		No	Peter Smith. Contact: peter_smith AT me DOT com
Logic in argumentative writing	ArticleWebsite	This handout is designed to help writers develop and use logical arguments in writing. This handout helps writers analyze the arguments of others and generate their own arguments.		No	Purdue University
The Many Worlds of Logic	QuizzesSlidesVideosWebsite	This website accompanies and supplements the standard logic class taught at most colleges and universities.	The videos, slides, lectures, and quizzes on this website are keyed to Introduction to Logic by Paul Herrick (Oxford University Press, 2012).	No	Paul Herrick, Shoreline Comm College
Puzzle Baron’s logic puzzles	Puzzles	Website with more than 25,000 unique puzzles available for play, both online and the old fashioned way – with pencil and paper	Feel free to solve online just for fun, or, for an added challenge, register a free account and compete against thousands of other solvers to make it into our Logic Puzzle Hall of Fame!	No	Puzzle Baron
Teach Yourself Logic	BookStudy Guide	A re-titled, expanded version of the old Teach Yourself Logic study guide. This is a book length guide to suitable texts either for teaching yourself logic by individual self-study, or to supplement a university course. You only need to read just the first half-dozen pages to see if this is for you!	The same reviews in the Appendix can also be found as separate webpages in linked to this page of Book Notes, which also links to comments/reviews about some forty(!) more books on logic and the philosophy of mathematics. These range from half-pages to (in one case) a 52 page essay. Most are a useful two or three pages!	No	Peter Smith. Contact: peter_smith AT me DOT com

Logic and Philosophy resources online

URL	Type	About	Features	External Software?	Author(s)	Notes
Logic in Action	BookWebsite	Open course in logic. This project was developed to provide a modern introduction to the field of logic with topics reflecting both its mathematical essentials and a broad view of its interdisciplinary role.	A pdf version of the textbook can be downloaded from here. There are also slides for teaching available, in English and in Spanish (made by Fernando Velazquez Quesada). Further exercise material for the chapters (courtesy of Dora Achourioti, AUC) can be found here. Online exercises in modal logic (an important topic in the course) can be found here.	No	Johan van Benthem, Hans van Ditmarsch, Jan van Eijck, Jan Jaspars
Logicomix	Comic	Covering a span of sixty years, the graphic novel Logicomix was inspired by the epic story of the quest for the Foundations of Mathematics.	This was a heroic intellectual adventure most of whose protagonists paid the price of knowledge with extreme personal suffering and even insanity. The book tells its tale in an engaging way, at the same time complex and accessible. It grounds the philosophical struggles on the undercurrent of personal emotional turmoil, as well as the momentous historical events and ideological battles which gave rise to them.	No	The Team
Logic in the 19th century, especially that of George Boole	BookWebsite	Link with book notes, slides, talks, lecture presentations centered on logic and logic in the 19th century, especially that of George Boole		No	Stanley N. Burris, Distinguished Professor Emeritus and Adjunct Professor, Department of Pure Mathematics, University of Waterloo, E-mail: snburris@math.uwaterloo.ca
SimcirJS	Circuit Simulator	SimcirJS(a.k.a. Simcir) is a circuit simulator in HTML5 and JavaScript.		NoYes	Kazuhiko Arase
Openproof Courseware: Tools for Learning Logic	BookOnline Course	The Openproof project at Stanford’s Center for the Study of Language and Information (CSLI) is concerned with the application of software to problems in logic. Since the early 1980’s we have been developing applications in logic education which are both innovative and effective. The development of these courseware packages has in turn informed and influenced our research agenda.	[REQUIRED TO BUY COURSES] Courses: Logical Reasoning with Diagrams and Sentences. Language, Proof and Logic. and	Yes	CSLI, Standford University
Mathigon	Educational Program	The Mathematical Playground: Free tools, courses and manipulatives to make online learning more interactive and engaging than ever before.		No	Team Mathigon
Beginning Mathematical Logic: A Study Guide	Book			No	Peter Smith. Contact: peter_smith AT me DOT com
Introduction to Logic course	Online Course			No	Coursera
Mathematical Thinking course	Online Course			No	Coursera
Book Of Proof by Richard Hammack	Book			No	Richard Hammack
Symbolic Logic by Lewis Carroll	Book			No	Lewis Carroll
Student Cognition Toolbox for Statistics	Online Course	The Student Cognition Toolbox (SCT) is a short course companion (or “sidecar”) introducing and providing direct practice in study strategies that are informed by learning science research. In this version of the SCT, material from introductory statistics is used to illustrate the application of the study strategies. This version gives examples and recommendations specifically for students studying Introductory Statistics.		No	Carnegie Mellon University	Open & Free Version Same as above
Logicmatters.net	BookWebsite		THE BIG RED LOGIC BOOKS The headline news. (New book, Aug 2023!) LOGIC MATTERS BLOG Peter Smith’s occasional blog posts on logic, music, and other enthusiasms. Most recent posts: ‘Category Theory I, the paperback!’ (Aug 5); ‘Schubert on Sunday 2: Eric Lu plays D959’ (Aug 6); ‘Mileti, Modern Mathematical Logic, Chs 11–12’ (Aug 7). INTRO TO FORMAL LOGIC. A corrected version of the second edition of An Introduction to Formal Logic is freely available here. There are also links to answers to exercises and to various supplementary materials. GÖDEL’S THEOREMS. Two books are freely available here, An Introduction to Gödel’s Theorems and the much shorter Gödel Without (Too Many) Tears, along with related materials. CATEGORY THEORY Links to resources at an introductory/intermediate level, including lecture notes and freely available books, and my evolving Category Theory: Notes Towards a Gentle Introduction. TEACH YOURSELF LOGIC You will find here the much-downloaded Beginning Mathematical Logic: A Study Guide as well as other resources (including Book Notes reviewing many texts) ARCHIVE Links to various old blog posts, papers, book reviews and other pieces. Also links to snippets from over a hundred notes on logic for (more or less) beginners. Plus my old advice for grad students on writing papers! LaTeX FOR LOGICIANS Pages pointing to a wide range of resources of interest to logicians, philosophers and others using LaTeX.	No	Peter Smith. Contact: peter_smith AT me DOT com
Logic.ly	Educational Program	[Buy or Free Online Demo] The digital logic simulator. Logic.ly simulates logic circuits and assists students in learning digital electronics. Keep students engaged with a simple and friendly UI that encourages experimentation and discovery.	• Design circuits quickly and easily with a modern and intuitive user interface with drag-and-drop, copy/paste, zoom & more. • Take control of debugging by pausing the simulation and watching the signal propagate as you advance step-by-step. • Don’t worry about multiple platforms on student computers. Install on both Windows and macOS.	Yes	Copyright 2008-2023 Bowler Hat LLC. All rights reserved.	News & Updates: • Logic.ly Blog, • Follow Logic.ly on Twitter
An Introduction to Computer Science	Online Course	I call this site many things, a textbook, a study guide, the course website. Its goal is to present the material is a comprehensive written way.		No	Charlie Stuart, Drexel University’s College of Computing and Informatics
Logic & Proofs	Online Course	An introductory logic course, designed for students from a broad range of disciplines, from mathematics and computer science to drama and creative writing. It is also designed to reflect aspects of the logical tradition (going back to Aristotle) as well as the practical applicability (for example for the construction of Boolean circuits). Below one finds a detailed description of the course with many of its special features.	Logic & Proofs is a rigorous introduction to modern symbolic logic that covers both sentential and predicate logic (including identity). The crucial skills of recognizing the (in-)correctness of arguments are honed by working in the LogicLab: in derivation or proof problems, students learn to construct complex arguments in a strategically guided way; in truth table and truth-tree problems, the emphasis is on systematically finding counterexamples.	No	Carnegie Mellon University	Open & Free Version Same as above
Causal and Statistical Reasoning	Online Course	An introduction to causal and statistical reasoning, this course is meant for students interested in critical thinking skills for daily life, students who will take a few statistics courses in service of a related field of study, and/or students interested in the foundations of quantitative causal models: called Bayes Networks.	Topics Covered: Causation, association and independence, causation to association, association to causation: problems, association to causation: strategies	No	Carnegie Mellon University	Open & Free Version This Open & Free Course provides you with access to an online course comparable to a full semester course on Causal and Statistical Reasoning taught at Carnegie Mellon University. Your access includes the complete online course including all expository text, simulations, case studies, comprehension tests, computer tutors, and the Causality Lab. At Carnegie Mellon, this online course is taught in combination with instructor-led discussion sections. The Open & Free Causal and Statistical Reasoning course does NOT include access to the end-of-module graded exams or to the course instructor. No credit is awarded for completing the Open & Free Causal and Statistical Reasoning course.