Handouts

 

Home
Announcements
Handouts
Windows Installation
Installing ACL2(r)

Examples

Flatten

A comparison of a recursive quadratic and an iterative linear implementation of the classic "flatten" function.

Tautology Checker

This is an adaptation of the tautology checker example from Chapter IV of Boyer and Moore's A Computational Logic, Academic Press, 1979.

Theorem-Prover Internals

Utilities

For Emacs

Here is my emacs initialization file.  If you put it in your home directory (C:\, unless you did something special) it will be loaded automatically when emacs starts.