0
$\begingroup$

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 

lead to

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)                
            ->                  
$\endgroup$
  • $\begingroup$ "I don't understand how this idea is implemented in formulas." What textbook are you using ? Lectures notes ? For sure there must be examples. $\endgroup$ – Mauro ALLEGRANZA May 19 at 8:53
1
$\begingroup$

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\}}$$

$\endgroup$
  • $\begingroup$ 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? $\endgroup$ – Shinichi Takagi May 19 at 17:48

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.