Online Otter-λ

Utility Link | Utility Link | Utility Link
SetTheory | Induction | LambdaLogic | Algebra | More >

Papers on or related to Otter-λsmall logo

Numbers in this list correspond to numbers in the list of all Beeson's publications.

48. Solving for functions, in: Proceedings of LMCS conference in Linz, Austria, October, 2002.
dvi (57 kb, 15 pages).
pdf(159 kb, 15 pages)

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.

Revised version (dvi, 24 pages)
Revised version (pdf, 24 pages)

Published version, dvi(62 kb, 15 pages)
Published version pdf(131 kb, 15 pages)

Two proofs were omitted from the published version of this paper to meet the 15-page length limit. Those proofs can be found here:
dvi(24 kb, 6 pages)
pdf (84 kb, 6 pages)

51. Otter-lambda, a theorem-prover with untyped lambda-unification. An earlier version of this manuscript appeared in the proceedings of the ESFOR workshop at IJCAR 2004.
dvi(96 kb)
pdf(170 kb)

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.

dvi(128 kb, 37 pages)
pdf(195 kb, 37 pages)

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.

dvi(71 kb, 15 pages)
pdf(140 kb, 15 pages)

A preliminary version of this paper was presented at the ESHOL workshop at LPAR-12, December, 2005. Here's the ESHOL version:

dvi(88 kb, 19 pages)
pdf(148 kb, 19 pages)

The entire workshop proceedings can be found at .

This material is based upon work supported by the National Science Foundation under Grant No. 0204362. Any opinions, findings, and conclusions or recommendations expressed in this material are those of the author(s) and do not necessarily reflect the views of the National Science Foundation.
include ('include/footer.php'); ?>