The Coq mailing list

[Hugo Herbelin <herbelin AT pauillac.inria.fr>]

  Hi,

> I am a student currently working on preparing a number of problems for
> benchmarking automated theorem provers. My work concentrates on locating
> atp's that provide the best support for tabular expressions and the
> logic introduced by David Parnas in his paper "Predicate Logic for
> Software Engineering". I am wondering how Coq was orginally benchmarked
> against other theorem provers and what method and problems were used in
> this process. Any help you can offer me in this subject is greatly
> appreciated.

  I don't believe that Coq can be basically considered as an automated
theorem provers. Coq is before all a proof assistant that provides
support (and logical confidence) for formalizing proofs of
mathematical statements and/or properties of programs. As a proof
assistant, it includes a few basic automation procedures (decision of
quantifier-free Presburger arithmetic, decision of bounded first-order
predicate logic, decision of quantifier-free field expressions,
decision of euclidean geometry, congruence closure, ...) but without
claims of efficiency compared to what a theorem prover specifically
designed for automation provides.

  Hugo Herbelin