problem-set/algebra/boolean/prob4.desc created: 06/30/86 revised: 08/18/89 Natural Language Description: The files beginning with prob4 concern the proof of the theorem from boolean algebra stating that x + (x * y) = x and x * (x + y) = x. Versions: prob4_part1.ver1: This is the proof of x * (x + y) = x. Hyperresolution is the inference rule and demodulators are not included. created: 06/30/86 verified for ITP: 06/30/86 translated for OTTER: tlh verified for OTTER: not yet prob4_part1.ver2 - This is the proof of x * (x + y) = x using equality formulation and demodulation. Paramodulation is the inference rule. created: 08/08/89 verified for ITP: not yet translated for OTTER: tlh verified for OTTER: 08/08/89 prob4_part2.ver1 - This is the proof of x + (x * y) = x. Hyperresloution is the inference rule and demodulators are not included. created: 06/30/86 verified for ITP: 06/30/86 translated for OTTER: tlh verified for OTTER: not yet prob4_part2.ver2 - This is the proof of x + (x * y) = x using equality formulation and demodulation. Paramodulation is the inference rule. created: 08/08/89 verified for ITP: not yet translated for OTTER: tlh verified for OTTER: 08/08/89