Intelligence 2E

foundations of computational agents

The definite clause language does not allow a contradiction to be stated. However, a simple expansion of the language can allow proof by contradiction.

An integrity constraint is a clause of the form

$\text{false}\leftarrow {a}_{1}\wedge \mathrm{\dots}\wedge {a}_{k}.$ |

where the ${a}_{i}$ are atoms and false is a special atom that is false in all interpretations.

A Horn clause is either a definite clause or an integrity constraint. That is, a Horn clause has either false or a normal atom as its head.

Integrity constraints allow the system to prove that some conjunction of atoms is false in all models of a knowledge base. Recall that $\mathrm{\neg}p$ is the negation of $p$, which is true in an interpretation when $p$ is false in that interpretation, and $p\vee q$ is the disjunction of $p$ and $q$, which is true in an interpretation if $p$ is true or $q$ is true or both are true in the interpretation. The integrity constraint $\text{false}\leftarrow {a}_{1}\wedge \mathrm{\dots}\wedge {a}_{k}$ is logically equivalent to $\mathrm{\neg}{a}_{1}\vee \mathrm{\dots}\vee \mathrm{\neg}{a}_{k}$.

A Horn clause knowledge base can imply negations of atoms, as shown in Example 5.19.

Consider the knowledge base ${{\text{\mathit{K}\mathit{B}}}}_{{\mathrm{1}}}$:

${\text{\mathit{f}\mathit{a}\mathit{l}\mathit{s}\mathit{e}}}{\leftarrow}{}{a}{\wedge}{}{b}{.}$ | ||

${a}{\leftarrow}{}{c}{.}$ | ||

${b}{\leftarrow}{}{c}{.}$ |

The atom ${c}$ is false in all models of ${{\text{\mathit{K}\mathit{B}}}}_{{\mathrm{1}}}$. To see this, suppose instead that ${c}$ is true in model ${I}$ of ${{\text{\mathit{K}\mathit{B}}}}_{{\mathrm{1}}}$. Then ${a}$ and ${b}$ would both be true in ${I}$ (otherwise ${I}$ would not be a model of ${{\text{\mathit{K}\mathit{B}}}}_{{\mathrm{1}}}$). Because false is false in ${I}$ and ${a}$ and ${b}$ are true in ${I}$, the first clause is false in ${I}$, a contradiction to ${I}$ being a model of ${{\text{\mathit{K}\mathit{B}}}}_{{\mathrm{1}}}$. Thus ${\mathrm{\neg}}{\mathit{}}{c}$ is true in all models of ${{\text{\mathit{K}\mathit{B}}}}_{{\mathrm{1}}}$, which can be written as

${{\text{\mathit{K}\mathit{B}}}}_{{1}}{\vDash}{\mathrm{\neg}}{}{c}$ |

Although the language of Horn clauses does not allow disjunctions and negations to be input, disjunctions of negations of atoms can be derived, as the following example shows.

Consider the knowledge base ${{\text{\mathit{K}\mathit{B}}}}_{{\mathrm{2}}}$:

${\text{\mathit{f}\mathit{a}\mathit{l}\mathit{s}\mathit{e}}}{\leftarrow}{}{a}{\wedge}{}{b}{.}$ | ||

${a}{\leftarrow}{}{c}{.}$ | ||

${b}{\leftarrow}{}{d}{.}$ | ||

${b}{\leftarrow}{}{e}{.}$ |

Either ${c}$ is false or ${d}$ is false in every model of ${{\text{\mathit{K}\mathit{B}}}}_{{\mathrm{2}}}$. If they were both true in some model ${I}$ of ${{\text{\mathit{K}\mathit{B}}}}_{{\mathrm{2}}}$, both ${a}$ and ${b}$ would be true in ${I}$, so the first clause would be false in ${I}$, a contradiction to ${I}$ being a model of ${{\text{\mathit{K}\mathit{B}}}}_{{\mathrm{2}}}$. Similarly, either ${c}$ is false or ${e}$ is false in every model of ${{\text{\mathit{K}\mathit{B}}}}_{{\mathrm{2}}}$. Thus,

${{\text{\mathit{K}\mathit{B}}}}_{{2}}{\vDash}{\mathrm{\neg}}{}{c}{\vee}{\mathrm{\neg}}{}{d}$ | ||

${{\text{\mathit{K}\mathit{B}}}}_{{2}}{\vDash}{\mathrm{\neg}}{}{c}{\vee}{\mathrm{\neg}}{}{e}{.}$ |

A set of clauses is unsatisfiable if it has no models. A set of clauses is provably inconsistent with respect to a proof procedure if false can be derived from the clauses using that proof procedure. If a proof procedure is sound and complete, a set of clauses is provably inconsistent if and only if it is unsatisfiable.

It is always possible to find a model for a set of definite clauses. The interpretation with all atoms true is a model of any set of definite clauses. Thus, a definite-clause knowledge base is always satisfiable. However, a set of Horn clauses can be unsatisfiable.

The set of clauses ${\mathrm{\{}}{a}{\mathrm{,}}{\text{\mathit{f}\mathit{a}\mathit{l}\mathit{s}\mathit{e}}}{\mathrm{\leftarrow}}{\mathit{}}{a}{\mathrm{\}}}$ is unsatisfiable. There is no interpretation that satisfies both clauses. Both ${a}$ and ${\text{\mathit{f}\mathit{a}\mathit{l}\mathit{s}\mathit{e}}}{\mathrm{\leftarrow}}{\mathit{}}{a}$ cannot be true in any interpretation.

Both the top-down and the bottom-up proof procedures can be used to prove inconsistency, by using false as the query.