10.37.3.2 Isolation Axioms

These axioms are used to rewrite equations such that the variable to be solved for is moved to the left hand side and the result of the evaluation of the right hand side can be assigned to the variable. This allows, for example, to use the exponentiation operator for the computation of roots and logarithms; see below.

A = B * C

Residuates unless B or C is ground or A and B or C are ground.

A = B / C

Residuates unless C is ground or A and B are ground.

X = min(Y,Z)

Residuates unless Y and Z are ground.

X = max(Y,Z)

Residuates unless Y and Z are ground.

X = abs(Y)

Residuates unless Y is ground.

X = pow(Y,Z), X = exp(Y,Z)

Residuates unless any pair of two of the three variables is ground. Example:

          
          clp(r) ?- { 12=pow(2,X) }.
          
          X = 3.5849625007211565
          
          clp(r) ?- { 12=pow(X,3.585) }.
          
          X = 1.9999854993443926
          
          clp(r) ?- { X=pow(2,3.585) }.
          
          X = 12.000311914286545

X = sin(Y)

Residuates unless X or Y is ground. Example:

          
          clp(r) ?- { 1/2 = sin(X) }.
          
          X = 0.5235987755982989

X = cos(Y)

Residuates unless X or Y is ground.

X = tan(Y)

Residuates unless X or Y is ground.