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 a set of clauses is Herbrand unsatisfiable then there exists a contradictory finite conjunction of ground instances of elements of the set of clauses.
|
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.
|
S' is unsatisfiable iff S = CNF(S') is unsatisfiable
A set of clauses has a model iff it has a Herbrand model, so
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
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) }
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:
|
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).