[plt-scheme] Theorem Prover

Hi folks,

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?

Another question: Has anyone on the list found a smart trick to look  
in Google for programs implemented in Scheme. Using "mysearchterm  
Scheme" produces just about anything about mysearchterm, since  
everyone uses the word "scheme" at one place or another. It seems to  
me that the name of the programming language wasn't a very wise  
choice with that respect, but to be fair, who could have anticipated  
Google and Altavista in the 70s. ;-) I usually add "PLT", "mzscheme",  
or "R5RS", but always fear I miss some search results.

Best regards,

Erich