Online Otter-λ
Source Code
You can download the source code for Otter-lambda and build it using gcc and the included Makefile.
Just download otter-lambda.tar, then unpack it in the directory X of your choice. That should create subdirectories "X/otter" and "X/otter2" and leave Makefile in directory X. Run "make all" in directory X. That should result in an executable file "otter-lambda" appearing in directory X.
The format of Otter-lambda input files, and the general way of working with the prover, is the same as for Otter. If you want to use Otter-lambda you should set certain options in the input file. Refer to the example input files for guidance. You should probably start with a working example file and modify it, rather than start with a blank file; this is the way people usually work with Otter.
This source code is available to you under the same terms as the source code of Otter. See the Otter legal page. It should work on any machine that can run gcc.
The version of Otter-lambda running on this web site also contains some proprietary code from MathXpert. This adds the capability to do some algebraic simplifications and to deal with integers of any size (Otter's arithmetic in $EVAL is performed mod 232). These features are not included with the source code supplied here, which is intended to show how lambda unification is implemented. Adding algebraic simplification to a first-order prover is a different topic, which was however interesting to combine with Otter-lambda because it permitted some algebraic proofs by induction to be found.
If you want to read the source code: the directory "otter" contains primarily McCune's original code, but I have had to make some changes in it. These are all commented with "Beeson" on or near the changed or inserted lines. The directory "otter2" contains the additional source code I wrote to implement Otter-lambda. In particular, unify2.c contains the code for lambda unification. You will not find this easy reading, since you must first understand the way Otter implements unification. Study McCune's "context" data structure and how it is used in unify.c, before trying to read unify2.c. Beta-reduction is in beta.c.