Online Otter-λ
-->
Examples
% test file for second-order unification
% quantificational logic using the axioms from Kleene's Introduction to Metamathematics
% note use of "junk" to discard double negations as they are deduced.
set(lambda).
set(demod_inf).
set(hyper_res).
set(ur_res). % Without this it doesn't find a proof, or at least not quickly.
assign(max_distinct_vars,3).
assign(max_weight,18).
assign(pick_given_ratio,2).
assign(max_proofs,1).
weight_list(pick_and_purge).
weight(junk,50).
end_of_list.
% implicit typings are as follows. See quantifiers8.in for explicit use of types in this problem.
% 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).
-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(n(x),i(x,y))). % for the intuitionistic system.
P(i(u,u)). % not part of Kleene's axioms; given extra in this file.
P(i( i(n(x),n(y)), i(y,x))).
P(i( i(x,y), i(n(y),n(x)))).
P(i(all(lambda(x,Ap(y,x))), Ap(y,z))).
end_of_list.
list(demodulators).
n(n(x)) = junk.
i(i(i(x,y),z),w) = junk.
n(junk)= junk.
i(x,junk) = junk.
i(junk,x)= junk.
P(junk) = junk.
end_of_list.
list(sos).
P(Ap(a,c)).
-P(n(all(lambda(x,n(Ap(a,x)))))).
end_of_list.