problem-set/algebra/henkin.models/hp5.desc created : 07/23/86 revised : 07/19/89 Natural Language Description : Theorem HP5: In a Henkin model, LE is transitive. Versions : hp5.ver1 : P-formulation, using hyperresolution and UR-resolution. created : 07/09/86. verified for ITP : untested. translated for OTTER by : caw. verified for OTTER : 07/17/89. hp5.ver2 : Equality formulation, using UR-resolution and paramodulation. created : 07/09/86. verified for ITP : untested. translated for OTTER by : caw. verified for OTTER : 07/18/89. hp5.ver3 : Equality formulation with LE removed, using UR-resolution, paramodulation, and dynamic demodulation. created : 07/19/89. verified for ITP : untested. translated for OTTER by : caw. verified for OTTER : 07/19/89.