Online Otter-λ
-->
Examples
% test file for second-order unification
% quantificational logic
set(lambda).
set(demod_inf).
set(hyper_res).
set(binary_res).
%set(very_verbose).
assign(max_distinct_vars,6).
assign(max_weight,32).
assign(pick_given_ratio,4).
weight_list(pick_and_purge).
weight(junk,50).
weight(cases($(1),$(1),$(1),$(1)), 50).
end_of_list.
% typings:
% The types are: PF (propositional function), prop (proposition), var, and obj (object)
% PF lambda(var, prop)
% prop all(PF)
% bool P(prop)
% prop i(prop,prop)
% prop n(prop)
% prop Ap(PF, obj)
% bool notfree(var,prop)
% bool notfree2(var, PF)
list(usable).
x=x.
%P(i(n(x),i(x,y))). % for the intuitionistic system.
%-P(i(x,ap(y,z))) | -notfree(z,x) | P(i(x,all(y))). % y is a functional lambda(z,Ap(a,z)).
%P(i(all(z),ap(z,y))).
% to permit working backwards:
%-notfree(z,x) | z != gensym.
% to permit working forwards:
%notfree(z,i(x,y)) | -notfree(z,x) | -notfree(z,y).
%notfree(z,n(x)) | -notfree(z,x).
%notfree(z,Ap(y,x)) | -notfree(z,x) | -notfree2(z,y).
%notfree2(z,lambda(u,v)) | u!=z | -notfree(z,v).
end_of_list.
list(demodulators).
n(n(x)) = junk.
n(junk)= junk.
i(x,junk) = junk.
i(junk,x)= junk.
P(junk) = junk.
%cases(x,y,z,z) = z.
%cases(x,x,u,v) = u.
end_of_list.
list(sos).
-P(x) | -P(i(x,y)) | P(y). % condensed detachment
% axioms from Kleene IM p. 82
P(i(x,i(y,x))).
P(i(i(x,y),i(i(x,i(y,z)),i(x,z)))).
P(i(i(x,y),i(i(x,n(y)),n(x)))).
P(i(n(n(x)),x)). %for the classical system
%-P(i(z,y)) | -notfree(x,z) | P(i(z,all(lambda(x,y)))).
P(i(all(lambda(x,Ap(y,x))), Ap(y,z))).
P(Ap(a,c)).
-P(n(all(lambda(x,n(Ap(a,x)))))).
end_of_list.