Resolution Example[Chang and Lee, Symbolic Logic and
Mechanical Theorem Proving, Academic Press, 1973.]
- No used car dealer buys a used car for his family.
- Some people who buy used cars are absolutely dishonest.
- Conclusion: Some absolutely dishonest people are not used car dealers.
- &forall x ( U(x) &rarr ¬ B(x) )
- &exist x ( B(x) &and D(x) )
- &exist x ( D(x) &and ¬ U(x) )
- ¬ U(x) &or ¬ B(x)
- a. B(a) b. D(a)
- ¬ ( &exist x ( D(x) &and ¬ U(x) ) )
&forall x ¬ ( D(x) &and ¬ U(x) )
&forall x ( ¬ D(x) &or U(x) )
¬ D(x) &or U(x)
- (1, 2.a.) ¬ U(a)
- (3, 4) ¬ D(a)
- (2.b, 5.) □
Contents
Page-10
Prev
Next
Page+10
Index