CSE 472/572, Spring 2002

ANOTHER NATURAL-DEDUCTION EXAMPLE

Show ((A ^ B) ^ C) |- (A ^ C):

1.  ((A ^ B) ^ C)	// premise
/*
Backward chaining strategy:
     want to show (A ^ C)
     therefore, need to show A & need to show C
     then use ^Intro;

     to show each of A, C: use ^Elim on premise
*/

2.  (A ^ B) 		// 1, ^Elim
3.  A			// 2, ^Elim
4.  C			// 1, ^Elim
5.  (A ^ C)		// 3, 4, ^Intro
For more information on this kind of natural-deduction system, see:

  1. Schagrin, Morton L.; Rapaport, William J.; & Dipert, Randall R. (1985), Logic: A Computer Approach (New York: McGraw-Hill). (SEL: BC138 .S32 1985)

  2. Rapaport, William J. (1992), "Logic, Propositional", in Stuart C. Shapiro (ed.), Encyclopedia of Artificial Intelligence, 2nd edition (New York: John Wiley): 891-897. (Lockwood or SEL: Q335 .E53 1992)



Copyright © 2002 by William J. Rapaport (rapaport@cse.buffalo.edu)
file: 572/S02/natded.27fb02.html