As far as I know, Otter has not, nor ever has used Lisp as the basis for its
code. It is coded in C. You might be able to find a similar type of
resolution and paramodulation algorithm for Lisp in one of the AI archives,
though.
Otter itself (along with source code) is available from Argonne National
Labs at http://www-unix.mcs.anl.gov/AR/otter/. The main reference for the
program is the book by Wos, Overbeek, Lusk & Boyle: Automated Reasoning:
Introduction and Applications, 2nd edition. This book gives an overview of
theorem proving and Otter's resolution and paramodulation algorithms in
particular.
faa
Dahai Guo wrote in message <·················@cec.wustl.edu>...
>Hi, Friends:
>
>I am wondering if anybody knows where I can get the basic "otter" lisp
>code for theorem provers ?
>
>Thanks,
>
>Dahai Guo
>
>