| ?- taut(A =< C, T).
no
| ?- sat(A =< B), sat(B =< C), taut(A =< C, T).
T = 1,
sat(A=:=_A*_B*C),
sat(B=:=_B*C)
| ?- taut(a, T).
T = 0
| ?- taut(~a, T).
T = 0
illustrates the entailment predicate. In the first query,
the expression “A implies C” is neither known to be true nor false, so
the query fails. In the second query, the system is told
that “A implies B” and “B implies C”, so “A implies C” is
entailed. The expressions in the third and fourth queries are to
be read “for each a, a is true” and “for each a, a is false”,
respectively, and so T = 0 in both cases since both are
unsatisfiable. This illustrates the fact that the implicit universal
quantifiers introduced by symbolic constants are placed in front of the
entire expression.