Reply-To: info-hol@ted
Sender: info-hol-request@edu.uidaho.cs.ted
Errors-To: info-hol-request@ted.cs.uidaho.edu
Date: Tue, 12 Nov 1991 11:12:04 +1100
From: Zdzislaw Meglicki <Zdzislaw.Meglicki@au.edu.anu.arp>
Message-Id: <199111120012.AA14311@diana.anu.edu.au>
To: info-hol@edu.uidaho.cs.ted
Subject: Which HOL?

I am modifying the layout and architecture of the computer systems I am
responsible for. One of the things I would like to install after all the
upgrades are over is, naturally, HOL. But which one? I've noticed having
received numerous mailing messages from this group, that there are quite
a few HOLs around these days. There are some which build on top of the
New Jersey SML, some that go along with Common Lisp and still some that
build on top of Franz Lisp. Which is the latest that would vanilla install
and work on Sun SPARCstations running SunOS 4.1.1? I have AKCL 1.600,
New Jersey SML 0.66, and I hope to have Sun Common Lisp (Lucid?). Where
is the best place to get the sources from (via ftp)? What HOL front ends
have been developed so far and where can I get those from? These may sound
like "Frequently Asked Questions", if so then perhaps some HOL guru could
send answers to those from time to time (say, once a month?).

Another (Frequently Asked?) question: my primary interests are in proving
theorems of (applied) mathematics mostly in areas such as analysis, functional
analysis, differential geometry, etc. Perhaps even moving into such notoriously
ill-defined areas as quantum mechanics and quantum field theory. Is HOL any
good for that? How would HOL compare against NuPRL, Boyer Moore, Isabelle?
How versatile and powerful is its system of tacticals? Is there a stage at
which a very formal system such as HOL should be dropped in favour of an
expert system? I had a fairly good look at the last three provers (i.e.,
NuPRL, Boyer Moore, and Isabelle). They all have some very interesting
features: NuPRL has a nice user interface, Isabelle seems marvelously
versatile and powerful, Boyer Moore can prove theorems of great difficulty
(but it takes a PhD project to write the input file) - still, I would be most
interested to hear from people who have done some real work in this area
themselves, and actually tried out more than one system, so that they can
comment on things such as ease of use, versatility, ability to link with the
external world, etc.  It looks to me like HOL is by far the most popular and
fastest developing system of all - but... will it do for me?

Regards,
Gustav

   Zdzislaw Gustav Meglicki, gustav@arp.anu.edu.au,
   postmaster@arp.anu.edu.au, postmaster@vulcan.anu.edu.au

   Automated Reasoning Project - CISR, and Plasma Theory Group - RSPhysS,
   The Australian National University, G.P.O. Box 4, Canberra, A.C.T., 2601,
   Australia, fax: (Australia)-6-249-0747, tel: (Australia)-6-249-0158

P.S.

   I am archiving this mailing group on one of my systems; if you do
   ftp-anonymous to arp.anu.edu.au and go to archive/anu/reasoning you'll
   find there 258 messages (some compressed) archived over the last year.
   This archive will be moved around a little in about one or two months
   time, but it'll be still there. Oh, yes, why don't I just look into
   it myself in order to answer the questions I asked above? I will, I
   promise, I will.