ACL2 Support for Interactive Proof
The slides below are for a talk presented by Matt Kaufmann at
Chalmers, Gothenburg, Sweden, August 10, 2015.
Abstract
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
- Slides (pdf)
Note: Some material on the slides will likely be
skipped.
- Associated demo materials (originally for KeY 2015 invited talk), including logs