**CSE 472/572, Spring 2002**
#### RESOLUTION PROOF IN NATURAL-DEDUCTION FORMAT

Here is the resolution proof we did in lecture written in the notation
of our earlier natural-deduction system assuming that Resolution has
been added as a rule of inference. Note: We can then simplify the rule
of ¬Elimination to read as follows:
__If, from an assumption ¬P in some subproof, you can infer { } in that subproof__

Then you can infer P in that subproof

1. F <=> (M ^ P)

2. M

3. P

4. Therefore, F

1a. | ¬FM | // assumption, from 1 |

1b. | ¬FP | // assumption, from 1 |

1c. | ¬M¬PF | // assumption, from 1 |

2. | M | // assumption, from 2 |

3. | P | // assumption, from 3 |

* 4. | ¬F | // temporary assumption, from 4 |

* 5. | ¬M¬PF | // send 1c |

* 6. | ¬M¬P | // 1c, 4, Resolution |

* 7. | M | // send 2 |

* 8. | ¬P | // 6, 7, Resolution |

* 9. | P | // send 3 |

*10. | { } | // 8, 9, Resolution |

*11. | F | // 4, 10, ¬Elimination |

12. | F | // return 11 |

Copyright © 2002 by
William J. Rapaport
(rapaport@cse.buffalo.edu)

file: 572/S02/resolution.pf.02ap02.html