abbott@AEROSPACE.AERO.ORG (Russell J. Abbott) (05/06/88)
Does anyone have or know of a public domain (or cheap) proof checker
that can be used by undergraduates to write and check simple proofs. I'
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)} 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 AbbottAIList-REQUEST@AI.AI.MIT.EDU (AIList Moderator Nick Papadakis) (05/25/88)
Date: Tue, 17 May 88 11:17:17 From: Leslie Burkholder <lb0q+@andrew.cmu.edu> To: AILIST@ai.ai.mit.edu Subject: proof checker Two queries concerning proof checkers have appeared. How about either (1) The Boyer-Moore theorem prover. Contact Computational Logic Inc 1717 West Sixth St Suite 290 Austin Texas 78703 (2) Mizar. Contact Andrzej Trybulec / Howard Blair EECS University of Connecticut Storrs CT 06268 Leslie Burkholder (If anyone suggests anything else please let me know.)