(18th-August-2020)
• The top-down procedure for the complete knowledge assumption proceeds by negation as failure. It is similar to the top-down definite-clause proof procedure of Figure 5.4. This is a non-deterministic procedure (see the box) that can be implemented by searching over choices that succeed. When a negated atom ∼a is selected, a new proof for atom a is started. If the proof for a fails, ∼a succeeds. If the proof for a succeeds, the algorithm fails and must make other choices. The algorithm is shown in Figure 5.12.
• For example, the clauses from Example 5.28. Suppose the query is ask p. Initially G={p}.
• Using the first rule for p, G becomes { q, ∼r}.
• Selecting q, and replacing it with the body of the third rule, G becomes {∼s, ∼r}.
• It then selects ∼s and starts a proof for s. This proof for s fails, and thus G becomes { ∼r}.
• It then selects ∼r and tries to prove r. In the proof for r, there is the subgoal ∼t, and thus it tries to prove t. This proof for t succeeds. Thus, the proof for ∼t fails and, because there are no more rules for r, the proof for r fails. Thus, the proof for ∼r succeeds.
• G is empty and so it returns yes as the answer to the top-level query.
• Note that this implements finite failure, because it makes no conclusion if the proof procedure does not halt. For example, suppose there is just the rule p←p. The algorithm does not halt for the query ask p. The completion, p↔p, gives no information. Even though there may be a way to conclude that there will never be a proof for p, a sound proof procedure should not conclude ∼p, as it does not follow from the completion.
Comments