ACL2 Seminar
April 21, 2010
J Moore

Title: Random Topics in ACL2

Abstract:

Today I will discuss three ``random'' topics
related to ACL2.  The first concerns the
verification of the guards for the
``too-many-ifs'' heuristic that controls the
opening of non-recursive function definitions.
The second concerns the ``improvement'' of the
forward-chaining heuristic and a rather bizarre
interaction with linear arithmetic that causes
some previously successful proof scripts to fail.
The third concerns a little pre-history of the
very first Boyer-Moore style theorem prover
written in Edinburgh in 1971.