Forward Chaining algorithm: Horn Clause(Fig 7.14 pseudocode): Note: If this info

Question

Forward Chaining algorithm:

Horn Clause(Fig 7.14 pseudocode):

Note: If this info isn't enough, then you can also google about it, anything that can help you out. Thanks.

function PL-FC-ENTAILS?(KB, q) returns true or false inputs: KB, the knowledge base, a set of propositional definite clauses g, the query, a proposition symbol count a table, where count [c] is the number of symbols in c's premise inferred a table, where inferred[s] is initially false for all symbols agenda a queue of symbols, initially symbols known to be true in KB while agenda is not empty do p POP( agenda) if p = q then return true if inferredlp]-false then inferred[p] true for each clause c in KB where p is in c.PREMISE do decrement count[c] if count[c] 0 then add c.CONCLUSION to agenda return false Figure 7.15 The forward-chaining algorithm for propositional logic. The agenda keeps track of symbols known to be true but not yet "processed." The count table keeps track of how many premises of each implication are as yet unknown. Whenever a new symbol p from the agenda is processed, the count is reduced by one for each implication in whose premise p appears (easily identified in constant time with appropriate indexing.) If a count reaches zero, all the premises of the implication are known, so its conclusion can be added to the agenda. Finally, we need to keep track of which symbols have been processed; a symbol that is already in the set of inferred symbols need not be added to the agenda again. This avoids redundant work and prevents loops caused by implications such as Q and Q P

Explanation / Answer

A Horn clause is a clause with at most one positive literal.

Any Horn clause therefore belongs to one of four categories:

Now, if resolution is restricted to Horn clauses, some interesting properties appear. Some of these are evident; others I will just state and you can take on faith.

I. If you resolve Horn clauses A and B to get clause C, then the positive literal of A will resolve against a negative literal in B, so the only positive literal left in C is the one from B (if any). Thus, the resolvent of two Horn clauses is a Horn clause.

II. If you resolve a negated goal G against a fact or rule A to get clause C, the positive literal in A resolves against a negative literal in G. Thus C has no positive literal, and thus is either a negated goal or the null clause.

III. Therefore: Suppose you are trying to prove Phi from Gamma, where ~Phi is a negated goal, and Gamma is a knowledge base of facts and rules. Suppose you use the set of support strategy, in which no resolution ever involves resolving two clauses from Gamma together. Then, inductively, every resolution combines a negated goal with a fact or rule from Gamma and generates a new negated goal. Moreover, if you take a resolution proof, and trace your way back from the null clause at the end to ~Phi at the beginning, since every resolution involves combining one negated goal with one clause from Gamma, it is clear that the sequence of negated goals involved can be linearly ordered. That is, the final proof, ignoring dead ends has the form

IV. Therefore, the process of generating the null clause can be viewed as a state space search where:

V. Moreover, it turns out that it doesn't really matter which literal in P you choose to resolve. All the literals in P will have to be resolved away eventually, and the order doesn't really matter. (This takes a little work to prove or even to state precisely, but if you work through a few examples, it becomes reasonably evident.)

Backward Chaining

Putting all the above together, we formulate the following non-deterministic algorithm for resolution in Horn theories. This is known as backward chaining.

If bc(~Phi,Gamma) succeeds, then Phi is a consequence of Gamma; if it fails, then Phi is not a consequence of Gamma.

Moreover: Suppose that Phi contains existentially quantified variables. As remarked above, when ~Phi is Skolemized, these become free variables. If you keep track of the successive bindings through the successful path of resolution, then the final bindings of these variables gives you a value for these variables; all proofs in Horn theories are constructive (assuming that function symbols in Gamma are constructive.) Thus the attempt to prove a statement like "exists(X,Y) p(X,Y)^q(X,Y)" can be interpreted as " Find X and Y such that p(X,Y) and q(X,Y)."

The succcessive negated goals Pi can be viewed as negations of subgoals of Phi. Thus, the operation of resolving ~P against C to get ~Q can be interpreted, "One way to prove P would be to prove Q and then use C to infer P". For instance, suppose P is "mortal(socrates)," C is "man(X) => mortal(X)" and Q is "man(socrates)." Then the step of resolving ~P against C to get ~Q can be viewed as, "One way to prove mortal(socrates) would to prove man(socrates) and then combine that with C."

Propositional Horn theories can be decided in polynomial time. First-order Horn theories are only semi-decidable, but in practice, resolution over Horn theories runs much more efficiently than resolution over general first-order theories, because of the much restricted search space used in the above algorithm.

Backward chaining is complete for Horn clauses. If Phi is a consequence of Gamma, then there is a backward-chaining proof of Phi from Gamma.

Related Questions

Navigate

• Browse (All)
• Browse F
• Subjects

---

---

Integrity-first tutoring: explanations and feedback only — we do not complete graded work. Learn more.