RealNumber
|
|
appearance as argument number 1 |
No TPTP formula. May not be expressible in strict first order. | chinese_format.kif 1737-1738 | |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 1895-1897 | |
No TPTP formula. May not be expressible in strict first order. | japanese_format.kif 345-346 | |
No TPTP formula. May not be expressible in strict first order. | pictureList.kif 11735-11735 | |
No TPTP formula. May not be expressible in strict first order. | pictureList.kif 10223-10223 | |
No TPTP formula. May not be expressible in strict first order. | pictureList.kif 11734-11734 | |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 1892-1892 | 实数 详尽无遗地 partition 成 负实数 和 非负实数 |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 1893-1893 | 实数 详尽无遗地 partition 成 有理数 和 无理数 |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 1891-1891 | 实数 是 数字 的 subclass |
appearance as argument number 2 |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 2009-2009 | 复数 和 % 2 是 disjoint |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 1825-1825 | 数字 详尽无遗地 partition 成 实数, 虚数, 和 复数 |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 4714-4714 | 加法函数 的 range 是 实数 的实例 |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 5260-5260 | ArcCosineFn 的 range 是 实数 的实例 |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 5270-5270 | ArcSineFn 的 range 是 实数 的实例 |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 5250-5250 | ArcTangentFn 的 range 是 实数 的实例 |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 3272-3272 | AverageFn 的 range 是 实数 的实例 |
No TPTP formula. May not be expressible in strict first order. | People.kif 71-71 | 每千人分娩 的 range 是 实数 的实例 |
No TPTP formula. May not be expressible in strict first order. | People.kif 443-443 | 每个女人出生的孩子 的 range 是 实数 的实例 |
No TPTP formula. May not be expressible in strict first order. | UXExperimentalTerms.kif 3331-3331 | ClickThroughRateFn 的 range 是 实数 的实例 |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 4802-4802 | 馀弦函数 的 range 是 实数 的实例 |
No TPTP formula. May not be expressible in strict first order. | People.kif 104-104 | 每千人死亡 的 range 是 实数 的实例 |
No TPTP formula. May not be expressible in strict first order. | People.kif 230-230 | 每千名活产婴儿死亡人数 的 range 是 实数 的实例 |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 4744-4744 | 除法函数 的 range 是 实数 的实例 |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 4821-4821 | 次幂函数 的 range 是 实数 的实例 |
No TPTP formula. May not be expressible in strict first order. | People.kif 396-396 | 女性出生时的预期寿命 的 range 是 实数 的实例 |
No TPTP formula. May not be expressible in strict first order. | People.kif 299-299 | 出生时的预期寿命 的 range 是 实数 的实例 |
No TPTP formula. May not be expressible in strict first order. | UXExperimentalTerms.kif 4555-4555 | LiftFn 的 range 是 实数 的实例 |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 3241-3241 | ListSumFn 的 range 是 实数 的实例 |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 4977-4977 | 对数函数 的 range 是 实数 的实例 |
No TPTP formula. May not be expressible in strict first order. | People.kif 348-348 | 男性出生时的预期寿命 的 range 是 实数 的实例 |
No TPTP formula. May not be expressible in strict first order. | People.kif 193-193 | 男女比例 的 range 是 实数 的实例 |
No TPTP formula. May not be expressible in strict first order. | People.kif 140-140 | 每千人移民 的 range 是 实数 的实例 |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 4701-4701 | 乘法函数 的 range 是 实数 的实例 |
No TPTP formula. May not be expressible in strict first order. | UXExperimentalTerms.kif 3088-3088 | PPIFn 的 range 是 实数 的实例 |
Display limited to 25 items. Show next 25 | ||
Display limited to 25 items. Show next 25 |
appearance as argument number 3 |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 4762-4762 | 绝对值函数 的 1 数量 是 实数 的 instance |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 4712-4712 | 加法函数 的 1 数量 是 实数 的 instance |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 4713-4713 | 加法函数 的 2 数量 是 实数 的 instance |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 5259-5259 | ArcCosineFn 的 1 数量 是 实数 的 instance |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 5269-5269 | ArcSineFn 的 1 数量 是 实数 的 instance |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 5249-5249 | ArcTangentFn 的 1 数量 是 实数 的 instance |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 4783-4783 | 顶整数函数 的 1 数量 是 实数 的 instance |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 4810-4810 | 分母函数 的 1 数量 是 实数 的 instance |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 4742-4742 | 除法函数 的 1 数量 是 实数 的 instance |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 4743-4743 | 除法函数 的 2 数量 是 实数 的 instance |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 4819-4819 | 次幂函数 的 1 数量 是 实数 的 instance |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 4828-4828 | 底整数函数 的 1 数量 是 实数 的 instance |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 4923-4923 | 整数平方根函数 的 1 数量 是 实数 的 instance |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 4975-4975 | 对数函数 的 1 数量 是 实数 的 instance |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 6348-6348 | 计量函数 的 1 数量 是 实数 的 instance |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 4699-4699 | 乘法函数 的 1 数量 是 实数 的 instance |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 4700-4700 | 乘法函数 的 2 数量 是 实数 的 instance |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 5036-5036 | 分子函数 的 1 数量 是 实数 的 instance |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 5070-5070 | 倒数函数 的 1 数量 是 实数 的 instance |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 5170-5170 | 四舍五入函数 的 1 数量 是 实数 的 instance |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 5189-5189 | 正或负值函数 的 1 数量 是 实数 的 instance |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 5211-5211 | 正弦函数 的 1 数量 是 实数 的 instance |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 5219-5219 | 平方根函数 的 1 数量 是 实数 的 instance |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 4726-4726 | 减法函数 的 1 数量 是 实数 的 instance |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 4727-4727 | 减法函数 的 2 数量 是 实数 的 instance |
Display limited to 25 items. Show next 25 | ||
Display limited to 25 items. Show next 25 |
antecedent |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 4768-4779 | 实数 的绝对值 equal 非负实数 和 那个 实数 是 实数 的 instance 和 那个 非负实数 是 实数 的 instance 若且唯若 那个 实数 是 非负实数 的 instance 和 那个 实数 equal 那个 非负实数 或 那个 实数 是 负实数 的 instance 和 那个 非负实数 equal (0.0 和 那个 实数) |
No TPTP formula. May not be expressible in strict first order. | UXExperimentalTerms.kif 3239-3259 | |
No TPTP formula. May not be expressible in strict first order. | UXExperimentalTerms.kif 3282-3302 | |
No TPTP formula. May not be expressible in strict first order. | Food.kif 479-488 | |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 5239-5245 | |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 6902-6906 |
consequent |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 1948-1952 | 实数 是 负实数 的 instance 若且唯若 那个 实数 是 lessThan 0 和 那个 实数 是 实数 的 instance |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 1926-1930 | 实数 是 非负实数 的 instance 若且唯若 那个 实数 是 greaterThanOrEqualTo 0 和 那个 实数 是 实数 的 instance |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 1937-1941 | 实数 是 正实数 的 instance 若且唯若 那个 实数 是 greaterThan 0 和 那个 实数 是 实数 的 instance |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 5369-5374 | |
No TPTP formula. May not be expressible in strict first order. | Food.kif 770-781 |