problem-set/logic.problems/morgan/morgan.six.ver1.desc created : 07/15/86 revised : 07/15/88 Natural Language Description: The files that begin with morgan.six concern problem six sent by Charles Morgan of Victoria University. The problem asks if ((a => b) => [(b => c) => (a => c)]) can be deduced from the three axioms given. The axioms are as follows: 1. x => (y => x) 2. [x => (y => z)] => [(x => y) => (x => z)] 4. -(x => y) | -x | y => means "implies", and - means "not". Thus axiom 4 represents the inference rule of modus ponens. Versions: morgan.six.ver1.in- Only axiom 1 and the negation of the hypothesis are in the set of support. Nonequality based axioms are used, UR resolution is the inference rule, and demodulators are not included. created by: E. Lusk verified for ITP: 07/15/86 translated for OTTER: SLM verified for OTTER: no proof