From: IN%"srlclark@liverpool.ac.uk" 24-FEB-1994 20:45:04.55 To: IN%"philos-l@liverpool.ac.uk" "Members of the list" CC: Subj: Logic Software 0.3 (fwd from philosop) Received: from mailhub.liverpool.ac.uk (mail.liv.ac.uk) by vax.csc.cuhk.hk (PMDF #12160) id <01H99ZL2483K8Y52MH@vax.csc.cuhk.hk>; Thu, 24 Feb 1994 20:44 +0800 Received: from liverpool.ac.uk by mailhub.liverpool.ac.uk with Local-SMTP (PP) id <28658-0@mailhub.liverpool.ac.uk>; Thu, 24 Feb 1994 12:40:23 +0000 Date: Thu, 24 Feb 1994 12:40:23 GMT From: Stephen Clark Subject: Logic Software 0.3 (fwd from philosop) Sender: philos-l-request@liverpool.ac.uk To: Members of the list Reply-to: srlclark@liverpool.ac.uk Message-id: <9402241223.AA25047@uxe.liv.ac.uk> Content-type: text/plain; charset=US-ASCII Originator: philos-l@liverpool.ac.uk Precedence: bulk X-Listprocessor-Version: 6.0c -- ListProcessor by Anastasios Kotsikonas X-Comment: UK Philosophers Content-Length: 7832 Mime-Version: 1.0 > From: "Eric J. Forbis" > > Below is an amended and slightly enlarged version of the list of logic > software that I recently posted. Many thanks to all those who emailed with > suggestions, hints, and descriptions! This list is still incomplete, > and the descriptions spotty to nonexistent; my apologies to any I may have > slighted. If you note any inaccuracies, or are aware of software that > should be included, please drop a note. I have received brief reviews of a > number of the programs listed, and hope to substitute these for the > present sketchy outlines soon. > > ----------------Begin Logic Software List----------------------------- > > > Logic programs and teaching aids, theorem provers and languages. > > ------------Public Domain Programs------------------------------------ > > 1. PROOFCHK > For use with the Shaum's _Outline of Logic_, natural deduction. > Student enters proof and the theorem prover (a help button) offers > graded series of hints for solutions. Also includes a validity > checker and help screens. > Send a disk and self- addressed stamped mailer to: > John Nolt > Philosophy Department > University of Tennessee > Knoxville, TN 37996-0480 > > 2. *Nqthm > Boyer- Moore theorem prover (see book by same authors). > Rascal.ics.utexas.edu :/pub/nqthm > > 3. *Proof-checker > rascal.ics.utexas.edu :/pub/proof-checker > > 4. *Otter Theorem Prover > Used with _Automated Reasoning: Introduction and Applications_, > Larry Wos et al, McGraw-Hill 1992. > Herky.cs.uiowa.edu :/public/otter > > 5. *DTP > meta.stanford.edu :/pub/dtp > > 6. ***Setheo SEquential THEOrem prover > Sun Sparcstations and X Windows. > flop.informatik.tu-muenchen.de (131.159.8.35) :/pub/fki > email: setheo@informatik.tu-muenchen.de > > 7. *HOL (Higher Order Logic) > Used with _Introduction to HOL: A Theorem Proving Environment for > Higher Order Logic_. Ed. M.J.C. Gordon and T.F. Melham, Cambridge > University Press 1993 > ftp.cs.tut.fi :/pub/src/DisCo/hol90.6 > > > 8. MacLL > "MacLogic-like proof editor for linear logic", by Roy Dyckhoff > and the MALT (Machine Assisted Logic Teaching) project at > St. Andrew's University. > 138.251.192.40 (tamdhu.dcs.st-and.ac.au) :/pub/malt/macLL. Also > get MacLogic fonts from /pub/malt/maclogic. > > 9. Coq > "Implementation of the Calculus of Inductive Constructions, a powerful > logic accepting higher-order reasoning and definition of a > wide class of functions. It also allows the extraction of proven- > correct ML programs from proofs. It is implemented in caml-light > (ML dialect) and thus runs on unix machines, macintosh's and PC's." > ftp.inria.fr :/INRIA/coq. > email address: coq@margaux.inria.fr. > > 10. Isabelle > General theorem prover, many-sorted first-order logic, constructive > and classical versions higher-order logic, Zermelo-Fraenkel set theory, > an extensional version of Martin-L\"of's Type Theory, the classical > first-order sequent calculus LK, the modal logics T, S4, and S43, > the Logic for Computable Functions, LCF, the Lambda Cube. > ftp.cl.cam.ac.uk [128.232.0.56] :/ml/Isabelle93.tar.gz > email: Larry.Paulson@cl.cam.ac.uk (Lawrence Paulson) > > 11. **Cambridge LCF Logic for Conputable Functions > Interactive theorem prover. Proofs conducted in PPLAMBDA, > a natural deduction logic based on the domain theory of Dana Scott, > and is particularly suitable for proofs involving denotational > semantics, lazy evaluation, or higher-order functions. > LCF provides a metalanguage (Standard ML), a functional programming > language whose values include PPLAMBDA terms, formulas, and theorems. > Theorem-proving primitives such as inference rules, subgoaling > strategies (tactics), and simplifiers are implemented as ML functions. > The user can extend LCF by programming in ML. > ftp.cl.cam.ac.uk :\ml > > 12. Mizar MSE first order Multi- Sorted predicate calculus with Equality > Logic validity and proof checking, mathematical proofs. > menaik.cs.ualberta.ca (129.128.4.241) :/pub/Mizar-MSE > email: piotr@cs.ualberta.ca (Piotr Rudnicki) > > 13. Nuprl3 > Proof development system described in _Implementing Mathematics_, > Prentice-Hall, 1986. Nuprl4 scheduled for released late August > 1994. > ftp.cs.cornell.edu :/pub/n/nuprl-3-2.tar.Z > :/pub/nuprl (docs) > email: kate@cs.cornell.edu (Prof. Constable) > > > > * Requires LISP. Kyoto Common Lisp seems to be widely compatible > with most of the above. At rascal.ics.utexas.edu, amoung many other > sites, and has been ported to most operating systems. > ** Requires Franz Lisp > *** Requires Scheme. Available at this site (flop.informatik....). > > > > -------Commercial---Programs------------------------------------------- > > > 1. MacLogic > Minimal, intuitionistic, classical propositional & predicate > calculi, with theorem provers. > Macintosh > Contact Roy Dyckhoff, the author, at rd@dcs.st-and.ac.uk for > an informational sheet with directions for ftping. > > > 2. LogicWorks College level intro logic. > 700 Excersizes and programs, $18 demo (?), DOS 2.0+ > Philosophical Documentation Center > Bowling Green State University > Bowling Green, OH 43403-0189 > (800) 444-2419 > > 3. Logic: A Workbook > Teaches college level symbolic logic. > Price unknown, DOS 2.0+. > Logic Software Project > Department of Philosophy > University of California, Los Angeles > Los Angeles, CA 90024-1451 > (310) 825-4641 > > 4. LogicCoach > Educational software for the Hurley and Kahane logic texts. User > friendly proof checker through 1st order functional calculus w/identity. > Distributed by the Wadsworth Publishing Company. > > 5. Symlog > College level symbolic logic educational software designed to be > used with _Logic with Symlog_, Frederic Portoraro and Robert Tulley. > Distributed by Prentice- Hall. > > > 6. Tarski's World 4.0 > 1st order logic educational software to supplement any standard > logic text. Represents logical propositions in graphical worlds, > manual and exercises. By Jon Barwise and John Etchemendy. > Macintosh and Windows, $19.50 > Distributed by the University of Chicago Press. For more information, > contact Dean Blobaum at dblobaum@press.uchicago.edu. > > 7. The Language of First- Order Logic_, 3rd edition. > A 1st order symbolic logic text that includes Tarski's World 4.0. > Macintosh and Windows, $34.95 > Distributed by the University of Chicago Press. For more information, > contact Dean Blobaum at dblobaum@press.uchicago.edu. > > 8. Turing's World 3.0: Introduction to Computability Theory > Software for diagramming Turing machines, includes short text > on Turing machines with software- integrated exercises. > Macintosh, $19.95 > Distributed by the University of Chicago Press. For more information, > contact Dean Blobaum at dblobaum@press.uchicago.edu. > > 9. Hyperproof > Text and software for analytic reasoning, can be used with items > 6 and 7 in this section. "Combines graphical and sentential > information, and presents a set of logical rules for integrating > these different forms of information." > Macintosh, $24.95 > Distributed by the University of Chicago Press. For more information, > contact Dean Blobaum at dblobaum@press.uchicago.edu. > > > -------------End Logic Software List------------------ > > Regards, > -=-=-=-=-=-=-=-=-=-=-=-= > Eric J. Forbis > forb0004@gold.tc.umn.edu >