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