Information Technology Reference
In-Depth Information
copy_term predicate. (It uses a parameter N to decide how many copies to make.) It
then uses the predicate nopick to confirm that there is no way to pick a literal from
each dclause in the resulting list. Below the dashed line in the figure, the estunsat
predicate is like the estsat predicate in figure 11.14 except that it uses the success of
unsat rather than the failure of sat to do all the hard work:
?- estunsat(1, [[p(a)],[not(p(X)),q(X)]], [q(a)])
Yes
?- estunsat(1, [[p(a)],[not(p(X)),q(X)]], [q(b)])
No
Note that for some queries it is necessary to use a parameter N >
1:
?- unsat(1, [[not(p(a)),not(p(b))],[p(X)]]).
% Wrong.
No
?- unsat(2, [[not(p(a)),not(p(b))],[p(X)]]).
% Right.
Yes
Unfortunately, there is no way to know in advance how large a value of N will be
needed to obtain the correct answer.
With a first-order language, more advanced reasoning problems can be handled.
Consider the following puzzle (a generalized version was discussed in section 4.4):
There are three blocks, A, B, C, in a stack, with the top one (A) green
and the bottom one (C) not green.
Is there a green block directly on top of a non-green one?
It is clear that the answer must be yes. If B is green, then it is a green one directly on
a non-green one (C); if, on the other hand, B is not green, then the top block (A) is a
green one directly on a non-green one (B). Either way, the conclusion follows.
What makes this puzzle challenging is that we know there has to be a green block
directly on top of a non-green one, and yet we cannot say which one it is. With back-
chaining, whenever it was known that something had a property, enough information
was always given to figure out what that something was. First-order reasoning using
estunsat is more general and does not have this limitation:
?- estunsat(2,
[ [on(a,b)], [on(b,c)], % The facts
[green(a)], [not(green(c))] ], % More facts
[ on(X,Y), green(X), not(green(Y))] ). % The query
Yes
 
Search WWH ::




Custom Search