Basic Elaboration Tolerant logic

% In all my attempts to implement "elaboration tolerant logics"  I find that the only non-defeasible/monotonic inferences I ever can draw upon are based on derivatives from the contrapositive (as in Modus Tollens) of implication.  "Elaboration tolerance" in the sense means tolerate additional rules without *RE*-canonicalizing the previous rules:

First to show what I am labeling as canonicalization:  (this is not SAT so it would be unfair to call this Unit Projection)

Rule1:     (if (and a b) d)  % IKL's "if" is what logicans call implication

% We can show proof of D if we have can show a proof of A and proof of  B
proved_d :- proved_a, proved_b.
% We can show a proof of the falseness of A by showing proof of B and showing proof of the falseness of D
proved_not_a :- proved_not_d, proved_b.
% We can show a proof of the falseness of B by showing proof of A and showing proof of the falseness of D
proved_not_b :- proved_not_d, proved_a.


Rule 2: (if (and a ~b c) d)​

proved_d :- proved_a, proved_not_b, proved_c.
proved_not_a :- proved_not_d, proved_b, proved_c.
proved_not_c :- proved_not_d, proved_b, proved_a.
proved_b :- proved_not_d, proved_a, proved_c.


For "tolerance" let us add (para)consistency:

% We can show proof of D if we *fail* to show proof of ~D
% *and* can show a proof of A and proof of  B
proved_d :- \+ proved_not_d,    proved_a, proved_b.
% We can show a proof of the falseness of A if we have *failed* to show proof of A
% *and* by showing proof of B and showing proof of the falseness of D
proved_not_a :- \+ proved_a, proved_not_d, proved_b.
% We can show a proof of the falseness of B if we have *failed* to show proof of B
% *and* by showing proof of A and showing proof of the falseness of D
proved_not_b :- \+ proved_b, proved_not_d, proved_a.


% Rule 2: ​(if (and a ~b c) d)​

proved_d :- \+ proved_not_d, proved_a, proved_not_b, proved_c.
proved_not_a :- \+ proved_a, proved_not_d, proved_b, proved_c.
proved_not_c :- \+ proved_c, proved_not_d, proved_b, proved_a.
proved_b :- \+ proved_not_b, proved_not_d, proved_a, proved_c.

% So far, realize we should not expect to prove anything *yet*