Open Mind Tree

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

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 falseor 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 - that is, to prove disjunctions of negations of atoms. Recall that ¬p is the negation of p, which is true in an interpretation when p is false in that interpretation, and p∨q is the disjunction of pand 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 false←a₁∧...∧a_k is logically equivalent to ¬a₁∨...∨¬a_k.

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

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

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.

Both the top-down and the bottom-up proof procedures can be used to prove inconsistency, by using falseas the query. That is, a Horn clause knowledge base is inconsistent if and only if false can be derived.