http://www.ccs.neu.edu/home/cce/acl2/ Erich Rast wrote: > Is there a theorem prover for first-order predicate logic or normal > modal logics written in Scheme? If not, has perhaps someone written an > interface to access an existing theorem prover in MzScheme? >