CS计算机代考程序代写 COMP30026 Models of Computation - Predicate Logic: Clausal Form

COMP30026 Models of Computation – Predicate Logic: Clausal Form

COMP30026 Models of Computation
Predicate Logic: Clausal Form

Bach Le / Anna Kalenkova

Lecture Week 4 Part 2 (Zoom)

Semester 2, 2021

Models of Computation (Sem 2, 2021) Predicate Logic: Clausal Form c© University of Melbourne 1 / 18

This Lecture is Being Recorded

Models of Computation (Sem 2, 2021) Predicate Logic: Clausal Form c© University of Melbourne 2 / 18

Resolution for Predicate Logic

The resolution technique generalises to first-order predicate logic.

As for propositional logic, it assumes clausal form, that is, having a
formula presented in conjunctive normal form, without any
quantifiers.

Again, it consists on generating logical consequences (resolvents),
trying to derive an empty clause, thereby proving the original formula
unsatisfiable.

Existential quantifiers are eliminated in a process called
Skolemization.

Models of Computation (Sem 2, 2021) Predicate Logic: Clausal Form c© University of Melbourne 3 / 18

Eliminating Existential Quantifiers

Consider the formula F = ∃x∀y P(x , y ) under some interpretation I.

F is satisfiable iff some valuation σ makes ∀y P(x , y ) true. Say that
σ, with σ(x) = d0, makes ∀y P(x , y ) true.

Now consider a fresh constant a, and the formula ∀y P(a, y ) .

This formula is satisfiable iff F is. If I satisfies F then we simply add
to I the mapping of a to d0—this extended interpretation satisfies
∀y P(a, y ).

If ∀y P(x , y ) is unsatisfiable, there is no valuation that will make
∀y P(x , y ) true. Hence no interpretation will make ∀y P(a, y ) true.

Models of Computation (Sem 2, 2021) Predicate Logic: Clausal Form c© University of Melbourne 4 / 18

Skolem Constants and Functions

Now consider the formula G = ∀y∃x P(x , y ).

We cannot conclude that ∀y P(a, y ) is satisfiable iff G is.

Since ∃x is within the scope of ∀y , the value of x for which P(x , y )
holds may differ, given different values of y . The value of x is a
function of the value of y . Replacing x by a constant will not do.

But then we can generate the formula ∀y P(f (y ), y ), choosing a
fresh function symbol f .

For reasons similar to those outlined on slide 4, this formula is
satisfiable iff G is.

Models of Computation (Sem 2, 2021) Predicate Logic: Clausal Form c© University of Melbourne 5 / 18

Skolemization

We call a (on slide 4) a Skolem constant, and f (on slide 5) a Skolem
function.

Skolem functions can be of arbitrary arity. To eliminate ∃y in
∀x1, x2, x3 ∃y [. . .] we replace each occurrence of y in its scope by
f (x1, x2, x3).

Namely, y may depend on all three xs.

Each introduced Skolem constant or function must be fresh.

Recall also our convention: We use letters from the start of the
alphabet (a, b, c, . . . ) for constants, and letters from the end of the
alphabet (u, v , x , y . . . ) for variables.

Models of Computation (Sem 2, 2021) Predicate Logic: Clausal Form c© University of Melbourne 6 / 18

Skolemization Example

This formula has three existential quantifiers—we remove them one
by one:

∃u∀v∃x∀y∃z
((¬P(u, f (v ), x , b) ∨ R(g(x , y ), u)) ∧ S(y , g(a, z)))

Models of Computation (Sem 2, 2021) Predicate Logic: Clausal Form c© University of Melbourne 7 / 18

Skolemization Example

This formula has three existential quantifiers—we remove them one
by one:

∃u∀v∃x∀y∃z
((¬P(u, f (v ), x , b) ∨ R(g(x , y ), u)) ∧ S(y , g(a, z)))

∀v∃x∀y∃z
((¬P(c, f (v ), x , b) ∨ R(g(x , y ), c)) ∧ S(y , g(a, z)))

Models of Computation (Sem 2, 2021) Predicate Logic: Clausal Form c© University of Melbourne 7 / 18

Skolemization Example

This formula has three existential quantifiers—we remove them one
by one:

∃u∀v∃x∀y∃z
((¬P(u, f (v ), x , b) ∨ R(g(x , y ), u)) ∧ S(y , g(a, z)))

∀v∃x∀y∃z
((¬P(c, f (v ), x , b) ∨ R(g(x , y ), c)) ∧ S(y , g(a, z)))

∀v∀y∃z
((¬P(c, f (v ), h(v ), b) ∨ R(g(h(v ), y ), c)) ∧ S(y , g(a, z)))

Models of Computation (Sem 2, 2021) Predicate Logic: Clausal Form c© University of Melbourne 7 / 18

Skolemization Example

This formula has three existential quantifiers—we remove them one
by one:

∃u∀v∃x∀y∃z
((¬P(u, f (v ), x , b) ∨ R(g(x , y ), u)) ∧ S(y , g(a, z)))

∀v∃x∀y∃z
((¬P(c, f (v ), x , b) ∨ R(g(x , y ), c)) ∧ S(y , g(a, z)))

∀v∀y∃z
((¬P(c, f (v ), h(v ), b) ∨ R(g(h(v ), y ), c)) ∧ S(y , g(a, z)))

∀v∀y
((¬P(c, f (v ), h(v ), b) ∨ R(g(h(v ), y ), c)) ∧ S(y , g(a, j(v , y ))))

Models of Computation (Sem 2, 2021) Predicate Logic: Clausal Form c© University of Melbourne 7 / 18

Skolemization Example

This formula has three existential quantifiers—we remove them one
by one:

∃u∀v∃x∀y∃z
((¬P(u, f (v ), x , b) ∨ R(g(x , y ), u)) ∧ S(y , g(a, z)))

∀v∃x∀y∃z
((¬P(c, f (v ), x , b) ∨ R(g(x , y ), c)) ∧ S(y , g(a, z)))

∀v∀y∃z
((¬P(c, f (v ), h(v ), b) ∨ R(g(h(v ), y ), c)) ∧ S(y , g(a, z)))

∀v∀y
((¬P(c, f (v ), h(v ), b) ∨ R(g(h(v ), y ), c)) ∧ S(y , g(a, j(v , y ))))

Instead of j(v , y ) we could have chosen k(v , y ), or even j(y , v )—as
long as we replace each occurrence of z by the same term, of course.

Models of Computation (Sem 2, 2021) Predicate Logic: Clausal Form c© University of Melbourne 7 / 18

From Predicate Logic Formulas to Clausal Form

The process is similar to what we did with propositional formulas:

1 Replace occurrences of ⊕, ⇔, and ⇒.

2 Drive negation in.

3 Standardise bound variables apart.

4 Eliminate existential quantifiers (Skolemize).

5 Eliminate universal quantifiers (just remove them).

6 Bring to CNF (using the distributive laws).

Models of Computation (Sem 2, 2021) Predicate Logic: Clausal Form c© University of Melbourne 8 / 18

Clausal Form: Step 1—Use Just ∨, ∧, ¬

Let us use this running example:

∀x (P(x)⇔∃y (R(x , y ) ∧ ∀z R(z , y )))

First use the usual translations to eliminate ⇔ (and ⇒ and ⊕):

∀x

(

(P(x)⇒∃y (R(x , y ) ∧ ∀z R(z , y ))) ∧
(∃y (R(x , y ) ∧ ∀z R(z , y ))⇒ P(x))

)

which then becomes:

∀x

(

(¬P(x) ∨ ∃y (R(x , y ) ∧ ∀z R(z , y ))) ∧
(¬∃y (R(x , y ) ∧ ∀z R(z , y )) ∨ P(x))

)

Models of Computation (Sem 2, 2021) Predicate Logic: Clausal Form c© University of Melbourne 9 / 18

Clausal Form: Step 2—Push Negation

Next drive negation in.

∀x

(

(¬P(x) ∨ ∃y (R(x , y ) ∧ ∀z R(z , y ))) ∧
(¬∃y (R(x , y ) ∧ ∀z R(z , y )) ∨ P(x))

)

then becomes

∀x

(

(¬P(x) ∨ ∃y (R(x , y ) ∧ ∀z R(z , y ))) ∧
(∀y (¬R(x , y ) ∨ ∃z ¬R(z , y )) ∨ P(x))

)

Models of Computation (Sem 2, 2021) Predicate Logic: Clausal Form c© University of Melbourne 10 / 18

Clausal Form: Step 3—Standardize Apart

Now rename variables so that no two quantifiers use the same
variable name. With that,

∀x

(

(¬P(x) ∨ ∃y (R(x , y ) ∧ ∀z R(z , y ))) ∧
(∀y (¬R(x , y ) ∨ ∃z ¬R(z , y )) ∨ P(x))

)

turns into, say

∀x

(

(¬P(x) ∨ ∃y (R(x , y ) ∧ ∀z R(z , y ))) ∧
(∀u (¬R(x , u) ∨ ∃v ¬R(v , u)) ∨ P(x))

)

Models of Computation (Sem 2, 2021) Predicate Logic: Clausal Form c© University of Melbourne 11 / 18

Clausal Form: Step 4—Skolemize

Let us highlight the existentially quantified variables:

∀x

(

(¬P(x) ∨ ∃y (R(x , y ) ∧ ∀z R(z , y ))) ∧
(∀u (¬R(x , u) ∨ ∃v ¬R(v , u)) ∨ P(x))

)

The existentially quantified y is in the scope of ∀x—so replace it by
f (x).

Models of Computation (Sem 2, 2021) Predicate Logic: Clausal Form c© University of Melbourne 12 / 18

Clausal Form: Step 4—Skolemize

Let us highlight the existentially quantified variables:

∀x

(

(¬P(x) ∨ ∃y (R(x , y ) ∧ ∀z R(z , y ))) ∧
(∀u (¬R(x , u) ∨ ∃v ¬R(v , u)) ∨ P(x))

)

The existentially quantified y is in the scope of ∀x—so replace it by
f (x).

The existentially quantified v is in the scope of ∀x , as well as of ∀u.
So we replace it by g(u, x).

∀x

(

(¬P(x) ∨ (R(x , f (x)) ∧ ∀z R(z , f (x)))) ∧
(∀u (¬R(x , u) ∨ ¬R(g(u, x), u)) ∨ P(x))

)

Clausal Form: Step 5—Drop Universal Quantifiers

Eliminating universal quantifiers is easy:

∀x

(

(¬P(x) ∨ (R(x , f (x)) ∧ ∀z R(z , f (x)))) ∧
(∀u (¬R(x , u) ∨ ¬R(g(u, x), u)) ∨ P(x))

)

becomes

(¬P(x)∨(R(x , f (x))∧R(z , f (x))))∧(¬R(x , u)∨¬R(g(u, x), u)∨P(x))

It is understood that all variables are now universally quantified. If
you prefer, you can think of all the universal quantifiers as sitting in
front of the formula.

Clausal Form: Step 6—Convert to CNF

(¬P(x)∨(R(x , f (x))∧R(z , f (x))))∧(¬R(x , u)∨¬R(g(u, x), u)∨P(x))

becomes, using distribution:

(¬P(x) ∨ R(x , f (x))) ∧
(¬P(x) ∨ R(z , f (x))) ∧
(¬R(x , u) ∨ ¬R(g(u, x), u) ∨ P(x))

or, written as a set of sets of literals:






{¬P(x),R(x , f (x))},
{(¬P(x),R(z , f (x))},

{(¬R(x , u),¬R(g(u, x), u),P(x))}







Justifying Skolemization

Note that Skolemization of a formula does not produce a logically
equivalent formula.

For example, ∀x∃y P(x , y ) turns into ∀x P(x , f (x)).

If we interpret these in the domain Z of integers, interpreting f as the
“successor” function (+1), and P as >, then the original formula is
satisfied, but the second is not.

However, Skolemization does produce an equisatisfiable formula—one
that is satisfiable iff the original was—and this is all we care about for
the purposes of resolution proofs.

A First Look at Resolution for Predicate Logic

We wish to develop the resolution principle for predicate logic with
function symbols.

However, now we will not be resolving on simple literals, but on
atomic formulas containing variables, constants, and function
symbols.

Simple cases seem easy enough, for example, from

¬B(x) ∨M(x) and ¬M(c)

we would like to conclude ¬B(c). (“Every borogove is mimsy” and
“Colin is not mimsy” entails “Colin is not a borogove.”)

Resolution for Predicate Logic

Note that all variables in

¬B(x) ∨M(x) and ¬M(c)

are universally quantified.

In particular, we could instantiate ¬B(x) ∨M(x) to ¬B(c) ∨M(c);
then we will be resolving the two clauses on M(c) and its negation,
just as happened in the propositional case.

The resolvent then comes out as ¬B(c), as we hoped.

Next we will develop this idea and define resolution deduction for
arbitrary sets of clauses.

Next Week

How resolution can be extended to predicate logic.

Plus: Induction principles.

Related Posts