5.5 Proving by Contradiction

5.5.1 Horn Clauses

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

falsea1ak.

where the ai 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 ¬p is the negation of p, which is true in an interpretation when p is false in that interpretation, and pq 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 falsea1ak is logically equivalent to ¬a1¬ak.

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

Example 5.19.

Consider the knowledge base 𝐾𝐵1:

𝑓𝑎𝑙𝑠𝑒ab.
ac.
bc.

The atom c is false in all models of 𝐾𝐵1. To see this, suppose instead that c is true in model I of 𝐾𝐵1. Then a and b would both be true in I (otherwise I would not be a model of 𝐾𝐵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 𝐾𝐵1. Thus ¬c is true in all models of 𝐾𝐵1, which can be written as

𝐾𝐵1¬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.

Example 5.20.

Consider the knowledge base 𝐾𝐵2:

𝑓𝑎𝑙𝑠𝑒ab.
ac.
bd.
be.

Either c is false or d is false in every model of 𝐾𝐵2. If they were both true in some model I of 𝐾𝐵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 𝐾𝐵2. Similarly, either c is false or e is false in every model of 𝐾𝐵2. Thus,

𝐾𝐵2¬c¬d
𝐾𝐵2¬c¬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.

Example 5.21.

The set of clauses {a,𝑓𝑎𝑙𝑠𝑒a} is unsatisfiable. There is no interpretation that satisfies both clauses. Both a and 𝑓𝑎𝑙𝑠𝑒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.