1% The sentential calculus (CN). 2% 3% {CN1, CN2, CN3} (Lukasiewicz), along with condensed detachment, 4% axiomatizes the sentential calculus (the classical propositional calculus). 5% 6% Show that CN16, CN18, and CN19 can be derived. 7 8set(hyper_res). 9clear(back_sub). 10assign(pick_given_ratio, 3). 11assign(max_proofs, 3). 12assign(max_weight, 16). 13clear(print_kept). 14set(order_history). 15 16assign(max_mem, 1500). % 1.5 Megabytes 17 18% The symbols -> and - have built-in declarations, and they are used for 19% clauses and formulas. When redeclaring them for use with terms, we 20% must be careful that they will still work for clauses and formulas. 21 22op(800, yfx, ->). % left association 23 24list(usable). 25-P(x -> y) | -P(x) | P(y). % condensed detachment 26end_of_list. 27 28list(sos). 29P(x -> y -> (y -> z -> (x -> z))). % CN1 30P(-x -> x -> x). % CN2 31P(x -> (-x -> y)). % CN3 32end_of_list. 33 34list(passive). 35-P(a -> a) | $Ans(CN_16). 36-P(b -> (a -> b)) | $Ans(CN_18). 37-P(a -> b -> c -> (b -> c)) | $Ans(CN_19). 38end_of_list. 39 40