Return-Path: <John.Harrison-request@cl.cam.ac.uk>
Delivery-Date: 
Received: from leopard.cs.byu.edu (no rfc931) by swan.cl.cam.ac.uk 
          with SMTP (PP-6.5) outside ac.uk; Sun, 17 Oct 1993 09:29:14 +0100
Received: by leopard.cs.byu.edu (1.37.109.4/16.2) id AA22012;
          Sun, 17 Oct 93 02:14:28 -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 AA22006; Sun, 17 Oct 93 02:14:27 -0600
Received: from Maui.CS.UCLA.EDU by dworshak.cs.uidaho.edu 
          with SMTP (1.37.109.4/16.2) id AA21848; Sun, 17 Oct 93 01:14:16 -0700
Received: from LocalHost.cs.ucla.edu 
          by maui.cs.ucla.edu (Sendmail 5.61d+YP/3.22) id AA23332;
          Sun, 17 Oct 93 01:11:58 -0700
Message-Id: <9310170811.AA23332@maui.cs.ucla.edu>
To: info-hol@cs.uidaho.edu
Subject: Theorem provers of the world
Date: Sun, 17 Oct 93 01:11:57 PDT
From: chou@cs.ucla.edu

Ours seems to be the Golden Age of mechanical theorem proving.
I do HOL hacking fairly often and, to list just a few, I know
of the existence of LCF, Isabelle, Nuprl, IMP, Nqthm, Automath,
Ontic, Coq, PVS, EHDM, LP, Otter, TPS, SDVS, .....
Are there papers in which some of these systems are surveyed,
compared, and classified?

- Ching Tsun