ACL2 Version 2.2 News

The Hyper-Card

If you are interested in learning how to program in the ACL2 subset of Common Lisp, you might want to look at the following.

Maintenance of ACL2

It has been brought to our attention that the demise of Computational Logic, Inc., has caused some potential users to shy away from ACL2 because of the fear that it would not be maintained. Don't worry about that. The ``Boyer-Moore'' theorem prover has been maintained by its two authors (with the help of a dedicated user community) for a quarter of a century without any formal organization behind it. Indeed, that personal stake in the ``product'' is part of the reason Nqthm is rugged and reliable. Matt Kaufmann and I have brought the same dedication and commitment to ACL2 (which celebrates its 9th birthday on August 14, 1998.) We have been lucky to have inherited many Nqthm users with their high expectations of reliability. We see no reason why ACL2 will not continue to be maintained. There are many reasons not to choose ACL2 as your theorem prover -- its relatively weak logic, its style of user interaction, its syntax, etc., -- but its continued maintenance is not among them.