Resolution

refutation method

proves unsatisfiability by deriving contradiction

works on clauses

Resolution rule

if A and B are clauses and x a variable:

A∨x B∨¬x

A∨B

Proof method

if a set of clauses is unsatisfiable, the empty clause can be derived by resolution

example: prove that {x, ¬x∨y, ¬y} is unsatisfiable:

x		¬x∨y
	⇓
	y		¬y
		⇓
	⊥

Other example

prove that {¬x∨¬y, ¬x∨y, x∨¬y, x∨y} is unsatisfiable

x∨y		¬x∨y
	⇓
	y			x∨¬y
			⇓
			x			¬x∨¬y
					⇓
					¬y
		⇓
			⊥

Another proof

same unsatisfiable set: {¬x∨¬y, ¬x∨y, x∨¬y, x∨y}

x∨y		¬x∨y		x∨¬y		¬x∨¬y
	⇓				⇓
	y				¬y
		⇓
			⊥

Resolution for first-order logic

still works on clauses

definition of clauses is slightly different from propositional logic

Clause in first order logic

∀x₁…∀x_m L₁ ∨ … ∨ L_n

where L_i's are literals
no free variables in the clause (all quantified)

Convention

by convention: quantifiers omitted

written as: L₁ ∨ … ∨ L_n

still no free variables!

quantified by ∀x₁…∀x_m

convention simplifies writing
omission not a consequence of semantics

Resolution rule

A, B clauses
L₁, L₂ literals

A∨L₁		B∨¬L₂
(A∨Bδ)σ

where:

δ is a renaming of B∨¬L₂ to new variables
σ is a MGU of L₁ and L₂δ

Factoring rule

A clause
L₁, L₂ literals

A∨L₁∨L₂

(A∨L₁)σ

where:

σ is a MGU of L₁ and L₂

next: why δ?
why σ?

MGU: explanation

A∨L₁		B∨¬L₂
(A∨Bδ)σ

why the substitution σ?

otherwise, rule could not be applied to clauses like:

P(x) ∨ ¬Q(f(z), y)
R(z,f(b)) ∨ Q(x, y)

indeed, Q(f(z), y) similar but not equal to Q(x, y)

idea: apply MGU [f(z)/x] to both clauses

MGU: application

the MGU of the two literals is [f(z)/x]

apply to both clauses:

P(x) ∨ ¬Q(f(z), y)	⇒	P(f(z)) ∨ ¬Q(f(z), y)
R(z,f(b)) ∨ Q(x, y)	⇒	R(z,f(b)) ∨ Q(f(z), y)

literals now exactly opposite of each other

but...

Renaming

a closer look at x in the two clauses:
(implicit quantifiers made explicit):

P(x) ∨ ¬Q(f(z), y)	=	∀x∀y∀z P(x) ∨ ¬Q(f(z), y)
R(z,f(b)) ∨ Q(x, y)	=	∀x∀y∀z R(z,f(b)) ∨ Q(x, y)

to match the literals Q(…), make x=f(z) everywhere

but then, P(x) becomes P(f(z))

necessary?

Renaming

rename the variables of the second clause:

P(x) ∨ ¬Q(f(z), y)	=	∀x∀y∀z P(x) ∨ ¬Q(f(z), y)
R(z',f(b)) ∨ Q(x', y')	=	∀x'∀y'∀z' R(z',f(b)) ∨ Q(x', y)

semantics is unchanged (because of implicit quantifiers)

now MGU is x'=f(z)

P(x) unchanged

Renaming: comparison

without renaming:: P(f(z)) ∨ R(z,f(b)) = ∀z P(f(z)) ∨ R(z,f(b))
with renaming:: P(x) ∨ R(z',f(b)) = ∀x∀z' P(x) ∨ R(z',f(b))

first formula weaker

P true only for f(z), not for every value

Renaming: general case

not just because of MGU application:

variables shared by A∨L₁ and B∨L₂ are forced equal in A∨B
since they are universally quantified, their names can be changed in one of the two clauses
this way, in the resulting clause the variables are no longer bound to be equal

Resolution rule: summary

rename the variables of the second clause: does not change the semantics, but avoid an unwanted equality in the resulting clause
unify the two opposite literals: necessary to make them equal
apply the rule as in the propositional case: can now be done because the literals are one the opposite of the other

Substitutions: correctness

both MGU and renaming are substitutions

P(x) ∨ ¬Q(f(z), y)	=	∀x∀y∀z P(x) ∨ ¬Q(f(z), y)
R(z,f(b)) ∨ Q(x, y)	=	∀x∀y∀z R(z,f(b)) ∨ Q(x, y)

to such formulae:

applying a substitution=produce a formula equivalent or weaker

e.g.: instead of ∀x, statement holds for x=f(z)

Correctness and completeness

resolution and factorization rules correct

formula unsatisfiable ⇒ empty clause can be generated by applying them

it can be proved (completeness)
(in this course, no formal proof of completeness seen)