Slides

• Lecture 03 - Theorem prover ACL2
• ACL2 handout
• ACL2 control script

Running ACL2 on Ubuntu

• install packages acl2 and acl2-emacs
• if you use emacs23, that should be enough
• however, if you use emacs24 you need also to fix things a bit:
  • edit /usr/share/emacs24/site-lisp/acl2/emacs-acl2.elc and replace "emacs/monitor.el" with "acl2/monitor.el"
  • create a link: # ln -s /usr/share/emacs/site-lisp/acl2/monitor.el /usr/share/emacs24/site-lisp/acl2/monitor.el

Supplementary materials

• ACL2 webpage - lots of examples, tutorials ...
• Isabelle/HOL theorem prover - higher order logic
• Coq proof assistant - constructive proofs can be executed