# How resolution methods' rules apply in proofs

I understand that resolution methods are used to prove something by disproving its negation (proof by contradiction), but I don't understand how this idea is implemented in formulas.

The following is a set of problems that was given to me as an assignment, and even after I got the complete answers for those problems in its review session I still don't understand how it works.

Problem 1

Premises:
P Ʌ Q  → R
R Ʌ T → S
→ P
→ Q
→ T
Conclusion:  S  drives from the premises    Therefore: demonstrate       S →    through resolution

R Ʌ T → S       S  →
R /\ T ->         P /\ Q -> R
T /\ P /\ Q ->           -> T
P /\ Q ->                 -> P
Q ->                      -> Q
->


Why is there nothing on the left side of the arrows of the premises? (-> P, ->Q, -> T)

Why does

R /\ T


P /\ Q -> R


?

And I'm wondering about basically the same thing on the rest of the problems (2-4)

Problem 2
Premises:
P Ʌ Q Ʌ R → S
U Ʌ V → P
W → Q
→ R
→ U
→ V
→ W

Conclusion:  S  drives from the premises    Therefore: demonstrate       S →    through resolution

P /\ Q /\ R -> S          S ->
P /\ Q /\ R ->            U /\ V -> P
Q /\ /\ U /\ V ->                W -> Q
R /\ U /\ V /\ W ->                -> R
U /\ V /\ W ->                     -> U
V /\ W  ->                         -> V
W ->                               -> W
->

Problem 3
Premises:
P(x) → Q(x)
Q(x) → R(x)
S(x) Ʌ T(y) → P(x)
→ S(1)
→ S(2)
→ S(3)
→ T(1)
→ T(3)

Conclusion:  R(2)  derives from the premises.   Therefore:  demonstrate  R(2) →     through resolution

Q(x0) → R(x0)            R(2) →
{<x0,2>}
P(x1) → Q(x1)           Q(2) →
{<x1, 2>}
P(2) ->     S(x2) /\ T(y2) -> P(x2)
{<x, 2>}
S(2) /\ T (y) ->        -> S(2)
T(y) ->         -> T(1)
{<y2, 1>}
->


What is going on in the curly braces, like

{<x0,2>}


?

Problem 4

Demonstrate by using resolution method that Anna has a grandmother

→   Mother(Lena,Ida)
→   Mother(Ida,Anna)

Mother(x,y) Ʌ Mother(y,z) → Grandmother(x,z)

Mother(x0,y0) Ʌ Mother(y0,z0) → Grandmother(x0,z0)      Grandmother(x,Anna) →
{x0,x>,<z0,Anna>}
Motherr(x,y0) Ʌ Motherr(y0,Anna) →              -> Mother(Lena, Ida)
{<x, Lena>,<y0, Ida>}
Mother(Ida, Anna) ->            -> Mother(Ida, Anna)
->

• "I don't understand how this idea is implemented in formulas." What textbook are you using ? Lectures notes ? For sure there must be examples. – Mauro ALLEGRANZA May 19 at 8:53

Why is there nothing on the left side of the arrows of the premises? (-> P, ->Q, -> T)

That "nothing" implies them means $$P, Q,$$ and $$T$$ are each unconditionally true.

Conversely, $$R\land T$$ implies "nothing" means $$R\land T$$ is false.

Why does $$R \land T$$ lead to $$P \land Q \to R$$

It doesn't. $$R\land T\to\{\}$$ and $$P\land Q \to R$$ combine to derive $$P\land Q\land T\to\{\}$$. The resolution process cancels the $$R$$ on the left and right and combines the remainder of the statements. $$\dfrac{\require{cancel}\cancel R\land T\to\{\}\qquad P\land Q\to\cancel R}{P\land Q\land T\to \{\}}$$

In full...

$$\dfrac{\dfrac{\dfrac{\dfrac{\dfrac{R \land T \to S \qquad S \to\varnothing}{R \land T \to\varnothing}\quad\lower{1.5ex}{P \land Q \to R}}{T \land P \land Q \to\varnothing}\quad\lower{1.5ex}{\varnothing\to T}}{ P \land Q \to\varnothing}\quad\lower{1.5ex}{\varnothing\to P}}{Q \to\varnothing}\quad\lower{1.5ex}{\varnothing\to Q}}{\varnothing\to\varnothing}$$

What is going on in the curly braces, like $$\{\langle x_0,2\rangle\}$$

They merely indicate that the free variable and constant term were being resolved in that step; ie, "all instances of $$x_0$$ are replaced by $$2$$".$$\dfrac{Q(x_0)\to R(x_0)\qquad R(2)\to\{\}}{Q(2)\to\{\}}{\{\langle x_0,2\rangle\}}$$

• Thank you for your answer. Can you tell me how you read the formula in English as well? For example, how does "R∧T→∅ P∧Q→R" read? Is it "If R and T implies nothing, then P and Q implies R"? Also, what is the purpose of replacing x0 with a number like 2? And why is it x0 instead of just a regular x? – Shinichi Takagi May 19 at 17:48