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 | 劃分 RealNumber, NegativeRealNumber and NonnegativeRealNumber |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 1893-1893 | 劃分 RealNumber, RationalNumber and IrrationalNumber |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 1891-1891 | 子類 RealNumber and Number |
appearance as argument number 2 |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 2009-2009 | 不相交的 ComplexNumber and RealNumber |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 1825-1825 | 劃分 Number, RealNumber, ImaginaryNumber and ComplexNumber |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 4714-4714 | 範圍 加成 and RealNumber |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 5260-5260 | 範圍 ArcCosineFn and RealNumber |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 5270-5270 | 範圍 ArcSineFn and RealNumber |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 5250-5250 | 範圍 ArcTangentFn and RealNumber |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 3272-3272 | 範圍 AverageFn and RealNumber |
No TPTP formula. May not be expressible in strict first order. | People.kif 71-71 | 範圍 每千人分娩 and RealNumber |
No TPTP formula. May not be expressible in strict first order. | People.kif 443-443 | 範圍 每個女人出生的孩子 and RealNumber |
No TPTP formula. May not be expressible in strict first order. | UXExperimentalTerms.kif 3331-3331 | 範圍 ClickThroughRateFn and RealNumber |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 4802-4802 | 範圍 餘弦 and RealNumber |
No TPTP formula. May not be expressible in strict first order. | People.kif 104-104 | 範圍 每千人死亡 and RealNumber |
No TPTP formula. May not be expressible in strict first order. | People.kif 230-230 | 範圍 每千名活產嬰兒死亡人數 and RealNumber |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 4744-4744 | 範圍 部 and RealNumber |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 4821-4821 | 範圍 冪 and RealNumber |
No TPTP formula. May not be expressible in strict first order. | People.kif 396-396 | 範圍 女性出生時的預期壽命 and RealNumber |
No TPTP formula. May not be expressible in strict first order. | People.kif 299-299 | 範圍 出生時的預期壽命 and RealNumber |
No TPTP formula. May not be expressible in strict first order. | UXExperimentalTerms.kif 4555-4555 | 範圍 LiftFn and RealNumber |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 3241-3241 | 範圍 ListSumFn and RealNumber |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 4977-4977 | 範圍 日誌 and RealNumber |
No TPTP formula. May not be expressible in strict first order. | People.kif 348-348 | 範圍 男性出生時的預期壽命 and RealNumber |
No TPTP formula. May not be expressible in strict first order. | People.kif 193-193 | 範圍 男女比例 and RealNumber |
No TPTP formula. May not be expressible in strict first order. | People.kif 140-140 | 範圍 每千人移民 and RealNumber |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 4701-4701 | 範圍 乘法 and RealNumber |
No TPTP formula. May not be expressible in strict first order. | UXExperimentalTerms.kif 3088-3088 | 範圍 PPIFn and RealNumber |
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 and RealNumber |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 4712-4712 | 域 加成, 1 and RealNumber |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 4713-4713 | 域 加成, 2 and RealNumber |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 5259-5259 | 域 ArcCosineFn, 1 and RealNumber |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 5269-5269 | 域 ArcSineFn, 1 and RealNumber |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 5249-5249 | 域 ArcTangentFn, 1 and RealNumber |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 4783-4783 | 域 天花板, 1 and RealNumber |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 4810-4810 | 域 分母, 1 and RealNumber |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 4742-4742 | 域 部, 1 and RealNumber |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 4743-4743 | 域 部, 2 and RealNumber |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 4819-4819 | 域 冪, 1 and RealNumber |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 4828-4828 | 域 地板, 1 and RealNumber |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 4923-4923 | 域 整數平方根, 1 and RealNumber |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 4975-4975 | 域 日誌, 1 and RealNumber |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 6348-6348 | 域 測量, 1 and RealNumber |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 4699-4699 | 域 乘法, 1 and RealNumber |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 4700-4700 | 域 乘法, 2 and RealNumber |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 5036-5036 | 域 分子, 1 and RealNumber |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 5070-5070 | 域 互相, 1 and RealNumber |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 5170-5170 | 域 回合, 1 and RealNumber |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 5189-5189 | 域 正負號, 1 and RealNumber |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 5211-5211 | 域 正弦, 1 and RealNumber |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 5219-5219 | 域 平方根, 1 and RealNumber |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 4726-4726 | 域 減法, 1 and RealNumber |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 4727-4727 | 域 減法, 2 and RealNumber |
Display limited to 25 items. Show next 25 | ||
Display limited to 25 items. Show next 25 |
antecedent |
consequent |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 1948-1952 | 例 RealNumber and NegativeRealNumber 少於 RealNumber and 0 例 RealNumber and RealNumber |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 1926-1930 | 例 RealNumber and NonnegativeRealNumber 大於或等於 RealNumber and 0 例 RealNumber and RealNumber |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 1937-1941 | 例 RealNumber and PositiveRealNumber 比較多 RealNumber and 0 例 RealNumber and RealNumber |
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 |
|