abbott@aero.ARPA (Russell J. Abbott) (05/13/88)
Does anyone have or know of a public domain, free, or cheap proof
checker that can be used by undergraduates to write and check simple
proofs. I'm teaching an automata theory and formal languages course,
and the students are having a hard time formalizing their thinking. It
would be nice if they could practice with an automated proof checker.
A simple example problem is: prove that all strings in the set denoted
by the regular expression (01 + 10)* have the same number of 0's as 1.
The proof is straightforward by induction on the length of the string.
The proof checker should have built into it knowledge of set notation,
i.e., {X | p(X)}, strings, and of inductive proofs. It should also have
a basic knowledge of simple arithmetic. Of course it also needs to be
able to use results that are proved earlier or given to it as axioms.
Thanks,
-- Russ Abbottrapaport@sunybcs.uucp (William J. Rapaport) (05/13/88)
In article <30133@aero.ARPA> abbott@aerospace.aero.org (Russell J. Abbott) writes: >Does anyone have or know of a public domain, free, or cheap proof >checker that can be used by undergraduates to write and check simple >proofs. There are proof checkers (as well as proof givers) for both propositional and predicate-logic natural-deduction systems in: Schagrin, Morton L.; Rapaport, William J.; & Dipert, Randall D. (1985) Logic: A Computer Approach (New York: McGraw-Hill). Software for them are available from: LCA Software c/o Prof. Randall R. Dipert Department of Philosophy State University College Fredonia, NY 14063 William J. Rapaport Assistant Professor Dept. of Computer Science||internet: rapaport@cs.buffalo.edu SUNY Buffalo ||bitnet: rapaport@sunybcs.bitnet Buffalo, NY 14260 ||uucp: {decvax,watmath,rutgers}!sunybcs!rapaport (716) 636-3193, 3180 ||
rgn@ecsvax.UUCP (Robert Norris) (05/13/88)
In article <30133@aero.ARPA>, abbott@aero.ARPA (Russell J. Abbott) writes: > Does anyone have or know of a public domain, free, or cheap proof > checker that can be used by undergraduates to write and check simple > proofs. I'm teaching an automata theory and formal languages course, [ requirements deleted ] I would also be interested in a proof checker for possible use in an Intro. to Theoretical Computer Science course. Thanks, Rob -- Rob Norris Dept. of Math Sciences UUCP: ...!mcnc!ecsvax!rgn Appalachian State Univ. BITNET: rgn@ecsvax Boone, NC 28608 (704) 264-2366
rapaport@sunybcs.uucp (William J. Rapaport) (05/13/88)
In article <5069@ecsvax.UUCP> rgn@ecsvax.UUCP (Robert Norris) writes: >In article <30133@aero.ARPA>, abbott@aero.ARPA (Russell J. Abbott) writes: >> Does anyone have or know of a public domain, free, or cheap proof >> checker that can be used by undergraduates to write and check simple >> proofs. I'm teaching an automata theory and formal languages course, > >[ requirements deleted ] > >I would also be interested in a proof checker for possible use in >an Intro. to Theoretical Computer Science course. Maybe this didn't get posted the first time? There are proof checkers (as well as proof givers) for both propositional and predicate-logic natural-deduction systems in: Schagrin, Morton L.; Rapaport, William J.; & Dipert, Randall D. (1985) Logic: A Computer Approach (New York: McGraw-Hill). Software for them are available from: LCA Software c/o Prof. Randall R. Dipert Department of Philosophy State University College Fredonia, NY 14063 dipert@cs.buffalo.edu dipert@sunybcs.bitnet William J. Rapaport Assistant Professor Dept. of Computer Science||internet: rapaport@cs.buffalo.edu SUNY Buffalo ||bitnet: rapaport@sunybcs.bitnet Buffalo, NY 14260 ||uucp: {decvax,watmath,rutgers}!sunybcs!rapaport (716) 636-3193, 3180 ||