Transcript Document

Logic seminar 4
Herbrand’s theorem
07.11.2005.
Slobodan Petrović
Herbrand’s theorem
• A general decision procedure to verify the
validity (inconsistency) of a formula:
– Tried by Leibnitz, Peano, Hilbert, …
– Proved inexistent by Church and Turing (1936)
• Church and Turing independently showed that
there is no general decision procedure to check
the validity of formulas of the first order logic.
Herbrand’s theorem
• There are, however, proof procedures which
can verify that a formula is valid if it is valid
indeed.
• For invalid formulas, these procedures never
terminate in general.
• This is the best that one can expect from a
proof procedure.
Herbrand’s theorem
• By definition, a valid formula is a formula that
is true under all interpretations.
• Herbrand (1930) developed an algorithm to
find an interpretation (if it exists) that can
falsify a given formula.
• If the given formula is indeed valid, no such
interpretation can exist and Herbrand’s
algorithm halts after a finite number of trials.
Herbrand’s theorem
• Herbrand’s procedure is a refutation procedure.
• Instead of proving a formula valid, it proves
that the negation of the formula is inconsistent.
• There is no loss of generality in using
refutation procedures.
• The refutation procedures are applied to a
“standard” form of a formula.
Herbrand’s theorem
• The standard form:
– A formula of the first order logic is transformed
into prenex normal form:
• The matrix contains no quantifiers
• The prefix is a sequence of quantifiers.
– The matrix is transformed into a conjunctive
normal form.
– The existential quantifiers in the prefix are
eliminated by using Skolem functions.
Herbrand’s theorem
• Skolem standard form (standard form)
– Let a formula F be already in a prenex normal
form (Q1x1)…(Qnxn)M, where M is in a
conjunctive normal form.
– Let Qr be an existential quantifier in the prefix
(Q1x1)…(Qnxn), 1≤r≤n.
Herbrand’s theorem
• Skolem standard form (cont.)
– If no universal quantifier appears before Qr, we do
the following:
• choose a new constant c different from other constants
occurring in M;
• replace all xr appearing in M by c;
• delete (Qrxr) from the prefix.
Herbrand’s theorem
• Skolem standard form (cont.)
– If Qs1,…,Qsm are all the universal quantifiers
appearing before Qr, 1≤s1≤s2≤…≤sm≤r, we do the
following:
• choose a new m-place function symbol f different from
other function symbols occurring in M;
• replace all xr appearing in M by f(xs1,xs2,…,xsm);
• delete (Qrxr) from the prefix.
Herbrand’s theorem
• Skolem standard form (cont.)
– After this process is applied to all the existential
quantifiers in the prefix, a Skolem standard form
of the formula F is obtained.
– The constants and functions used to replace the
existential variables are called Skolem functions.
– This process is called Skolemization.
Herbrand’s theorem
• Example
– Obtain a standard form of the formula
• (x)(y)(z)(u)(v)(w)P(x,y,z,u,v,w)
– (x) is preceded by no universal quantifiers, (u) is
preceded by (y) and (z), and (w) by (y), (z)
and (v).
– Therefore, we replace the existential variable x by
a constant a, u by a two-place function f(y,z), and
w by a three-place function g(y,z,v).
– The standard form of the formula is
• (y)(z)(v)P(a,y,z,f(y,z),v,g(y,z,v)).
Herbrand’s theorem
• Example
– Obtain a standard form of the formula
• (x)(y)(z)((~P(x,y)Q(x,z))R(x,y,z)).
– First, the matrix is transformed into a conjunctive
normal form:
• (x)(y)(z)((~P(x,y)R(x,y,z))(Q(x,z)R(x,y,z))).
– Then, since (y) and (z) are both preceded by
(x), the existential variables y and z are replaced,
respectively by one-place functions f(x) and g(x).
– The standard form of the formula is
• (x)((~P(x,f(x))R(x,f(x),g(x)))(Q(x,g(x))R(x,f(x),g(x)))).
Herbrand’s theorem
• Definition
– A clause is a disjunction of literals.
• When it is convenient, it is possible to regard a
set of literals as synonymous with a clause.
• Example
– PQ~R={P,Q,~R}
• A clause consisting of r literals is called an
literal clause.
• A one-literal clause is called a unit clause.
r-
Herbrand’s theorem
• When a clause contains no literal, it is called
the empty clause.
• Since the empty clause has no literal that can
be satisfied by an interpretation, the empty
clause is always false.
• The empty clause is denoted by □.
• Example – the clauses are
– ~P(x,f(x))R(x,f(x),g(x))
– Q(x,g(x))R(x,f(x),g(x)).
Herbrand’s theorem
• A set S of clauses is regarded as a conjunction
of all clauses in S.
• Every variable in S is considered governed by
a universal quantifier.
• Thus, a standard form can be represented by a
set of clauses.
Herbrand’s theorem
• Example
– The standard form of the formula
• (x)((~P(x,f(x))R(x,f(x),g(x)))(Q(x,g(x))R(x,f(x),g(x))))
– can be represented by a set of clauses
• {~P(x,f(x))R(x,f(x),g(x)), Q(x,g(x))R(x,f(x),g(x))}.
• Theorem
– Let S be a set of clauses that represents a standard
form of a formula F.
– Then F is inconsistent if and only if S is
inconsistent.
Herbrand’s theorem
• Let S be a standard form of a formula F.
• If F is inconsistent, then F=S.
• If F is not inconsistent, F is not equivalent to S
in general.
• Example
– F=(x)P(x),
– S=P(a).
– S is a standard form of F.
Herbrand’s theorem
• Example (cont.)
– The interpretation I:
• Domain: D={1,2}
• Assignment for P: P(1)=F, P(2)=T.
– F is true in I, but S is false in I. That is, FS.
• A formula may have more than one standard form.
• When a formula F is transformed into a standard
formula S, existential quantifiers should be replaced
by the simplest possible Skolem functions – with the
least number of arguments.
Herbrand’s theorem
• Existential quantifiers should be moved to the
left as far as possible.
• If F=F1…Fn, it is possible to separately
obtain a set Si of clauses, where Si represents a
standard form of Fi, i=1,…,n.
• Let S=S1…Sn.
• Then F is inconsistent if and only if S is
inconsistent.
Herbrand’s theorem
• Example
– The theorem: If xx=e for all x in group G, where 
is a binary operator and e is the identity in G, then
G is commutative.
– We first symbolize the theorem and some other
axioms of group theory.
– Then we represent the negation of the theorem as a
set of clauses.
Herbrand’s theorem
• Example (cont.)
– The axioms of the group:
• A1: x,yG implies that xyG (closure property)
• A2: x,y,zG implies that x(yz)=(xy)z (associativity
property)
• A3: xe=ex=x for all xG (identity property)
• A4: For every xG there exists an element x-1G such
that xx-1=x-1x=e (inverse property).
Herbrand’s theorem
• Example (cont.)
– Let P(x,y,z) stand for xy=z and i(x) for x-1.
– Then, the axioms of the group can be represented
by:
• A1’: (x)(y)(z)P(x,y,z)
• A2’: (x)(y)(z)(u)(v)(w)(P(x,y,u)P(y,z,v)P(u,z,w)P(x,v,w))
(x)(y)(z)(u)(v)(w)(P(x,y,u)P(y,z,v)P(x,v,w)P(y,z,w))
• A3’: (x)P(x,e,x)(x)P(e,x,x)
• A4’: (x)P(x,i(x),e)(x)P(i(x),x,e).
Herbrand’s theorem
• Example (cont.)
– The conclusion of the theorem:
• B: If xx=e for all xG, then G is commutative, i.e.,
uv=vu for all u,vG.
– B formalized:
• B’: (x)P(x,x,e)((u)(v)(w)(P(u,v,w)P(v,u,w))).
– The entire theorem is represented by the formula:
• F=A1’…A4’B’.
• Thus, ~F=A1’A2’A3’A4’~B’.
Herbrand’s theorem
• Example (cont.)
– To obtain a set S of clauses for ~F, we first obtain a
set Si of clauses for each axiom Ai’, i=1, 2, 3, 4:
• S1: {P(x,y,f(x,y))}
• S2: {~P(x,y,u)~P(y,z,v)~P(u,z,w)P(x,v,w),
~P(x,y,u)~P(y,z,v)~P(x,v,w)P(u,z,w)}
• S3: {P(x,e,x),P(e,x,x)}
• S4: {P(x,i(x),e),P(i(x),x,e)}.
Herbrand’s theorem
• Example (cont.)
• ~B’=~((x)P(x,x,e)((u)(v)(w)(P(u,v,w)P(v,u,w)
)))
=~(~(x)P(x,x,e)((u)(v)(w)(~P(u,v,w)P(v,u,w))))
=(x)P(x,x,e)~((u)(v)(w)(~P(u,v,w)P(v,u,w)))
=(x)P(x,x,e)(u)(v)(w)(P(u,v,w)~P(v,u,w)).
– A set of clauses for ~B’:
• T: {P(x,x,e),P(a,b,c),~P(b,a,c)}.
Herbrand’s theorem
• Example (cont.)
– The set S=S1S2S3S4T:
•
•
•
•
•
•
•
•
•
•
(1) P(x,y,f(x,y))
(2) ~P(x,y,u)~P(y,z,v)~P(u,z,w)P(x,v,w)
(3) ~P(x,y,u)~P(y,z,v)~P(x,v,w)P(u,z,w)
(4) P(x,e,x)
(5) P(e,x,x)
(6) P(x,i(x),e)
(7) P(i(x),x,e)
(8) P(x,x,e)
(9) P(a,b,c)
(10) ~P(b,a,c).
Herbrand’s theorem
• F is valid if and only if S is inconsistent.
• Refutation procedures are used to prove
theorems.
• The input to a refutation procedure is always a
set of clauses.
• Instead of “inconsistent” (“consistent”)
“unsatisfiable” (“satisfiable”) is used,
respectively for sets of clauses.
Herbrand’s theorem
• The Herbrand universe of a set of clauses
– A set of clauses S is unsatisfiable if and only if it is
false under all interpretation over all domains.
– It is impossible to consider all interpretations over all
domains.
– It would be desirable to have one special domain H
such that S is unsatisfiable if and only if S is false
under all the interpretations over this domain.
– There exists such a domain – Herbrand universe of S.
Herbrand’s theorem
• The Herbrand universe of a set of clauses
– Let H0 be the set of constants appearing in S.
– If no constant appears in S, then H0 is to consist of a
single constant, H0={a}.
– For i=0,1,2,… let Hi+1 be the union of Hi and the set
of all terms of the form fn(t1,…,tn) for all n-place
functions fn occurring in S, where tj, j=1,…,n, are
members of the set Hi.
– Hi is called the i-level constant set of S.
Herbrand’s theorem
• The Herbrand universe of a set of clauses
– Example 1: S={P(a),P(x)P(f(x))}
•
•
•
•
•
•
H0={a}
H1={a,f(a)}
H2={a,f(a),f(f(a))}
.
.
H={a,f(a),f(f(a)),f(f(f(a))),…}
Herbrand’s theorem
• The Herbrand universe of a set of clauses
– Example 2: S={P(x)Q(x),R(z),T(y)W(y)}
• There is no constant in S, so we let H0={a}
• There is no function symbol in S, hence H=H0=H1=…={a}
– Example 3: S={P(f(x),a,g(y),b)}
• H0={a,b}
• H1={a,b,f(a),f(b),g(a),g(b)}
• H2={a,b,f(a),f(b),g(a),g(b),f(f(a)),f(f(b)),f(g(a)),f(g(b)),g(f(a
)),g(f(b)),g(g(a)),g(g(b))}
•…
Herbrand’s theorem
• The Herbrand universe of a set of clauses
– Expression – a term, a set of terms, an atom, a set of
atoms, a literal, a clause, or a set of clauses.
– When no variable appears in an expression, it is
called a ground expression.
– It is possible to use a ground term, a ground atom, a
ground literal, and a ground clause – this means that
no variable occurs in respective expressions.
– A subexpression of an expression E is an expression
that occurs in E.
Herbrand’s theorem
• The Herbrand universe of a set of clauses
– Let S be a set of clauses. The set of ground atoms of
the form Pn(t1,…,tn) for all n-place predicates Pn
occurring in S, where t1,…,tn are elements of the
Herbrand universe of S, is called the atom set, or the
Herbrand base of S.
– A ground instance of a clause C of the set S of
clauses is a clause obtained by replacing variables in
C by members of the Herbrand universe of S.
Herbrand’s theorem
• The Herbrand universe of a set of clauses
– Example
•
•
•
•
S={P(x),Q(f(y))R(y)}
C=P(x) is a clause in S
H={a,f(a),f(f(a)),…} is the Herbrand universe of S.
P(a) and P(f(f(a))) are ground instances of C.
Herbrand’s theorem
• The Herbrand universe of a set of clauses
– Let S be a set of clauses.
– An interpretation over the Herbrand universe of S is
an assignment of constants, function symbols and
predicate symbols occurring in S.
Herbrand’s theorem
• The Herbrand universe of a set of clauses
– Let S be a set of clauses, H the Herbrand universe of
S and I an interpretation of S over H. I is an Hinterpretation of S if:
• I maps all constants in S to themselves.
• Let f be an n-place function symbol and h1,…,hn be
elements of H. In I, f is assigned a function that maps
(h1,…,hn) (an element in Hn) to f(h1,…,hn) (an element in
H).
Herbrand’s theorem
• The Herbrand universe of a set of clauses
– There is no restriction on the assignment to each
n-place predicate symbol in S.
– Let A={A1,A2,…,An,…} be the atom set of S.
– An H-interpretation I can be conveniently
represented by a set I={m1,m2,…,mn,…} in
which mj is either Aj or ~Aj for j=1,2,…
– If mj is Aj then Aj is assigned “true”, otherwise Aj
is assigned “false”.
Herbrand’s theorem
• The Herbrand universe of a set of clauses
– Example: S={P(x)Q(x),R(f(y))}
• The Herbrand universe of S is H={a,f(a),f(f(a)),…}.
• Predicate symbols: P, Q, R.
• The atom set of S:
– A={P(a),Q(a),R(a),P(f(a)),Q(f(a)),R(f(a)),…}.
• Some H-interpretations for S:
– I1={P(a),Q(a),R(a),P(f(a)),Q(f(a)),R(f(a)),…}
– I2={~P(a),~Q(a),~R(a),~P(f(a)),~Q(f(a)),~R(f(a)),…}
– I3={P(a),Q(a),~R(a),P(f(a)),Q(f(a)),~R(f(a)),…}
Herbrand’s theorem
• The Herbrand universe of a set of clauses
– An interpretation of a set S of clauses does not
necessarily have to be defined over the Herbrand
universe of S.
– Thus an interpretation may not be an
H-interpretation.
– Example:
• S={P(x),Q(y,f(y,a))}
• D={1,2}
Herbrand’s theorem
• The Herbrand universe of a set of clauses
– Example (cont.) – an interpretation of S:
a f(1,1) f(1,2) f(2,1) f(2,2)
2
1
2
2
1
P(1) P(2) Q(1,1) Q(1,2) Q(2,1) Q(2,2)
T
F
F
T
F
T
Herbrand’s theorem
• The Herbrand universe of a set of clauses
– Example (cont.) – we can define an H-interpretation I*
corresponding to I.
– First we find the atom set of S
• A={P(a),Q(a,a),P(f(a,a)),Q(a,f(a,a)),Q(f(a,a),a),Q(f(a,a),f(a,a)),…}
– Next we evaluate each member of A by using the given table
•
•
•
•
P(a)=P(2)=F
Q(a,a)=Q(2,2)=T
P(f(a,a))=P(f(2,2))=P(1)=T
Q(a,f(a,a))=Q(2,f(2,2))=Q(2,1)=F
Herbrand’s theorem
• The Herbrand universe of a set of clauses
– Example (cont.)
• Q(f(a,a),a)=Q(f(2,2),2)=Q(1,2)=T
• Q(f(a,a),f(a,a))=Q(f(2,2),f(2,2))=Q(1,1)=T
– H-interpretation I* corresponding to I
– I*={~P(a),Q(a,a),P(f(a,a)),~Q(a,f(a,a)),Q(f(a,a),a),
~Q(f(a,a),f(a,a)),…}.
Herbrand’s theorem
• The Herbrand universe of a set of clauses
– If there is no constant in S, the element a used to initiate the
Herbrand universe of S can be mapped into any element of
the domain D.
– If there is more than one element in D, then there is more
than one H-interpretation corresponding to I.
– Example: S={P(x),Q(y,f(y,z))}, D={1,2}
Herbrand’s theorem
• The Herbrand universe of a set of clauses
– Example (cont.):
f(1,1) f(1,2) f(2,1) f(2,2)
1
2
2
1
P(1) P(2) Q(1,1) Q(1,2) Q(2,1) Q(2,2)
T
F
F
T
F
T
Herbrand’s theorem
• The Herbrand universe of a set of clauses
– Example (cont.):
– Then the two H-interpretations corresponding to I are:
• I*={~P(a),Q(a,a),P(f(a,a)),~Q(a,f(a,a)),Q(f(a,a),a),
~Q(f(a,a),f(a,a)),…} if a=2,
• I*={P(a),~Q(a,a),P(f(a,a)),~Q(a,f(a,a)),~Q(f(a,a),a),
~Q(f(a,a),f(a,a)),…} if a=1.
Herbrand’s theorem
• The Herbrand universe of a set of clauses
– Definition
• Given an interpretation I over a domain D, an H-interpretation I*
corresponding to I is an H-interpretation that satisfies the condition:
• Let h1,…,hn be elements of H (the Herbrand universe of S). Let
every hi be mapped to some di in D. If P(d1,…,dn) is assigned T (F)
by I, then P(h1,…,hn) is also assigned T(F) in I*.
– Lemma:
• If an interpretation I over some domain D satisfies a set S of
clauses, then any H-interpretation I* corresponding to I also
satisfies S.
Herbrand’s theorem
• The Herbrand universe of a set of clauses
– Theorem
• A set S of clauses is unsatisfiable if and only if S is false under all
the H-interpretations of S.
– We need consider only H-interpretations for checking
whether or not a set of clauses is unsatisfiable.
– Thus, whenever the term “interpretation” is used, a
H-interpretation is meant.
Herbrand’s theorem
• The Herbrand universe of a set of clauses
– Let  denote an empty set. Then:
• A ground instance C’ of a clause C is satisfied by an interpretation I
if and only if there is a ground literal L’ in C’ such that L’ is also in
I, i.e. C’I.
• A clause C is satisfied by an interpretation I if and only if every
ground instance of C is satisfied by I.
• A clause C is falsified by an interpretation I if and only if there is at
least one ground instance C’ of C such that C’ is not satisfied by I.
• A set S of clauses is unsatisfiable if and only if for every
interpretation I there is at least one ground instance C’ of some
clause C in S such that C’ is not satisfied by I.
Herbrand’s theorem
• The Herbrand universe of a set of clauses
– Example: Consider the clause C=P(x)Q(f(x)). Let I1, I2,
and I3 be defined as follows:
• I1={P(a),Q(a),P(f(a)),Q(f(a)),P(f(f(a))),Q(f(f(a))),…}
• I2={P(a),Q(a),P(f(a)),Q(f(a)),P(f(f(a))),Q(f(f(a))),…}
• I3={P(a),Q(a),P(f(a)),Q(f(a)),P(f(f(a))),Q(f(f(a))),…}
– C is satisfied by I1 and I2, but falsified by I3.
– Example: S={P(x),P(a)}. The only two H-interpretations
are: I1={P(a)}, I2={P(a)}.
– S is falsified by both H-interpretations and therefore is
unsatisfiable.
Herbrand’s theorem
• Semantic trees
– Introduced by Robinson, 1968.
– It can be shown that finding a proof for a set of clauses is
equivalent to generating a semantic tree.
– Definition
• If A is an atom, then the two literals A and A are said to be each
other’s complement.
• The set {A,A} is called a complementary pair.
– A clause is a tautology if it contains a complementary pair.
Herbrand’s theorem
• Semantic trees
– Definition
• Given a set S of clauses, let A be the atom set of S.
• A semantic tree for S is a (downward) tree T, where each link is
attached with a finite set of atoms or negations of atoms from A in
such a way that:
– For each node N, there are only finitely many immediate links
L1,…,Ln from N. Let Qi be the conjunction of all the literals in the set
attached to Li, i=1,…,n. Then Q1Q2…Qn is a valid propositional
formula.
– For each node N, let I(N) be the union of all the sets attached to the
links of the branch of T down to and including N. Then I(N) does not
contain any complementary pair.
Herbrand’s theorem
• Semantic trees
– Definition
• Let A={A1,A2,…,Ak,…} be the atom set of a set S of clauses.
• A semantic tree for S is said to be complete if and only if for every
tip node N of the semantic tree, i.e. a node that has no links
sprouting from it, I(N) contains either Ai or Ai for i=1,2,…
– Example:
• Let A={P,Q,R} be the atom set of a set S of clauses.
• Two examples of complete semantic trees for S:
Herbrand’s theorem
• Semantic trees
– Example (cont.)
Herbrand’s theorem
• Semantic trees
– Example (cont.)
Herbrand’s theorem
• Semantic trees
– Example:
• S={P(x),P(a)}
• The atom set of S is {P(a)}
• A complete semantic tree for S:
– Example:
• S={P(x),Q(f(x))}
• The atom set of S is
{P(a),Q(a),P(f(a)),Q(f(a)),P(f(f(a))),Q(f(f(a))),…}
• A semantic tree for S:
Herbrand’s theorem
• Semantic trees
– Example (cont.)
Herbrand’s theorem
• Semantic trees
– For each node N in a semantic tree for S, I(N) is a subset of
some interpretation for S.
– I(N) is called partial interpretation for S.
– When the atom set A of a set S of clauses is infinite, any
complete semantic tree for S is infinite.
– A complete semantic tree for S corresponds to an
exhaustive survey of all possible interpretations for S.
– If S is unsatisfiable, then S fails to be true in each of the
interpretations.
– We may stop expanding nodes from a node N if I(N)
falsifies S.
Herbrand’s theorem
• Semantic trees
– Definition – A node N is a failure node if I(N) falsifies
some ground instance of a clause in S, but I(N’) does not
falsify any ground instance of a clause in S for every
ancestor node N’ of N.
– Definition – A semantic tree T is said to be closed if and
only if every branch of T terminates at a failure node.
– A node N of a closed semantic tree is called an inference
node if all the immediate descendant nodes of N are failure
nodes.
Herbrand’s theorem
• Semantic trees
– Example:
• Let S={P,QR,PQ,PR}.
• The atom set of S is A={P,Q,R}.
• A complete semantic tree for S:
Herbrand’s theorem
• Semantic trees
– Example (cont.):
• A closed semantic tree for S:
Herbrand’s theorem
• Semantic trees
– Example:
• Consider S={P(x),P(x)Q(f(x)),Q(f(a))}
• The atom set of S: A={P(a),Q(a),P(f(a)),Q(f(a)),…}
• A closed semantic tree for S:
Herbrand’s theorem
• To test whether a set S of clauses is unsatisfiable, we
need consider only interpretations over the Herbrand
universe of S.
• If S is false under all interpretations over the
Herbrand universe of S, then we can conclude that S
is unsatisfiable.
• Since there are usually many, possibly an infinite
number, of these interpretations, we should organize
them in a systematic way – by using a semantic tree.
Herbrand’s theorem
• Herbrand’s theorem – Version 1 (a classical one).
– A set S of clauses is unsatisfiable if and only if there is a
finite unsatisfiable set S’ of ground instances of clauses of
S.
• Herbrand’s theorem – Version 2 (with semantic trees)
– A set S of clauses is unsatisfiable if and only if
corresponding to every complete semantic tree of S, there
is a finite closed semantic tree.
Herbrand’s theorem
• Example:
– Let S={P(x),P(f(a))}.
– S is unsatisfiable.
– Hence, by Herbrand’s theorem, there is a finite
unsatisfiable set S’ of ground instances of clauses
in S.
– One of these sets is S’={P(f(a)),P(f(a))}
Herbrand’s theorem
• Example:
– Let S={P(x)Q(f(x),x),P(g(b)),Q(y,z)}
– S is unsatisfiable.
– One of the unsatisfiable sets of ground instances of
clauses in S:
• S’={P(g(b))Q(f(g(b)),g(b)),P(g(b)),Q(f(g(b)),g(b))}
Herbrand’s theorem
• Example:
– Let S consist of the following clauses:
• S={P(x,y,u)P(y,z,v)P(x,v,w)P(u,z,w),
P(x,y,u)P(y,z,v)P(u,z,w)P(x,v,w),
P(g(x,y),x,y),P(x,h(x,y),y),P(x,y,f(x,y)),
P(k(x),x,k(x))}
– S is unsatisfiable.
– It is not easy to find by hand a finite unsatisfiable
set S’ of ground instances of clauses in S.
Herbrand’s theorem
• Example (cont.):
– One way to find such a set S’ is to generate a
closed semantic tree T’ for S.
– Then the set S’ of all the ground instances falsified
at all the failure nodes of T’ is such a desired set.
– Each ground clause in S’ is a ground instance of
some clause in S.
– S’ is unsatisfiable.
Herbrand’s theorem
• Example (cont.):
– The set S’:
S’={P(a,h(a,a),a),P(k(h(a,a)),h(a,a),k(h(a,a))),
P(g(a,k(h(a,a))),a,k(h(a,a))),
P(g(a,k(h(a,a))),a,k(h(a,a)))P(a,h(a,a),a)
P(g(a,k(h(a,a))),a,k(h(a,a)))
P(k(h(a,a)),h(a,a),k(h(a,a)))}
Herbrand’s theorem
• Implementations of Herbrand’s theorem
– The classical version of the Herbrand’s theorem
suggests a refutation procedure.
– Given an unsatisfiable set of clauses to prove, if
there is a mechanical procedure that can
successively generate sets S1’,…Sn’,… of ground
instances of clauses in S and can successively test
S1’,S2’,… for unsatisfiability, then it is guaranteed
by Herbrand’s theorem that this procedure can
detect a finite N such that Sn’ is unsatisfiable.
Herbrand’s theorem
• Gilmore’s implementation
– In 1960, Gilmore wrote a computer program that
successively generated S0’,S1’,… , where Si’ is the
set of all the ground instances obtained by
replacing variables in S by the constants in the
i-level constant set Hi of S.
– Since each Si’ is a conjunction of ground clauses, it
is possible to use any method of the propositional
logic to check its unsatisfiability.
Herbrand’s theorem
• Gilmore’s implementation (cont.)
– Gilmore used the multiplication method.
– As each Si’ is produced, it is multiplied out into a
disjunctive normal form.
– Any conjunction in the disjunctive normal form
containing a complementary pair is removed.
– Should some Si’ be empty, then Si’ is unsatisfiable
and a proof is found.
Herbrand’s theorem
• Gilmore’s implementation (cont.)
– Example: S={P(x),P(a)}.
• H0={a}
• S0’=P(a)P(a)=□.
• Thus S is proved to be unsatisfiable.
Herbrand’s theorem
• Gilmore’s implementation (cont.)
– Example: S={P(a),P(x)Q(f(x)),Q(f(a))}.
• H0={a}
• S0’=P(a)(P(a)Q(f(a)))Q(f(a))
=(P(a)P(a)Q(f(a)))(P(a)Q(f(a))Q(f(a)))
=□□=□.
• Thus S is proved to be unsatisfiable.
Herbrand’s theorem
• Gilmore’s implementation (cont.)
– The multiplication method used by Gilmore is
inefficient.
– Even for a small set of ten two-literal ground
clauses, there are 210 conjunctions.
Herbrand’s theorem
• The method of Davis and Putnam
– Let S be a set of ground clauses.
– The method of Davis and Putnam consists of four
rules:
• Tautology:
– Delete all the ground clauses from S that are tautologies. The
remaining set S’ is unsatisfiable if and only if S is.
• One-literal rule:
– If there is a unit ground clause L in S, obtain S’ from S by
deleting those ground clauses in S containing L. If S’ is empty,
S is satisfiable. Otherwise, obtain a set S’’ from S’ by deleting
L from S’. S’’ is unsatisfiable if and only if S is. If L is a unit
ground clause, then the clause becomes □ when L is deleted
from it.
Herbrand’s theorem
• The method of Davis and Putnam
– The method of Davis and Putnam rules (cont.):
• Pure-literal rule:
– A literal L in a ground clause of S is said to be pure in S if and
only if the literal L does not appear in any ground clause in S.
If a literal L is pure in S, delete all the ground clauses
containing L. The remaining set S’ is unsatisfiable if and only if
S is.
Herbrand’s theorem
• The method of Davis and Putnam
– The method of Davis and Putnam rules (cont.):
• Splitting rule:
– If the set S can be put into the form:
(A1L)…(AmL)(B1L)…(BnL)R,
where Ai, Bi, and R are free of L and L, then obtain the sets
S1=A1…AmR and S2=B1…BnR. S is unsatisfiable if and
only if (S1S2) is unsatisfiable, i.e. both S1 and S2 are
unsatisfiable.
Herbrand’s theorem
• The method of Davis and Putnam
– Example: Show that
S=(PQR)(PQ)PRU is unsatisfiable.
(PQR)(PQ)PRU
(QR)(Q)RU
(One-literal rule on P)
RRU
(One-literal rule on Q)
□U
(One-literal rule on R)
– Since the last formula contains the empty clause □,
S is unsatisfiable.
Herbrand’s theorem
• The method of Davis and Putnam
– Example: Show that S=(PQ)Q(PQR) is
satisfiable.
(PQ)Q(PQR)
P(PR)
R
■
– Thus, S is satisfiable.
(One-literal rule on Q)
(One-literal rule on P)
(One-literal rule on R)
Herbrand’s theorem
• The method of Davis and Putnam
– Example: Show that
S=(PQ)(PQ)(QR)(QR) is
satisfiable.
(PQ)(PQ)(QR)(QR)
(Q(QR)(QR))
(Q(QR)(QR))
(Splitting rule on P)
RR
(One-literal rule on Q and Q)
■■
(One-literal rule on R)
– Thus, S is satisfiable.
Herbrand’s theorem
• The method of Davis and Putnam
– Example: Show that
S=(PQ)(PQ)(RQ)(RQ) is satisfiable.
(PQ)(PQ)(RQ)(RQ)
(RQ)(RQ)
(Pure-literal rule on P)
■
(Pure-literal rule on R)
– Thus, S is satisfiable.
Herbrand’s theorem
• The method of Davis and Putnam
– The method of Davis and Putnam is more efficient
than the Gilmore’s multiplication method.
– This method can be applied to any formula in the
propositional logic.
– The procedure is:
• Transform the given propositional formula into a
conjunctive normal form.
• Apply the four rules on the conjunctive normal form.