Introduction to Otter-λ
Otter-λ is a theorem-proving program. It accepts as input a list of axioms and a theorem to try to prove, and if successful, it outputs a proof of that theorem from those axioms. The subject whose aim is to construct programs that do that is called automated deduction, or perhaps somewhat more generally, automated reasoning. This web site is devoted to explaining Otter-λ to any interested parties. These parties vary widely in background and interest, from high-school students to graduate students to experts in the field. Therefore we intend to provide a number of links from this page to background information needed to understand the aims of the field of automated deduction and the methods used in Otter-λ, without attempting to provide a complete course in the subject. In addition to general information about automated deduction and specific information about Otter-λ, this website also presents a number of example input files for Otter-λ (and the corresponding proofs), with commentary, and it also offers the user the chance to run Otter-λ on files of their own preparation as well as on the example files. To look at the example files or run Otter-λ, use the buttons at the top of this page.
What is automated reasoning? This is a general introduction to the subject area, written for the general public. It explains why we want to have computers find proofs, what it is involved in that effort, what's been accomplished in the half century that the field has existed, and what the future might hold. After finishing this introduction, you might want to read the book chapter, The Mechanization of Mathematics, which appeared in . There is also an interesting general introduction by Larry Wos, published in the 1998 Communications of the ACM. Wos describes the approach to automated reasoning taken at Argonne National Laboratory and embodied in the program Otter, on whichOtter-λ has been based. Today, however, there are many other theorem proving programs in existence, and the new ideas in Otter-λ could in principle be added to any of them. I do not want to give the impression that the work on Otter-λ is only useful with Otter. It is just that I wanted to pick some existing prover to add my new ideas to, rather than start over from scratch.
What is lambda logic? Roughly speaking, lambda logic is the union of lambda calculus and first-order logic. It is the logic in which Otter-λ finds proofs. This technical paper is written for people who already have some familiarity with lambda calculus, first-order logic, and unification. It does not discuss automated deduction at all, only the logical theory on which Otter-λ is based.
What is special about Otter-λ? Otter-λ is a first-order theorem prover (Otter) augmented by lambda calculus and an algorithm for untyped lambda unification. That is a way of unifiying terms (or formulas) in lambda logic that allows the creation of terms defining functions (using lambda calculus). This algorithm is what gives Otter-λ more power than Otter. Otter supplies the first-order machinery, and Otter-λ supplements it with lambda unification.
What is lambda unification exactly? This technical note gives the definition in two different ways, first as an algorithm and then as an "inference system", which is a technical tool that researchers in "unification theory" like to use to describe unification algorithms.
Some more specialized topics, needed to understand some of the examples:
Implicit and explicit typing with first-order unification (needed to understand the Algebra examples)
What theorems have been proved using Otter-lambda? Click the View Examples button at the top of this page. Each example has a Commentary file that explains the problem and the proof.
What papers have been written about Otter-lambda? Click the Papers button at the top of this page. Each of the papers can be downloaded.
Two graduate students have helped with this project: Nadia Ghamrawi and Shahin Saadati, both of whom wrote master's theses in the area of automated deduction.
 Alan Turing: Life and Legacy of a Great Thinker , Springer-Verlag, Berlin Heidelberg NewYork, 2003.
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.