10.36.3.1 Example 1
     | ?- sat(X + Y).
     
     sat(X=\=_A*Y#Y)

illustrates three facts. First, any accumulated constraints affecting the top-level variables are displayed floundered goals, since the query is not true for all X and Y. Secondly, accumulated constraints are displayed as sat(V=:=Expr) or sat(V=\=Expr) where V is a variable and Expr is a “polynomial”, i.e. an exclusive or of conjunctions of variables and constants. Thirdly, _A had to be introduced as an artificial variable, since Y cannot be expressed as a function of X. That is, X + Y is true iff there exists an _A such that X=\=_A*Y#Y. Let's check it!

     | ?- taut(_A ^ (X=\=_A*Y#Y) =:= X + Y, T).
     
     T = 1

verifies the above answer. Notice that the formula in this query is a tautology, and so it is entailed by an empty set of constraints.


Send feedback on this subject.