Online Otter-λ

Examples

Sum of the first n integers

This is the famous problem that Gauss supposedly solved at age 12: The sum of 0 + 1 + 2 + ... + n is n(n+1)/2. It is a classical exercise in mathematical induction, but the induction step requires some elementary algebra. To formulate this as a problem about integers, we put the 2 on the other side of the equation, so that what has to be proved is 2 sum(i,i,0,n) = n(n+1).

So before we get to the algebra, we will have to break up the sum up to n+1 into the sum up to n and the last term, then distribute the 2. At that point algebra is required to show that (n-1)n +2( n+1) = n(n+1). This step is carried out by external simplification (for which Otter-lambda uses MathXpert's code).

Note that "sum" is, in Otter-lambda, a functional, applying to functions from natural numbers to natural numbers, so in Otter-lambda we have

sum(lambda(k,k),0,n))

instead of the term sum(k,k,0,n) with which MathXpert works. There is a translation module that passes terms back and forth (in their string representations) from Otter-lambda to MathXpert; it has to make conversions such as this. At present "lambda" is the only binding operator in Otter-lambda, and the only operator to which lambda-unification is applied, so indexed sums, definite integrals, sets, etc. must be expressed using lambda.

Here is the proof that Otter-lambda finds, with the Skolem term g(lambda(y,2*sum(z,z,0,y))) replaced by a constant c for readability:

2 [] sum(u,v,x,x)=Ap(lambda(u,v),x).
4 [] sum(u,v,x,y+1)=sum(u,v,x,y)+Ap(lambda(u,v),1+y).
7 [] x+1!=y+1|x=y.
8 [] -Ap(y,0)|Ap(y,g(y))|Ap(y,z).
9 [] -Ap(y,0)| -Ap(y,g(y)+1)|Ap(y,z).
10 [] 2*sum(x,x,0,n)!=n* (n+1).
11 [binary,10,9,demod,beta,2,beta,beta,4,beta,simplify] 2* (sum(x,x,0,c)+1+c)!= (1+c)* (2+c).
12 [binary,10,8,demod,beta,2,beta,beta,simplify] 2*sum(x,x,0,c)= (1+c)*c..
22 [binary,11,7,simplify] 2*c+2*sum(x,x,0,c)!=3*c+c^2.
29 [para_into,22,12,simplify] $F.

The proof begins with a bang at step 11, where in one step, lambda unification has identified the induction step to be proved, expanded "sum" using its definition in terms of lambda, and broken up the sum to n+1 into the sum to n and the last term. Note that, since this is a resolution proof, the equality to be proved occurs negated, so that the final result should be a contradiction. Similarly, in line 12 the induction hypothesis is identified. In step 22, the distributive law is used several times by simplification, and c*c is made into c^2. Then we are in a position to use the induction hypothesis (by paramodulation from 12 into 22), and then simplification easily verifies the desired equality. Since that desired equality was negated, the penultimate form of the inequality is of the form x != x for some term x, which resolves with the equality axiom x=x to yield a contradiction.