| ?- 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 ?
yes
| ?- 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.