some logic resolution engines that'll run within common lisp

--- SNARK -------------------------------
Runs under clisp; there are some examples ... but docs are slim.

Can understand TPTP (Tons of Problems for Theorem Provers) 
format, KIF (Knowledge Interchange Format)

http://www.ai.sri.com/~stickel/snark.html
http://www.ai.sri.com/~stickel/snark.tar.gz
http://www.ai.sri.com/snark/tutorial/tutorial.html

I have written a simplified interface to snark,
which is in the snark-..../ directory.
A clisp memory image of snark+aima+jims_simple_kb is kb.mem .

  $ clisp -M kb -m 200MB
  *** clisp + aima + snark + jim's simple kb ***
  [1]> (load "curiosity_cat" :verbose nil)
  T
  [2]> (ask '(kills curiosity tuna))
  T

---- Lisa --------------------------------------
http://lisa.sourceforge.net/
Sep 2007 lisa-32.tgz

docs:
http://lisa.sourceforge.net/ref-guide.html
"monkey and bananas"
http://lisa.sourceforge.net/mab.lisp