Return-Path: Delivery-Date: Received: from leopard.cs.byu.edu (no rfc931) by swan.cl.cam.ac.uk with SMTP (PP-6.5) outside ac.uk; Mon, 18 Oct 1993 10:28:48 +0100 Received: by leopard.cs.byu.edu (1.37.109.4/16.2) id AA17201; Mon, 18 Oct 93 03:18:52 -0600 Sender: info-hol-request@leopard.cs.byu.edu Errors-To: info-hol-request@leopard.cs.byu.edu Precedence: bulk Received: from dworshak.cs.uidaho.edu by leopard.cs.byu.edu with SMTP (1.37.109.4/16.2) id AA17195; Mon, 18 Oct 93 03:18:44 -0600 Received: from swan.cl.cam.ac.uk by dworshak.cs.uidaho.edu with SMTP (1.37.109.4/16.2) id AA23151; Mon, 18 Oct 93 02:18:34 -0700 Received: from teal.cl.cam.ac.uk (user rjb (rfc931)) by swan.cl.cam.ac.uk with SMTP (PP-6.5) to cl; Mon, 18 Oct 1993 10:15:33 +0100 To: chou@cs.ucla.edu Cc: info-hol@cs.uidaho.edu Subject: Re: Theorem provers of the world In-Reply-To: Your message of "Sun, 17 Oct 93 01:11:57 PDT." <9310170811.AA23332@maui.cs.ucla.edu> Date: Mon, 18 Oct 93 10:15:19 +0100 From: Richard Boulton Message-Id: <"swan.cl.cam.:130670:931018091558"@cl.cam.ac.uk> In addition to the papers cited by Catia there is: @InCollection{BMproverNuprlComparison, author = "D. A. Basin and M. Kaufmann", title = "The Boyer-Moore Prover and Nuprl: An Experimental Comparison", booktitle = "Logical Frameworks", publisher = "Cambridge University Press", year = "1991", pages = "89--119", note = "Also: Research Paper 525, Department of Artificial Intelligence, University of Edinburgh."} You may also be interested in Carolyn Talcott's database of information about automated reasoning systems which is accessible by anonymous ftp: ftp sail.stanford.edu Directory: /pub/clt/ARS