

InstructorThe Interdisciplinary Center, Herzliya Email: yishai@idc.ac.il Phone: (09) 9527305 IntroductionThis is the home page for the course ComputerAided 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 email to yishai@idc.ac.il. For bureaucratic reasons, this course counts as a seminar (2 points). The purpose of this course is to give students handson experience using computeraided 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 industrialstrength 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. ScheduleTime: Sundays 15:0017:00. Place: Schreiber 210. Reference MaterialTextbooksThe main texts for this course are the two books describing ACL2 and several large case studies:
OnLine Material
Obtaining and Installing the SoftwareInstallation 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 nonstandard analysis. The installation of ACL2(r) is a little different from that of ACL2, although it uses the same sources. 