Herbrand's Theorem
A set of clauses is Herbrand unsatisfiable iff there exists a
contradictory finite conjunction of ground Herbrand universe instances of
elements of the set.
| Proof
|
|---|
A set of clauses is Herbrand unsatisfiable if there exists a contradictory
finite conjunction of ground instances of elements of the set.
- If there exists a contradictory finite conjunction, then the set of
the conjuncts (the set of clause instances) is (Herbrand) unsatisfiable.
- For each branch of the semantic tree, one of the conjuncts is
FALSE in the interpretation identified by the branch.
- If an instance of a clause if
FALSE in a Herbrand
interpretation, then the clause itself is FALSE in the
interpretation.
- Therefore, in every interpretation, there is a clause that is
FALSE, i.e., every interpretation is not a model of the
set of clauses, i.e., the set of clauses is unsatisfiable.
If a set of clauses is Herbrand unsatisfiable then there exists a
contradictory finite conjunction of ground instances of elements of
the set of clauses.
- If a set of clauses is Herbrand unsatisfiable, then it has a failure tree.
- For each branch of the failure tree there is a ground instance of a
clause that is
FALSE at each failure node.
- As the failure tree is finite, the conjunction of these ground instances
is finite.
- As all branches of the semantic tree are 'covered' by the failure tree,
this finite conjunction is Herbrand unsatisfiable, and must therefore
contain a contradiction.
|
| Example
|
|---|
S = { wise(jim),
~wise(X) | wise(brother_of(X)),
~wise(brother_of(brother_of(jim))) }
A set of clauses is Herbrand unsatisfiable if there exists a contradictory
finite conjunction of ground instances of elements of the set.
If a set of clauses is Herbrand unsatisfiable then there exists a contradictory
finite conjunction of ground instances of elements of a set of clauses.
|
The Quest for Logical Consequence
To show that C is a logical consequence of A, it is necessary to:
- Show that every model of A is a model of C
OR
- Show that S' = A ∪ {~C} is unsatisfiable.
S' is unsatisfiable iff S = CNF(S') is unsatisfiable
- Show that S is unsatisfiable.
A set of clauses has a model iff it has a Herbrand model, so
- Show that S is Herbrand unsatisfiable.
A set of clauses is Herbrand unsatisfiable iff there exists a Herbrand
unsatisfiable (contradictory) finite conjunction of ground Herbrand
universe instances of elements of the set, so
- Search for a Herbrand unsatisfiable (contradictory) finite conjunction
of ground Herbrand universe instances of elements of S.
The Gilmore Procedure
This is a generic idea.
Ground instances of clauses are generated, and their conjunction tested.
This may be done directly using truth tables, by assigning a truth value
to each ground atom that appears in the conjunction.
Each such ground atom is an element of the Herbrand base, so such an
assignment is a partial specification for a Herbrand interpretation.
There are a finite number of such atoms, so there are a finite number of
rows in the table of interpretations.
If no such interpretation is a model of the conjunction, i.e., the conjunction
is a contradiction, then the original set is Herbrand unsatisfiable, and
logical consequence is established.
| Example
|
|---|
S1 = { p(b) | r(Y) | p(Y),
~p(S) | p(b),
~p(b),
~r(a),
~r(c) }
p(b) | r(Y) | p(Y)
|
+
|
~p(b)
|
|
|
=
|
r(Y) | p(Y)
|
r(Y) | p(Y)
|
+
|
~r(a)
|
|
|
=
|
p(a)
|
p(a)
|
+
|
~p(S) | p(b)
|
|
|
=
|
p(b)
|
p(b)
|
+
|
~p(b)
|
FALSE
|
The set of ground Herbrand universe instances, which the Gilmore procedure
would find, is :
{ p(b) | r(a) | p(a),
~p(a) | p(b),
~p(b),
~r(a) }
The truth table that shows that this set is Herbrand unsatisfiable is:
p(a) |
p(b) |
r(a) |
p(b) | r(a) | p(a) |
~p(a) | p(b) |
~p(b) |
~r(a) |
T |
T |
T |
T |
T |
F |
F |
T |
T |
F |
T |
T |
F |
T |
T |
F |
T |
T |
F |
T |
F |
T |
F |
F |
T |
F |
T |
T |
F |
T |
T |
T |
T |
F |
F |
F |
T |
F |
T |
T |
F |
T |
F |
F |
T |
T |
T |
T |
F |
F |
F |
F |
F |
T |
T |
T |
|
An alternative to the "table" method is to use a specialized propositional
decision procedure, e.g., the DPLL procedure.
The way in which ground instances are generated is crucial.
There are several techniques, including systematic ones and heuristically
guided ones.
The Gilmore procedure has a very large search space.
An alternative solution is to delay the instantiation of variables for as
long as possible.
This is the technique used in resolution.
As a by-product, resolution finds contradictory conjunctions of instances
of clauses in a set of clauses.
If there are uninstantiated variables in the refutation, then any Herbrand
universe instantiation will provide a contradictory set of ground Herbrand
universe instances
(every ground instance of a contradictory conjunction is also contradictory).
