Node:Example 2, Next:Example 3, Previous:Example 1, Up:CLPB Examples

Example 2

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