Online Otter-λ
-->
Examples
% An element z is called nilpotent if z^n = 0 for some positive integer n.
% Show that 0 is the only nilpotent in a domain.
% This is an ordinary Otter file in which the required instance of induction is given.
% It shows that Otter can do inductive proofs if you give it the right instances of induction.
op(450, xfx, +). % sum
op(350, fy, ~). % minus
op(400, xfx, *). % product
set(knuth_bendix).
set(hyper_res).
set(unit_deletion).
set(factor).
assign(pick_given_ratio,4).
list(sos).
x=x.
% ring axioms
0 + x = x.
x + 0 = x.
~x + x = 0.
x + ~x = 0.
(x + y) + z = x + (y + z).
x + y = y + x.
(x * y) * z = x * (y * z). % product is associative
x * (y + z) = x * y + x * z. % right distributivity
(y + z) * x = y * x + z * x. % left distributivity
x * 1 = x.
1 * x = x.
x * y != 0 | x = 0 | y = 0. % no zero divisors ("domain")
pow(y+1,z) = z * pow(y,z).
pow(1,z) = z.
pow(o,z) = 1. % pow(o,0) included.
end_of_list.
% P(x,y) is pow(x,y) != 0.
% Induction(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]
list(usable).
1 != 0.
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]
b != 0.
end_of_list.
list(sos).
pow(c,b) = 0.
end_of_list.