Examples

Flatten

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

• The functions and theorems: flatten.lisp.
• The full proof: flatten-proof.txt.

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.

• The functions and theorems: taut2.lisp.
• An alternative formulation: taut3.lisp.

Theorem-Prover Internals

• The ordinal functions: ordinals.txt.
• An induction example: induction.txt.
• Rev-rev examples: rev-rev.txt.

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.