Theorem Proving
Tableaux in Lisp
Another Tableaux