Bank
Bank
HIS LIST comprises both provers, ie programs which
control making proofs by machines, and checkers, ie programs which test
the validity of proofs caaried out by humans, provided that a proof is
written down in a specially devised language (mentioned below versions of
Mizar provide typical examples).
The list is originally found in the American Philosophical Association resources. Encouraged by Authors' statement "additions are welcome", ', we added seven items, viz. programs called "Deductio" (Moscow), "Logika1" (Cracow, Poland), "MacLogic" (St. Andrews, Scottland), "Mizar-MSE"" nd "PC-Mizar" (Warsaw University, Poland), Theax (Japan), and Tableaux II (Oxford). Here follows the original text with the mentioned insertions.
The following is a preliminary list of logic tutorial programmes . This list is compiled from responses to our request for information concerning programmes compatible with Copi's Introductory and Symbolic Logic texts. Additions are welcome.
Deductio: interactive software for inference construction support. By A.Nowodworsky and A.Smirnov. Moscow, ILCSDP. E-mail alexey.smirnov@usa.net [Item added by the LogBank Editors.] Address for downloading: http://logic.radio-msu.net
DN-FN, by Patrice Bailhache, Dept of Philosophy, University of Nantes, B.P. 1025, 44036 NANTES CEDEX 01, France. For PC (Mac in preparation). DN is a deriver teaching how to build a natural deduction in Kleene-Gentzen's style, FN how to calculate normal forms. Available as freeware from http://193.51.78.161 or pbailhache@humana.univ-nantes.fr
Deriver, Deriver Plus. By Martin Fricke, Philosophy Department, University of Otago, Dunedin, New Zealand; Tel 03-479-8726, Fax 03-479-2305, E-mail mfricke@gandalf.otago.ac.nz. Mac (1 Mb, Version 6.0.5). Available from: Intellimation, Department Y4, P.O. Box 1530, Santa Barbara CA 93116-1530; Tel (US orders) 1-800-346-8355, Fax 1-805-968-8899.
The Electronic Accessory. Dept of Philosophy, California State University at Chico, Chico CA 95929-0730. PC or Mac. Informal logic/critical thinking.
Elementary Logic Package. Mark Watson, Dept of Mathematics and Computer Science, Hillsdale College, Hillsdale MI 49242. Mac, Windows PC, NeXt. Needs Mathematica.
Learning Logic: The Basics. Frank Williams, Dept of Philosophy, Eastern Kentucky State University, Richmond KY 40475. PC. Informal logic/critical thinking.
Logic Tutor. By Laurence Goldstein, email laurence@hkucc.hku.hk. Available from: Logical Products, Dept of Philosophy, University of Hong Kong, Pokfulam Road, Hong Kong; Tel (5) 8592796-8, Fax (852) 559-8425. PC or Mac. Venn diagrams, propositional calculus, and either argument recognition and analysis (PC) or logic games (Mac); user's manual and technical manual.
Logic/Work Checker. Nelson Pole, Dept of Philosophy, Cleveland State University, Cleveland OH 44115. PC. Proof checker.
The LogicWorks. By Bob Brady, Dept of Philosophy, Stetson University, Deland FL 32720; Bitnet Brady@Stetson. Available from: Philosophy Documentation Center, Bowling Green State University, Bowling Green OH 43403-0189; (800) 444-2419, (419) 372-2419. PC or Mac. Informal logic/critical thinking, intro to logic.
[The four following items are added by the LogBank Editors.]Logika1, accompanied by Test1 (exercises for automatic exams) - interactive checker re. sentential calculi: classical, intuitionistic, three-valued, and S4, both in the Polish and the infix notation. Contact with the author: Wojciech Sucho\'n, Logic Department, Jagiellonian University, Grodzka 52, Cracow, Poland.
MacLogic - A proof assistant for first-order logic on the Apple Macinntosh. Contact: Roy Dyckhoff, Machine Assisted Logic Teaching Project. Computational Science Division, University of St Andrews. St Andrews, Fife, Scotland, UK. rd@dcs.st-and.ac.uk
Mizar-MSE. By Andrzej Trybulec, Institute of Mathematics, Warsaw University, Bialystok Campus. Available from romat@plearn.bitnet. Proof Checker for Multi-Sorted first-order predicate calculus with Equality.
PC-Mizar. By Andrzej Trybulec, Institute of Mathematics, Warsaw University, Bialystok Campus; Available from: mizar@plbial11.bitnet. Inference Verifier for mathematical texts, combined with Main Mizar Library, ie, a set of hundreds of mathematical articles jointly involving ca. 20000 mathematical facts (theorems, definitions, schemas).
ProofDesigner. Jim Moor, Dept of Philosophy, Dartmouth College, Hanover NH 03755. Mac. Design a logic, then do proof checking in the logic.
Proof Tutor. Tom Weston, Dept of Philosophy, San Diego State University, San Diego CA 92182. PC. Proof checker that gives some advice.
Tableaux II - the logic teaching program by Duncan Watt with collab. of Michael Potter. Analytic Tableaux in two versions: Smullyan's and Hodges'. Oxford University, Computer Laboratory for Social Sciences. [Item added by the LogBank Editors.]
Tarski's World 3.0. By Barwise and Etchemendy. Mac. Available from: (1) Packaged with the textbook "The Language of First-Order Logic"; order through bookstore from University of Chicago Press. (2) Book/software from CSLI; contact Publications at CSLI, Ventura Hall, Stanford CA; Tel 415-723-1712, Fax 723-0758, Email Dirkan@csli.stanford.edu. (3) Intellimation.
THEAX System. Author Yatsuka Nakamura. A system for practical formalization of mathematics. Distribution : Executable codes (for SUN and PC) and the source code of THEAX is in pub/theax avalaible by anonymous ftp from 160.252.129.195 [Item added by the LogBank Editors.]
TUTORIALS. By Robert Cavalier and Christopher Dresibach. Available from: MacMillan. To accompany Copi's Introduction to Logic.
We would like to thank all those who provided us with information and in particular Rober Cavalier and Martin Fricke who sent us sample software. Ken Hanly, Mark Breault.