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 file shows that Otter-lambda can use lambda-unification to find the required instance of induction.
op(450, xfx, +). % sum
op(350, fy, ~). % minus
op(400, xfx, *). % product
set(lambda).
set(induction).
set(hyper_res).
set(binary_res).
set(knuth_bendix).
assign(max_weight,32).
assign(pick_given_ratio,4).
%Typings: R +(R,R)
% R *(R,R)
% R^ inv(R) where R^ means R union "undefined"
% R pow(N,R)
% Prop ap(PF,N).
% PF lambda(N,Prop).
% i.e. all propositional functions take integer variables
list(usable).
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.
one * x = x.
x = 0 | x * inv(x) = 1.
x = 0 | inv(x) * x = one.
1 != 0.
x * y != 0 | x = 0 | y = 0. % no zero divisors ("integral domain")
pow(s(y),z) = z * pow(y,z).
pow(o,z) = 1.
%axioms for natural numbers. Use lower case o for 0 to preserve typing. s is successor, p is predecessor.
x = o | x = s(p(x)). % every nonzero number is the successor of its predecessor.
ap(y,o) | -ap(y,g(z,y)) | -ap(y,z). % These two are the clausal form of mathematical induction
ap(y,o) | ap(y,s(g(z,y))) | -ap(y,z).
b != 0.
end_of_list.
list(sos).
pow(n,b) = 0. % The negated goal
end_of_list.