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:
-
Schagrin, Morton L.;
Rapaport, William J.;
&
Dipert,
Randall R. (1985),
Logic: A Computer Approach (New York:
McGraw-Hill).
(SEL: BC138 .S32 1985)
-
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