Node:Example 1, Next:Example 2, Previous:CLPB Examples, Up:CLPB Examples
| ?- sat(X + Y). sat(X=\=_A*Y#Y) ?
illustrates three facts. First, any accumulated constraints affecting the
top-level variables are displayed as 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.