problem-set/algebra/henkin.models/hp10.desc created : 07/23/86 revised : 07/19/89 Natural Language Description : Theorem HP10: In a Henkin model, for all x, if x'=1/x, then x' = x'/(1/x'). Versions : hp10.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/18/89. hp10.ver2 : Equality formulation, using paramodulation and UR-resolution. created : 07/09/86. verified for ITP : untested. translated for OTTER by : caw. verified for OTTER : 07/18/89. hp10.ver3 : Equality formulation with LE removed, using paramodulation, UR-resolution, unit deletion, and dynamic demodulation. created : 07/19/89. verified for ITP : untested. translated for OTTER by : caw. verified for OTTER : 07/19/89.