This was a preliminary report on Otter-lambda. Read Papers 50, 51, and 55 below instead.
49. The mechanization of mathematics, in Teuscher, C. (ed.) Alan Turing: Life and Legacy of a Great Thinker, pp. 77-134. Springer-Verlag, Berlin Heidelberg New York, 2003.
dvi (221 kb, 55 pages).
pdf(357 kb, 55 pages)
This is a survey article on automated deduction, written for the scientist without specialized training.
50. Lambda Logic, in Basin, David; Rusinowitch, Michael (eds.) Automated Reasoning: Second International Joint Conference, IJCAR 2004, Cork, Ireland, July 4-8, 2004, Proceedings. Lecture Notes in Artificial Intelligence 3097, pp. 460-474, Springer (2004).
This paper gives the theoretical basis for the prover Otter-lambda. At the time I did not realize that AC is inconsistent with lambda logic, which makes one theorem vacuously true and leaves a gap in the proof of the completeness theorem for lambda logic. These defects are repaired in the revised version; but the published version is also given here for reference. The revised version also includes the proofs omitted from the published version because of conference proceedings length limits.
This paper describes the main algorithms of Otter-lambda and gives five example proofs.
55. Mathematical induction in Otter-lambda, Journal of Automated Reasoning> 36 (4) 2006, pp. 311-344.
Copyright has been transferred to Kluwer; this posting is in accordance with the copyright transfer agreement.
57. Implicit and explicit typing in lambda logic, unpublished. This paper addresses the relationship between proofs in a typed logic and proofs in lambda logic such as are found by Otter-lambda.
A preliminary version of this paper was presented at the ESHOL workshop at LPAR-12, December, 2005. Here's the ESHOL version:
The entire workshop proceedings can be found at http://arxiv.org/abs/cs/0601042 .