The Coq mailing list

[Adam Chlipala <adamc AT cs.berkeley.edu>]

Can anyone provide a summary of which interactive proof assistants 
besides Coq produce a proof of each goal that is successfully 
discharged, and which definitely don't?  By "a proof" I mean a more or 
less efficiently checkable (meaning no "search" is required) term in 
some (hopefully simple) logic.

I'm also interested in automated deduction tools in general that produce 
such proofs.  It seems that the list of tools in this category isn't as 
large as I expected, but I might be looking in the wrong places.

Thanks!