ACL2 Support for Interactive Proof

The slides below are for a talk presented by Matt Kaufmann at Chalmers, Gothenburg, Sweden, August 10, 2015.


This talk is intended to give a sense of the ACL2 system, especially how it supports user interaction. It will begin with a high-level introduction to ACL2 and its ``Boyer-Moore'' predecessors, including brief remarks on a theorem prover for an ancestor of Haskell. Then the talk will illustrate ACL2 interaction through a series of demos. Questions will be encouraged!

Talk materials