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; Mon, 24 Oct 1994 04:59:14 +0000
Received: by leopard.cs.byu.edu (1.38.193.4/16.2) id AA15003;
          Sun, 23 Oct 1994 22:56:21 -0600
Sender: info-hol-request@lal.cs.byu.edu
Errors-To: info-hol-request@lal.cs.byu.edu
Precedence: bulk
Received: from Maui.CS.UCLA.EDU by leopard.cs.byu.edu 
          with SMTP (1.38.193.4/16.2) id AA14999;
          Sun, 23 Oct 1994 22:56:20 -0600
Received: from LocalHost.cs.ucla.edu by maui.cs.ucla.edu (Sendmail 4.1/3.26) 
          id AA16501; Sun, 23 Oct 94 21:48:56 PDT
Message-Id: <9410240448.AA16501@maui.cs.ucla.edu>
To: info-hol@leopard.cs.byu.edu
Subject: Major traditions in mechanical theorem proving
Date: Sun, 23 Oct 94 21:48:55 PDT
From: chou@cs.ucla.edu


Hello,

I am writing my dissertation and would like to briefly mention in it
the major traditions in or approaches to mechanical theorem proving.
As I am untutored in this area, I know only of a few:

* LCF-like systems: LCF, HOL, Nuprl, Coq (?), and what else?

* Resolution-based systems: Otter, and what else?

* Boyer-Moore: where did it come from?

* Rewriting-based systems: LP, and what else?

* Logical frameworks: Isabelle, LF, and what else?

I would appreciate your inputs on:

(1) Does the classification above make any sense at all?

(2) Additions/corrections to the list above.

(3) Survey/representative articles/reports/books that I can cite.

Many thanks in advance!!!

- Ching Tsun