The Interdisciplinary Center, Herzliya
Phone: (09) 9527305
This is the home page for the course Computer-Aided Reasoning. This course is currently given in an experimental form to selected graduate students at Tel Aviv University. Registration is limited, by instructor permission only. To apply, send e-mail to firstname.lastname@example.org. For bureaucratic reasons, this course counts as a seminar (2 points).
The purpose of this course is to give students hands-on experience using computer-aided reasoning systems, with a particular orientation towards reasoning about programs. The tool we will use is ACL2, which is a descendant of Boyer and Moore's theorem prover Nqthm. This industrial-strength system has been used in a number of commercial applications, and has extensive documentation, including the two textbooks. During the course, we will explore the logic of ACL2, try some small projects, and follow some of the case studies.
Time: Sundays 15:00-17:00.
Place: Schreiber 210.
The main texts for this course are the two books describing ACL2 and several large case studies:
Obtaining and Installing the Software
Installation of ACL2 is quite complex. If you are installing on a Windows platform, follow the provided instructions. For other platforms, follow the instructions in the ACL2 installation page. (In that case, you may be able to download an existing executable.)
Chapters 6 and 18 of the ACL2 Case Studies book use a modification of ACL2 called ACL2(r), which can be used for reasoning about the real numbers using non-standard analysis. The installation of ACL2(r) is a little different from that of ACL2, although it uses the same sources.