Last Update: 16 March 2005
Note: or material is highlighted |

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:

Infer α in that subproof

1. F
(M ^ P)

2. M

3. P

4. Therefore, F

1a. | ¬FvM | : assumption, from 1 |

1b. | ¬FvP | : assumption, from 1 |

1c. | ¬Mv¬PvF | : assumption, from 1 |

2. | M | : assumption, from 2 |

3. | P | : assumption, from 3 |

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

* 5. | ¬Mv¬PvF | : send 1c |

* 6. | ¬Mv¬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, ¬Elim |

12. | F | : return 11 |

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

file: 563S05/resolution.pf-2005-03-16.html