Subject: Second Edition of A Computational Logic Handbook
From: [email-masked]
To: [email-masked]
Date: Tue, 21 Oct 1997 10:54:25 -0500 (CDT)

The second edition of the book "A Computational Logic Handbook" is now in
print.

   Robert S. Boyer and J Strother Moore, A Computational Logic Handbook,
   Second Edition, Academic Press, 1997, ISBN 0121229556. 518+xxv pages.
   Be sure to mention "second edition".

It could be hard to find it in book stores just yet, so we mention the
Academic Press 800 number, 1-800-321-5068.  $69.95.

The second edition is the authoritative documentation for Nqthm-1992, the
most recent edition of the Boyer-Moore prover, which may be obtained with
sources and without fee at

  ftp://ftp.cs.utexas.edu/pub/boyer/nqthm/index.html.

In addition to a very large number of minor corrections and improvements to
the first edition, here are some of the major differences of the second
edition over the first

     describes new syntax, including COND, CASE, LET, LIST*, and backquote
     describes some "higher order" inference procedures, including
         "constrained functions" and "functional instantiation"
     documents more sophisticated control machinery for manipulating
         very large theories
     introduces a "secure" proof-checking environment
     describes thousands of pages of fascinating example input dealing with
         very difficult questions in formal methods and mathematics
     provides a formal parser for the syntax
     compares the proof complexity of many interesting checked examples
     includes much new tutorial help, especially for the many 
         new features
     contains a thorough bibliography of interesting Nqthm
         applications

Bob Boyer and J Moore

P. S.  There is a "new" release of Nqthm-1992 available at
ftp://ftp.cs.utexas.edu/pub/boyer/nqthm/index.html.  However, this is
actually only a "bureaucratic" update to make slightly easier the life of
folks who wish to install Nqthm from scratch.  This new release combines the
Nqthm-1992 "release" of 1994 with the "examples" of 1995.  In other words, if
you already have a working Nqthm-1992 and the 1995 examples release, it's
probably a waste of your time to do a reinstallation.  (There is actually
something new included: the ancient and crufty but operational Lisp code for
our Fortran Verification Condition Generator, in directory
examples/fortran-vcg.)

From: [email-masked]
Date: Tue, 21 Oct 1997 10:54:25 -0500 (CDT)
To: [email-masked]
Subject: Second Edition of A Computational Logic Handbook
Content-Type: text
Content-Length: 2270

The second edition of the book "A Computational Logic Handbook" is now in
print.

   Robert S. Boyer and J Strother Moore, A Computational Logic Handbook,
   Second Edition, Academic Press, 1997, ISBN 0121229556. 518+xxv pages.
   Be sure to mention "second edition".

It could be hard to find it in book stores just yet, so we mention the
Academic Press 800 number, 1-800-321-5068.  $69.95.

The second edition is the authoritative documentation for Nqthm-1992, the
most recent edition of the Boyer-Moore prover, which may be obtained with
sources and without fee at

  ftp://ftp.cs.utexas.edu/pub/boyer/nqthm/index.html.

In addition to a very large number of minor corrections and improvements to
the first edition, here are some of the major differences of the second
edition over the first

     describes new syntax, including COND, CASE, LET, LIST*, and backquote
     describes some "higher order" inference procedures, including
         "constrained functions" and "functional instantiation"
     documents more sophisticated control machinery for manipulating
         very large theories
     introduces a "secure" proof-checking environment
     describes thousands of pages of fascinating example input dealing with
         very difficult questions in formal methods and mathematics
     provides a formal parser for the syntax
     compares the proof complexity of many interesting checked examples
     includes much new tutorial help, especially for the many 
         new features
     contains a thorough bibliography of interesting Nqthm
         applications

Bob Boyer and J Moore

P. S.  There is a "new" release of Nqthm-1992 available at
ftp://ftp.cs.utexas.edu/pub/boyer/nqthm/index.html.  However, this is
actually only a "bureaucratic" update to make slightly easier the life of
folks who wish to install Nqthm from scratch.  This new release combines the
Nqthm-1992 "release" of 1994 with the "examples" of 1995.  In other words, if
you already have a working Nqthm-1992 and the 1995 examples release, it's
probably a waste of your time to do a reinstallation.  (There is actually
something new included: the ancient and crufty but operational Lisp code for
our Fortran Verification Condition Generator, in directory
examples/fortran-vcg.)

From: [email-masked] (Warren A. Hunt Jr.)
Date: Tue, 23 May 95 10:06:19 CDT
To: [email-masked]
Subject: FM9001 Announcement

Dear Carolyn,

Bob Boyer suggested that I convey the announcement of the public
release of the FM9001 microprocessor: its specification, design, and
correctness proof.  We hope that you may find the results of this
research to be valuable, and we look forward to any feedback you may
have.

Warren
++++++
                      The FM9001 Microprocessor:
                     Its Formal Specification and
                     Mechanical Correctness Proof

                            Spring 1995

We are releasing the mechanically checked proof scripts for the FM9001
microprocessor.  The FM9001 is a general-purpose 32-bit microprocessor
which has been implemented as a CMOS ASIC.  The proof being released
rigorously connects the expression of the FM9001 as a netlist with the
characterization of the FM9001 at the machine-code programmer's level.
(The FM9001 is the foundation of the `CLI Stack', which also includes
several verified compilers and applications all running on the FM9001.
Other parts of the `CLI Stack' are separately released.)

To obtain information about the FM9001 microprocessor and proof,
please examine the URL http://www.cli.com/hardware/fm9001.html

To obtain the FM9001 system, connect to Internet site ftp.cli.com by
anonymous ftp, giving your email address as the password, `get' the
file /pub/fm9001/README and follow the instructions therein.  Or get
the URL ftp://ftp.cli.com/pub/fm9001/README via your WWW browser.

Bishop C. Brock and Warren A. Hunt, Jr.
[email-masked]       [email-masked]