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