Date: Fri, 23 May 1997 08:16:16 -0500
From: Matt Kaufmann <kaufmann@cli.com>
To: acl2@cli.com, nqthm-users@cli.com, softverf@leopard.cs.byu.edu,
        qed@mcs.anl.gov, theorem-provers@ai.mit.edu, fsdm@it.uq.edu.au
Subject: ACL2 Version 1.9
Content-Type: text
Content-Length: 1496

We are pleased to announce the release of Version 1.9 of the ACL2 theorem
proving system.  ``ACL2'' stands for ``A Computational Logic for Applicative
Common Lisp.''  ACL2 is similar to the Boyer-Moore theorem prover, Nqthm, and
Kaufmann's interactive extension, Pc-Nqthm.  However, instead of supporting the
``Boyer-Moore logic,'' ACL2 supports a large applicative subset of Common Lisp.
Furthermore, ACL2 is programmed almost entirely within that language.  It is
extensively documented in Postscript, HTML, and Emacs Info formats.

You can find your way to the ACL2 Version 1.9 home page by visiting
Computational Logic, Inc. at http://www.cli.com, or you can go directly to
http://www.cli.com/software/acl2/v1-9/acl2-doc.html .  From there you can get
more information about ACL2, and you can download it.  If you merely want to
know what is new in Version 1.9, visit:
http://www.cli.com/software/acl2/v1-9/acl2-doc-52.html#NOTE9 .

If you would like to join the unmoderated ACL2 mailing list, acl2@cli.com, send
to acl2-request@cli.com a message containing as its body (NOT its Subject) the
the single word `subscribe'.  To get general information about the mailing
list, send the word `info' (this will not subscribe you to the mailing list).
To send a message to all who receive ACL2 mail, send the message to
acl2@cli.com.  Finally, please report bugs in ACL2 to acl2-bugs@cli.com.

We gratefully acknowledge Bob Boyer's significant contributions to this work.

Matt Kaufmann and J Moore