I have added the examples from this week's lecture to the Handouts page.
Our first exercise will be the graph-theory example from Chapter 5 of the ACL2 Case Studies book. Please start reading this chapter and doing all the exercises. Take your time, and do it carefully, without peeking at the answers in the book or on the website. It will be easier to do after the discussion of the theorem-prover internals next week, but please start (at least) reading now.
You can now download a compiled version of ACL2. This will save you steps 2-4 of the installation instructions. Just open the zip file into your acl2-sources directory instead.
The meeting place has been changed to Schreiber 210.
As agreed in the first meeting, the meeting time will be changed to Sundays 15:00-17:00. I will only know the place on Sunday morning, and I will notify you by e-mail as well as on this page.