Please explain in a brief note, showing the query and the
result.
Using programs (sat . pl) and (estsat .
pl) from Chapter 11 of the
Levesque textbook, show the proof of the following
:
q is a logical consequence of the clause set { -p, -p V -q, p V
q } . (Here "-" denotes negation)
(Book name: Thinking as Computation: A First Course by Hector J.
Levesque (MIT Press), 2017, ISBN-13: 978-0262534741)
=============================================
- This Question Is Based On The Prolog Language Please Explain In A Brief Note Showing The Query And The Result Using P 1 (20.41 KiB) Viewed 38 times
- This Question Is Based On The Prolog Language Please Explain In A Brief Note Showing The Query And The Result Using P 2 (64.06 KiB) Viewed 38 times
- This Question Is Based On The Prolog Language Please Explain In A Brief Note Showing The Query And The Result Using P 3 (37.33 KiB) Viewed 38 times
Case Study: Other Ways of Thinking 261 sat.pl Figure 11.13. A satisfiability program % The dclauses in DL are satisfied by picking Lits. sat (DL, Lits) :- satpick (DL,[],Lits). % satpick (L.P.Lits): the dclauses in Il can be satisfied by % picking the literals in Lits, given that those in P are taken. satpick ([1,P.P). satpick([D|DL], P1, Lits) :- pickone (D,P1,P2), satpick (DL, P2, Lits). pickone([L_],P.P) :- member (L,P). *L is picked. pickone([L_],P,[LP]) :- \+ member_neg (L,P). % 'l is not picked. pickone (LID),P,P2) :- pickone (D,P.P2). * Use D instead. member_neg (A.P) :- member(not(A),P). member_neg (not (A),P) :- member CA,P). The predicate member_neg is used to check if the negation of a literal has already been picked. It does this by either adding or removing a not on the given literal. It is not hard to confirm that this predicate does the right thing: ?- sat([[P], [not(p),not(a)). [not(Q)]],). L = [not(q). p] Yes ?- sat([[p], [not(p),not(].[9]],L). No ?- sat([[p.a), [not(p).2). [not(q).p], [not (p).not(0]],-). No 11.4.4 Logical entailment reconsidered The notion of logical entailment can now be enlarged to deal with knowledge bases that are lists of dclauses. Continue to assume that there are no variables in the dclauses, and for simplicity, that the queries are as before, a list of atoms or their negations, all of which are to be established. It is then easy to do logical entailment: negate the literals in the query and let the sat predicate do the heavy lifting, as shown in figure 11.14 With this procedure, one can go beyond what was possible with back-chaining. For example, the puzzle with Alice, Bob, and Carol can now be solved: ?- estsat([[a,b,c), [not(a),b], [a,not(0]][a]). NO
estsat.pl Figure 11.14. Entailment using satisfiability * Dclauses DL entails Q using sat (defined elsewhere). estsat (DL.Q :- negs (Q,NQ), I+ sat([NQ|DL]..). % negs (0,00): NQ is the negation of the literals in Q. negs([],[]). negs([not CAT].[AINT]) :- negs(T,NT). negs([A]T], [not(A) INT]) :- \+ A=noto, negs (T,NT). ?- estsat([[a,b,c], [not(a),b],[a, noto]], ). 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 conditional translated into dclauses: ?- estsat([[a], , [u,not (p),not(b)],[p.not(a)]], [b,a]). Yes ?- estsat([[a], , [u, not(p),not(b)]. [p,not(a)]], ). Yes ?- estsat([[a],. [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.