Intelligence 2E

foundations of computational agents

The third edition of Artificial Intelligence: foundations of computational agents, Cambridge University Press, 2023 is now available (including full text).

The bottom-up procedure for negation as failure is a modification of the bottom-up procedure for definite clauses. The difference is that it can add literals of the form $\sim p$ to the set $C$ of consequences that have been derived; $\sim p$ is added to $C$ when it can determine that $p$ must fail.

Failure can be defined recursively: $p$ fails when every body of a clause with $p$ as the head fails. A body fails if one of the literals in the body fails. An atom ${b}_{i}$ in a body fails if $\sim {b}_{i}$ can be derived. A negation $\sim {b}_{i}$ in a body fails if ${b}_{i}$ can be derived.

Figure 5.11 gives a bottom-up negation-as-failure interpreter for computing consequents of a ground KB. Note that this includes the case of a clause with an empty body (in which case $m=0$, and the atom at the head is added to $C$) and the case of an atom that does not appear in the head of any clause (in which case its negation is added to $C$).

Consider the following clauses:

${p}{\leftarrow}{}{q}{\wedge}{\mathrm{\sim}}{}{r}{.}$ | ||

${p}{\leftarrow}{}{s}{.}$ | ||

${q}{\leftarrow}{\mathrm{\sim}}{}{s}{.}$ | ||

${r}{\leftarrow}{\mathrm{\sim}}{}{t}{.}$ | ||

${t}{.}$ | ||

${s}{\leftarrow}{}{w}{.}$ |

The following is a possible sequence of literals added to ${C}$:

${t}$ | ||

${\sim}{r}$ | ||

${\sim}{w}$ | ||

${\sim}{s}$ | ||

${q}$ | ||

${p}$ |

where ${t}$ is derived trivially because it is given as an atomic clause; ${\mathrm{\sim}}{r}$ is derived because ${t}{\mathrm{\in}}{C}$; ${\mathrm{\sim}}{w}$ is derived as there are no clauses for ${w}$, and so the “for every clause” condition of line 18 of Figure 5.11 trivially holds. Literal ${\mathrm{\sim}}{s}$ is derived as ${\mathrm{\sim}}{w}{\mathrm{\in}}{C}$; and ${q}$ and ${p}$ are derived as the bodies are all proved.

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 $\sim a$ is selected, a new proof for atom $a$ is started. If the proof for $a$ fails, $\sim a$ succeeds. If the proof for $a$ succeeds, the algorithm fails and must make other choices. The algorithm is shown in Figure 5.12.

Consider the clauses from Example 5.31. Suppose the query is ${\text{\U0001d5ba\U0001d5cc\U0001d5c4}}{\mathit{\text{}}}{\mathit{}}{p}$.

Initially, ${G}{\mathrm{=}}{\mathrm{\{}}{p}{\mathrm{\}}}$.

Using the first rule for ${p}$, ${G}$ becomes ${\mathrm{\{}}{q}{\mathrm{,}}{\mathrm{\sim}}{r}{\mathrm{\}}}$.

Selecting ${q}$, and replacing it with the body of the third rule, ${G}$ becomes ${\mathrm{\{}}{\mathrm{\sim}}{s}{\mathrm{,}}{\mathrm{\sim}}{r}{\mathrm{\}}}$.

It then selects ${\mathrm{\sim}}{s}$ and starts a proof for ${s}$. This proof for ${s}$ fails, and thus ${G}$ becomes ${\mathrm{\{}}{\mathrm{\sim}}{r}{\mathrm{\}}}$.

It then selects ${\mathrm{\sim}}{r}$ and tries to prove ${r}$. In the proof for ${r}$, there is the subgoal ${\mathrm{\sim}}{t}$, and so it tries to prove ${t}$. This proof for ${t}$ succeeds. Thus, the proof for ${\mathrm{\sim}}{t}$ fails and, because there are no more rules for ${r}$, the proof for ${r}$ fails. Therefore, the proof for ${\mathrm{\sim}}{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\leftarrow p$. The algorithm does not halt for the query $\text{\U0001d5ba\U0001d5cc\U0001d5c4}\text{}p$. The completion, $p\iff 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 $\sim p$, as it does not follow from the completion.