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. -- Best, Bill ____________________ Racket Users list: http://lists.racket-lang.org/users
