1% Equivalential calculus (EC): YQL is a single axiom. 2% 3% {EC1, EC2} (Lesniewski) was the first axiomatization of EC. 4% Show that EC1 and EC2 can be derived from YQL by condensed detachment. 5 6set(hyper_res). 7assign(pick_given_ratio,3). 8clear(back_sub). 9assign(max_proofs,2). 10assign(max_weight, 16). 11clear(print_kept). 12set(order_history). 13 14list(usable). 15-P(e(x,y)) | -P(x) | P(y). % condensed detachment 16end_of_list. 17 18list(sos). 19P(e(e(x,y),e(e(z,y),e(x,z)))). % YQL 20end_of_list. 21 22list(passive). 23-P(e(e(e(a,b),e(c,a)),e(b,c))) | $Ans(EC_1). 24-P(e(e(a,e(b,c)),e(e(a,b),c))) | $Ans(EC_2). 25end_of_list. 26 27% The following demodulators discard clauses that contain an 28% instance of e(x,x) as a proper subformula. 29 30list(demodulators). 31e(e(x,x),y) = junk. 32e(y,e(x,x)) = junk. 33e(x,junk) = junk. 34e(junk,x) = junk. 35P(junk) = $T. 36end_of_list. 37 38% For reference, the 13 shortest single axioms for EC: 39% 40% P(e(e(x,y),e(e(z,y),e(x,z)))). % YQL % Lukasiewicz P1 41% P(e(e(x,y),e(e(x,z),e(z,y)))). % YQF % Lukasiewicz P2 42% P(e(e(x,y),e(e(z,x),e(y,z)))). % YQJ % Lukasiewicz P3 43% P(e(e(e(x,y),z),e(y,e(z,x)))). % UM % Meredith P4 = P4' 44% P(e(x,e(e(y,e(x,z)),e(z,y)))). % XGF % Meredith P5 45% P(e(e(x,e(y,z)),e(z,e(x,y)))). % WN % Meredith P7 46% P(e(e(x,y),e(z,e(e(y,z),x)))). % YRM % Meredith P8 47% P(e(e(x,y),e(z,e(e(z,y),x)))). % YRO % Meredith P9 48% P(e(e(e(x,e(y,z)),z),e(y,x))). % PYO % Meredith P10 = P9' 49% P(e(e(e(x,e(y,z)),y),e(z,x))). % PYM % Meredith P11 = P8' 50% P(e(x,e(e(y,e(z,x)),e(z,y)))). % XGK % Kalman 51% P(e(x,e(e(y,z),e(e(x,z),y)))). % XHK % Winker 52% P(e(x,e(e(y,z),e(e(z,x),y)))). % XHN % Winker 53