The Coq mailing list

[Daniel Nagle <Daniel.Nagle AT ul.ie>]

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

All the best,
Daniel.

-- 
Daniel A. Nagle
Postgraduate Student
Software Quality Research Laboratory
University of Limerick, Ireland.
+35361202761