/*

This example 
shows how commutation can be eliminated
in the presence of certain ordering constraints
at the expense of explicit inferences with an
ordered variant of symmetry.

Applying that symmetry law
orders negative equations are ordered 
such that the maximal term occurs
on the right side.

The ST-transformation
transforms a=b
into X=a -> X=b


*/


id(X,X).
eq(X,Y) <- id(X,Y).
eq(Z,Y) <- eq(Z,X), eq(Y,X) if [Y>=Z].
eq(X,Y) <- eq(Y,X) if [X>Y].
eq(X,b) <- eq(X,a) if [b>=X].
eq(X,a) <- id(X,b).



precedence([a,b]).
top_predicates_precedence([eq,id]).


:-option([crw_depth(2),memo_constraints(on)]).
:-sama([3]).             % We want saturation by ordered resolution w/o sel.
:-sarp([1-7,10-15]).    % the usual + clausal rewriting  
:-sams([3,19]).         % messages about redundancy proofs by clausal rewrtng.


:-saci([2]).

/*

Saturation terminated.

Persisting Clauses:

    1(1) : id(B,B)
    2(1) : id(B,C) -> eq(B,C)
*   3(1) : eq(B,C),eq(D,C) -> eq(B,D) {[conj([D>=B],[],[])]}
    4(1) : eq(B,C) -> eq(C,B) {[conj([C>B],[],[])]}
    5(1) : eq(B,a) -> eq(B,b) {[conj([b>=B],[],[])]}
    6(1) : id(B,b) -> eq(B,a)
    7(2) : id(B,a) -> eq(B,b) {[conj([b>B],[],[])]}



Total time: 2040 milliseconds

Number of forward inferences: 6
Number of tableau inferences: 0
Number of kept clauses: 6

Equation (7) is redundant but Saturate fails to
see this. 



According to this result,
the STC modification (ST modification with constraints)
should have

A) theory axioms 

A.1) reflexivity
x==y
x==y -> x=y

A.2) ordered symmetry
x=y  -> y=x if y>x
the significance of the latter is to order negative equations

B) the STC modification replaces any positive equation
   a=b with a>b by two clauses

x=a  -> x=b  if b>=x           (*)
x==b -> x=a                    (**)



From ordered resolution inferences
of the form

x==b -> x=a         x=a -> x=c [c>=x]
-------------------------------------
       b==x -> x==c [c>=x]

one again generates 

- if b<c again a clause of the form (*)
- if b>=c a redundant clause of the form (7)

********

no, doesn't work. ordered resolution fails
as one does not produce new equations of the form (*)
without resolving into the commutation law.

*/