No TPTP formula. May not be expressible in strict first order. | Merge.kif 1891-1891 | 实数 是 数字 的 subclass |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 1911-1911 | 有理数 是 实数 的 subclass |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 1916-1916 | 无理数 是 实数 的 subclass |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 1921-1921 | 非负实数 是 实数 的 subclass |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 1943-1943 | 负实数 是 实数 的 subclass |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 2003-2003 | 二进制数 是 实数 的 subclass |