Herbrand Revisited
Herbrand Revisited: We have presented the concept of Herbrand Universe HS for a set of clauses S. Here we meet the concept of Herbrand Base, H(S), for a set of clauses S. H(S) is obtained from S by considering the ground instances of the clauses of S under all the substitutions that map all the variables of S into elements of the Herbrand universe of S. Clearly, if in S occurs some variable and the Herbrand universe of S is infinite then H(S) is infinite.
[NOTE: Viceversa, if S has no variables, or S has variables and possibly individual constants, but no other function symbol, then H(S) is finite. If H(S) is finite then we can, as we will see, decide if S is or not satisfiable.]
[NOTE: it is easy to determine if a finite subset of H(S) is satisfiable: since it consists of ground clauses, the truth table method works now as in propositional cases.]
But, as we shall soon see, we can come up with a better refutation complete proof procedure.
Refutation Completeness of the Resolution Proof Procedure: Given a set of clauses S, the Resolution Closure of S, R(S), is the smallest set of clauses that contains S and is closed under Resolution. In other words, it is the set of clauses obtained from S by applying repeatedly resolution.
Ground Resolution Theorem: If S is an unsatisfiable set of ground clauses, then R(S) contains the clause FALSE. In other words, there is a resolution deduction of FALSE from S.
Lifting Lemma: Given clauses C1 and C2 that have no variables in common, and ground instances C1' and C2', respectively, of C1 and C2, if C' is a resolvent of C1' and C2', then there is a clause C which is a resolvent of C1 and C2 which has C' as a ground instance
With this we have our result, that the Resolution Proof procedure is Refutation Complete. Note the crucial role played by the Herbrand Universe and Basis. Unsatisfiability of S is reduced to unsatisfiability for a finite subset HS(S) of H(S), which in turn is reduced to the problem of finding a resolution derivation for FALSE in HS(S), derivation which can be "lifted" to a resolution proof of FALSE from S.
Dealing with Equality: Up to now we have not dealt with equality, that is, the ability to recognize terms as being equivalent (i.e. always denoting the same individual) on the basis of some equational information. For example, given the information that
S(x) = x 1
then we can unify:
F(S(x) y) and F(x 1, 3).
There are two basic approaches to dealing with this problem.
- The first is to add inference rules to help us replace terms by equal terms. One such rule is the Demodulation Rule: Given terms t1, t2, and t3 where t1 and t2 are unifiable with MGU s, and t2 occurs in a formula A, then
{t1 = t3, A(... t2 ...)}
------------------------
A(... t3.s ...)
Another more complex, and useful, rule is ParamodulationThe importance of the concepts of Herbrand Universe and of Herbrand Base is due to the following theorems:
Herbrand Theorem: If a set S of clauses is unsatisfiable then there is a finite subset of H(S) that is also unsatisfiable.
Because of the theorem, when H(S) is finite we will be able to decide is S is or not satisfiable. Herbrand theorem immediately suggests a general refutation complete proof procedure:
given a set of clauses S, enumerate subsets of H(S) until you find one that is unsatisfiable.
- The second approach is not to add inference rules and instead to add non-logical axioms that characterize equality and its effect for each non logical symbol. We first establish the reflexive, symmetric and transitive properties of "=":
x=x
x=y IMPLIES y=x
x=y AND y=z IMPLIES x=z
Then for each unary function symbol F we add the equality axiom
x=y IMPLIES F(x)=F(y)
Then for each binary function symbol F we add the equality axiom
x=z AND y=w IMPLIES F(x y)=F(z w)
And similarly for all other function symbols.
The treatment of predicate symbols is similar. For example, for the binary predicate symbol P we add
x=z AND y=w IMPLIES ( P(x y) IFF P(z w))
Whatever approach is chosen, equality substantially complicates proofs.