The Coq mailing list

[Jean-Christophe Filliatre <filliatr AT lri.fr>]

Hello,

Adam Chlipala writes:
 > 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.

Freek  Wiedijk  compiled  a   detailed  comparison  of  several  proof
assistants, including the presence / lack of de Bruijn criterion which
is your question. See page 10 of this article

  http://www.cs.ru.nl/~freek/comparison/diffs.ps.gz

and the whole web page at

  http://www.cs.ru.nl/~freek/comparison/index.html

 > 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.

I'm aware of at least two decision procedures that output proof terms
to be checked independently:

- CVC Lite : http://verify.stanford.edu/CVCL/

- Zenon; this prover is part of the Focal distribution : 
http://focal.inria.fr/

Hope this helps,
-- 
Jean-Christophe Filliâtre (http://www.lri.fr/~filliatr)