Association of Symbolic Logic
Committee on Logic Education

Members:

• John Baldwin
• J. Karel Lambert
• Jeff Hirst
• Jean A. Larson
• Judith Roitman
• Daniel J. Velleman
• Richard Zach
• Past members include Cathy Kessel, Carl Posy , and Wilfried Sieg

ASL and the NCTM Standards

Computers in Logic Education

• Special Session at 2002 ASL Annual Meeting, June 1-4, Las Vegas, Nevada
• Previous meetings on Logic Education:
  • Computers and Philosophy sponsors meetings with info on computers in teaching philosophy
  • Teaching Logic and Reasoning in an Illogical World, DIMACS Symposium, July 1996
  • Symposium on logic, computers, and education, European Summer School in Logic, Language, and Information(ESSLLI), Prague, 1996
  • Logic Dissemination Meeting, by the Spinoza Logic Dissemination Group, February, 1998
  • ESSLLI 2000 included a talk on Proof systems for all by Krysia Broda of Imperial College
  • APA Computers and Philosophy Conferences
  • ITS 2000 Abstracts of invited papers gives a quick look at work by people interested in Intelligent Tutoring Systems in a big picture way.
• List of logic courseware:
  • Logic Courseware collected by Hans van Ditmarsch of the University of Otago (AI)
  • Automated deduction systems and groups listed by the Automated Reasoning Group at Argonne National Laboratory
  • Formal Methods, maintained by Jonathan Bowen
• Some sites for freshman logic courseware:
  • Bertie3, a proof checker for natural deduction systems in sentential and predicate logic. for use with the rule system of Bergmann, Moor, and Nelson, The Logic Book, 2nd edition, McGraw-Hill, 1992. This free courseware by Austen Clark at University of Connecticut, Storrs, is available for DOS, (Windows 3.x, 95 running in a DOS window), but not MacIntosh.
  • Bertrand, symbolic logic problem solving software for MacIntosh, posted by Larry Herzberg, of UCLA
  • Carnegie Mellon Proof Tutor, developed by Richard Scheines and Wilfried Sieg at Carnegie Mellon
  • CSLI software includes Turing's world, Tarski's world, Boole, Hyperproof, that were developed by the late Jon Barwise, and John Etchemendey. Available in the print and courseware package Language, Proof and Logic, works with both Windows and MacIntosh operating systems.
  • Logic Cafe, online courseware for symbolic logic, developed by John F. Halpin at Oakland University in Michigan.
  • Logic Daemon, a web-based proof checker to accompany Logic Primer, MIT Press, 2000, by Colin Allen and Michael Hand, of Texas A&M.
  • Plato, a natural deduction proof editor, and Socrates, a semantic table builder. Used by Robert C. Koons , UT Austin. It is available for PC with Windows and MacIntosh. It is used with the textbook, A Logical Toolbox, 2000.
• Some resources and/or courses using computers in logic or with logic:
  • MIZAR-MSE (proof checker) in a paper about teaching logic to freshman prospective computer science majors at University of Alberta
  • Mizar in Formal Systems and Logic in Computing Science at University of Alberta
  • ProofDesigner by Dan Velleman at Amherst is a Macintosh program that writes outlines of proofs in elementary set theory, under the guidance of the user.
  • Brown Dot Teaching Resources of Randall Pruim includes some course pages using the Barwise/Etchemendy courseware and other fun stuff
  • Helsinki Math Logic 2 appears to use Otter
  • Play with Otter, PVS, and Causal Calculator in this Stanford course
  • (Automated) Deduction and problem solving uses a variety of software including otter. Course by Kunen in Wisconsin.
  • MathXpert as a Theorem Prover, by Michael Beeson of San Jose State, in the Newsletter of the Association for Automated Reasoning, April 2001.
• Kent State University software reviews by Michael Byron
  • Criteria tracks textbook, covers categorical (Venn diagrams), propositional and predicate logics, homework done, turned in and graded over the internet, online quizzes and tests with automatic grading.
  • Barwise, Etchemendy (Boole, Fitch, Submit, Tarski's World)
  • Bergmann, et al (Bertie and Twootie)
  • Copi
  • DeHaven (BlueStorm)
  • Hurley (LogicCoach, Learning Logic (Venn diagrams, informal fallacies) Concise Introduction to Logic, 7th ed. Wadsworth, 2000
  • LogicWorks
• Kent State University textbook reviews by Michael Byron
  • Criteria
  • Language, Proof, and Logic, Jon Barwise, John Etchemendy, Seven Bridges, 1999.
  • The Logic Book, Merrie Bergmann, James Moor, Jack Nelson, McGraw-Hill, 1998. There is down-loadable free software to go with it.
  • Introduction to Logic, 10th edition, Prentice Hall, 1998
  • The Logic Course, 2nd edition, Broadview, 1998
  • A Concise Introduction to Logic, 7th ed. Wadsworth, 2000
• Keith Stenning's papers (list with bibliographic information only)
• Some links related to research on use of computers in logic education
  • Graphical effects in learning logic: reasoning, representation and individual differences, by Cox, R., and Stenning, K., apparently from a 1994 Cognitive Science Conference; it reports on Hyperproof.
  • Proofs as discourse: an empirical study, by Oberlander, Cox, Stenning. This site includes links to postscript and pdf versions of this 1995 paper which discusses research on use of Hyperproof in teaching logic to students at Stanford. It also includes citations and similar documents.
  • Contrasting the cognitive effects of graphical and sentential logic teaching: reasoning, representation and individual differences, Stenning, K., Cox, R. Oberlander, J., 1995 preprint, based on a study of Stanford students, some of whom used Hyperproof
  • Jon Oberlander: Publications including 1999 postscript preprint of a paper analysing proof logs from Hyperproof to conclude that the cognitive style of a student influences the structure of their mathematical discourse:
    Oberlander, J., Monaghan, P., Cox, R., Stenning, K. and Tobin, R. [1999] Unnatural language processing: an empirical study of multimodal proof styles. Journal of Logic, Language and Information, 8, 363-384.