problem-set/algebra/boolean/prob2.desc created: 07/09/86 revised: 08/02/89 Natural Language Description: The files beginning with prob2 concern the proof of the theorem from boolean algebra stating that x + x = x and x * x = x. Versions: prob2_part1.ver1: This is the theorem from boolean algebra stating that x * x = x. Hyper resolution is the inference rule and demodulators are not included. created: 07/09/86 verified for ITP: 06/30/86 translated for OTTER: tlh verified for OTTER: 08/08/89 prob2_part1.ver2: This is the above theorem with equality formulation and demodulation. Paramodulation is the inference rule. created: 07/31/89 verified for ITP: not yet translated for OTTER: tlh verified for OTTER: 07/31/89 prob2_part2.ver1: This is the theorem from boolean algebra stating that x + x = x. Hyper resolution is the inference rule and demodulators are not included. created: 07/09/86 verified for ITP: 06/30/86 translated for OTTER: tlh verified for OTTER: 07/31/89 prob2_part2.ver2 - This is the above theorem with equality formulation and demodulation. Paramodulation is the inference rule. created: 08/02/89 verified for ITP: not yet translated for OTTER: tlh verified for OTTER: 08/02/89