Information Technology Reference
In-Depth Information
Figure 11.14.
Entailment using satisfiability
estsat.pl
% Dclauses DL entails Q using sat (defined elsewhere).
estsat(DL,Q) :- negs(Q,NQ), \+ sat([NQ|DL],_).
% negs(Q,NQ): NQ is the negation of the literals in Q.
negs([],[]).
negs([not(A)|T],[A|NT]) :- negs(T,NT).
negs([A|T],[not(A)|NT]) :- \+ A=not(_), negs(T,NT).
?- estsat([[a,b,c],[not(a),b],[a,not(c)]], [b]).
Yes
?- estsat([[a,b,c],[not(a),b],[a,not(c)]], [c]).
No
The given facts entail that Bob is guilty, but they do not entail the guilt (or innocence)
of Alice or Carol.
The
back-chaining
examples
shown
in
figure
11.2
can
be
repeated
with
the
conditionals translated into dclauses:
?- estsat([[a],[b],[u,not(p),not(b)],[p,not(a)]], [b,a]).
Yes
?- estsat([[a],[b],[u,not(p),not(b)],[p,not(a)]], [u]).
Yes
?- estsat([[a],[b],[u,not(p),not(b)],[p,not(a)]], [p,d]).
No
Of course, the way these queries are answered (using the
sat
predicate) is very
different from the back-chaining method used until now.
11.4.5 First-order reasoning
∗
When a propositional language is enlarged to include variables, it is usually called
a
first-order language
. Reasoning correctly with a first-order language is much more
complicated than what has been done so far. For satisfiability, it is no longer sufficient
to pick a literal from every dclause; a literal must be picked from every dclause for
every value of the variables in that dclause.
For example, the formula
[[not(p(a))],[not(q(b))],[p(X),q(X)]]
is consid-
ered to be satisfiable, since
q(X)
can be chosen when
X
is
a
, and
p(X)
otherwise.
But the formula
[[not(p(a))],[not(q(a))],[p(X),q(X)]]
is unsatisfiable,
since
