problem-set/algebra/rings/zero.desc created : 07/10/86 revised : 07/12/88 Natural Language Description : The problem is to prove that in any ring for all x, x * 0 = 0 [ where 0 is the additive identity element ]. Versions : zero.ver1.in: this is the nonprocedural version; it uses UR resolution. created : ? verified for ITP : 07/09/86. translated for OTTER by : caw. verified for OTTER : 07/12/88. zero.ver2.in: this is the procedural version, its main difference from version 1 being that it uses the demodulator -(-x)=x, which is a basic lemma of ring theory [ - indicates additive inverse ]; uses UR resolution. created : ? verified for ITP : untested. translated for OTTER by : caw. verified for OTTER : 07/12/88.