Bill Richter wrote:
>Carl Eastlund developed Dracula for Rackety use of the ACL2 theorem
>prover.
Thanks, Ian! May I suggest that you try to handle Coq, Isabelle or
HOL Light? I believe these are the foremost proof assistants. The
fields medalist Vladimir Voevodsky uses Coq, in which the 4-color
theorem and the Feit-Thompson theorem was formalized by Georges
Gonthier. Tom Hales just finished formalizing his proof of Kepler
conjecture in HOL Light and Isabelle (which is HOL as well). I'm no
expert, but I think that ACL2 (also Prover9) is an FOL prover, and
the bulk of activity in formal proofs uses type theories. HOL is
simple, it's Church's simple types (a version of the Lambda
Calculus), and Coq uses a much more complicated type theory.
I'm sorry, I forgot about Carl's Dracula work when composing my earlier
reply. ACL2 is more limited, but its advantage (besides being probably
far and away the theorem prover that has had the most industrial impact)
is that its language (Applicative Common Lisp, hence the acronym) is
much closer to Racket, allowing for stronger integration both with
DrRacket and into a Racket-based curriculum. A DrRacket interface to Coq
or Isabelle would, in contrast, be more superficial, in the style of
Proof General. --PR
____________________
Racket Users list:
http://lists.racket-lang.org/users
