CSE 463/563, Spring 2003

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:

From a subproof ¬α |- [ ]
Infer α in that subproof

1. F <-> (M ^ P)
2. M
3. P
4. Therefore, F

1a.¬FM// premise, from 1
1b.¬FP// premise, from 1
1c.¬M¬PF// premise, from 1
2.M// premise, from 2
3.P// premise, from 3
*  4.¬F// temporary premise, 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 © 2003 by William J. Rapaport (rapaport@cse.buffalo.edu)
file: 563/resolution.pf.2003.03.27.html