Online Otter-λ
Examples
Theorem. There are no nilpotents in an integral domain.
An integral domain is a ring with no zero divisors. A nilpotent element is a non-zero element b of the ring such that the n-th power of b, here written pow(n,b), is zero. Proving this is an elementary exercise in mathematical induction; it does occurs as an exercise in Jacobson's textbook on algebra. It is an interesting example because it mixes abstract algebra and induction. Even to formulate it, we need variables for ring elements and variables for natural numbers.
You might think that we should use unary predicates N(x) and R(x) for the natural numbers and the ring. That is not necessary, because of a technique called "implicit typing", explained in detail elsewhere on this website and in Beeson's papers. Roughly speaking, as applied here, it means that
+ and * are operations on the ring, i.e. type(R,+(R,R)) and type(R, *(R,R)), and pow is an operation that takes a number and a ring element
and produces a ring element: type(R, pow(N,R)). These are "implicit" typings because these type expressions are not part of Otter-lambda's input.
The typing of ap is type(Boolean, ap(Pred,N)), where Pred is the type of predicates on natural numbers, i.e. Boolean-valued functions on N.
The typing of the Skolem function g is type(N,g(N,Pred)). The constant 0 is used for the zero element of the ring, and a different symbol o
is used for the natural number o. You will see that the axioms in the input file are correctly typed, i.e. all the axioms use the symbols in accordance with these typings. In fact the proof is also correctly typed, and hence it could be converted to a proof in which unary predicates N(x) and R(x) were used. However, it is much easier to find the proof without the predicates N(x) and R(x); you will note that the input file specifies hyperresolution as a rule of inference, and with unary predicates that will no longer be applicable.
Otter-lambda can find this proof, given only the general form of the induction axiom of Peano Arithmetic. See nilpotent4 for that example.
This example is meant to clarify the contribution of Otter-lambda in inductive proofs. People sometimes say that "Otter can't do induction", but that is not true. If you specifically tell it the instance of induction to use, and give it the clausal form of that instance of induction, it can do induction. We demonstrate that in this example.
The integral domain axioms that are used in the proof are the first two lines:
27 [] 1!=0.
28 [] x*y!=0|x=0|y=0.
The axioms use s(x) for the successor of x, and
the n-th power of x, pow(n,x), is recursively
defined:
30,29 [] pow(s(x),y)=y*pow(x,y).
32,31 [] pow(o,x)=1.
Note that the zero element of the ring is written 0, while the natural number zero is written o. That is done to ensure that the axioms are "implicitly typed". When Otter-lambda (or Otter itself) puts two equation numbers on a line, it's because it has added a copy of the equation as a new demodulator, which will be used to rewrite future conclusions before saving them.
For Otter we can specify a particular predicate P(u,x) that we want to prove by induction on u.
Induction for P is -P(o,y) | all(x,(P(x,y) & -P(x+1,y)) | P(z,y).
Bringing induction to clausal form we have (using a Skolem function g)
-P(o,u) | P(g(u,z),u) | P(z,u). [1]
-P(o,u) | -P(g(u,z)+1,u) | P(z,u). [2]
In our case P(u,x) is pow(u,x) != 0. We get
pow(o,u) = 0 | pow(g(u,z),u) != 0 | pow(z,u) != 0. % This is [1]
pow(o,u) = 0 | pow(g(u,z)+1,u) = 0 | pow(z,u) != 0. % This is [2]
Finally we have the negation of the goal:
b!=0.
pow(n,b)=0.
This explains the input file nilpotent3.in. The proof from this file is straighforward, and can be found by either Otter-lambda or by unmodified Otter. Compare this with the example nilpotent4.in, in which Otter-lambda is just given the induction schema, rather than the particular instance of induction, and finds the correct instance by itself, using lambda unification.