|
|
   RealNumber
|
|
|
| appearance as argument number 1 |
|
|
| (documentation RealNumber ChineseLanguage "任何可以表达为一个（可能是无限的)十进制的 Number， 即任何在数字线上佔有一席位 Number。") | Merge.kif 1965-1966 | |
| (documentation RealNumber EnglishLanguage "Any Number that can be expressed as a (possibly infinite) decimal, i.e. any Number that has a position on the number line.") | Merge.kif 1962-1964 | |
| (externalImage RealNumber "http://upload.wikimedia.org/wikipedia/commons/ 0/ 09/ Number-line.gif") | pictureList.kif 11762-11762 | externalImage 实数 and "http://upload.wikimedia.org/wikipedia/commons/0/09/ Number-line.gif" |
| (externalImage RealNumber "http://upload.wikimedia.org/wikipedia/commons/ 9/ 98/ Real_Number_Line.PNG") | pictureList.kif 10244-10244 | externalImage 实数 and "http://upload.wikimedia.org/wikipedia/commons/9/98/ Real_Number_Line.PNG" |
| (externalImage RealNumber "http://upload.wikimedia.org/wikipedia/commons/ f/ fd/ Recta_real_entero_o_decimal_exacto.png") | pictureList.kif 11761-11761 | externalImage 实数 and "http://upload.wikimedia.org/wikipedia/commons/f/fd/ Recta_real_entero_o_decimal_exacto.png" |
| (partition RealNumber NegativeRealNumber NonnegativeRealNumber) | Merge.kif 1960-1960 | 实数 详尽无遗地 partition 成 负实数 和 非负实数 |
| (partition RealNumber RationalNumber IrrationalNumber) | Merge.kif 1961-1961 | 实数 详尽无遗地 partition 成 有理数 和 无理数 |
| (subclass RealNumber Number) | Merge.kif 1959-1959 | 实数 是 数字 的 subclass |
| appearance as argument number 2 |
|
|
| appearance as argument number 3 |
|
|
| antecedent |
|
|
| (<=> (and (equal (AbsoluteValueFn ?NUMBER1) ?NUMBER2) (instance ?NUMBER1 RealNumber) (instance ?NUMBER2 RealNumber)) (or (and (instance ?NUMBER1 NonnegativeRealNumber) (equal ?NUMBER1 ?NUMBER2)) (and (instance ?NUMBER1 NegativeRealNumber) (equal ?NUMBER2 (SubtractionFn 0 ?NUMBER1))))) |
Merge.kif 4924-4935 | 实数 的绝对值 equal 非负实数 和 那个 实数 是 实数 的 instance 和 那个 非负实数 是 实数 的 instance 若且唯若 那个 实数 是 非负实数 的 instance 和 那个 实数 equal 那个 非负实数 或 那个 实数 是 负实数 的 instance 和 那个 非负实数 equal (0 和 那个 实数) |
| (=> (and (instance ?BUYINGS Collection) (instance ?GMB CurrencyMeasure) (instance ?TOTAL RealNumber) (equal ?GMB (GMBFn ?BUYINGS)) (equal ?TOTAL (CardinalityFn (KappaFn ?ITEM (and (instance ?ITEM Object) (exists (?BUYING) (and (member ?BUYING ?BUYINGS) (patient ?ITEM ?BUYING)))))))) (equal (ABPFn ?BUYINGS) (DivisionFn ?GMB ?TOTAL))) |
UXExperimentalTerms.kif 3444-3464 | |
| (=> (and (instance ?REL RelationExtendedToQuantities) (instance ?REL BinaryPredicate) (instance ?NUMBER1 RealNumber) (instance ?NUMBER2 RealNumber) (?REL ?NUMBER1 ?NUMBER2)) (forall (?UNIT) (=> (instance ?UNIT UnitOfMeasure) (?REL (MeasureFn ?NUMBER1 ?UNIT) (MeasureFn ?NUMBER2 ?UNIT))))) |
Merge.kif 6585-6595 | |
| (=> (and (instance ?SELLINGS Collection) (instance ?GMV CurrencyMeasure) (instance ?TOTAL RealNumber) (equal ?GMV (GMVFn ?SELLINGS)) (equal ?TOTAL (CardinalityFn (KappaFn ?ITEM (and (instance ?ITEM Object) (exists (?SELLING) (and (member ?SELLING ?SELLINGS) (patient ?ITEM ?BUYING)))))))) (equal (ASPFn ?SELLINGS) (DivisionFn ?GMV ?TOTAL))) |
UXExperimentalTerms.kif 3487-3507 | |
| (=> (instance ?N RealNumber) (equal (MeasureFn ?N Horsepower) (MeasureFn (MultiplicationFn ?N 746) Watt))) |
Merge.kif 7145-7149 |
| consequent |
|
|
| (<=> (instance ?NUMBER NegativeRealNumber) (and (lessThan ?NUMBER 0) (instance ?NUMBER RealNumber))) |
Merge.kif 2020-2024 | 数量 是 负实数 的 instance 若且唯若 那个 数量 是 lessThan 0 和 那个 数量 是 实数 的 instance |
| (<=> (instance ?NUMBER NonnegativeRealNumber) (and (greaterThanOrEqualTo ?NUMBER 0) (instance ?NUMBER RealNumber))) |
Merge.kif 1998-2002 | 数量 是 非负实数 的 instance 若且唯若 那个 数量 是 greaterThanOrEqualTo 0 和 那个 数量 是 实数 的 instance |
| (<=> (instance ?NUMBER PositiveRealNumber) (and (greaterThan ?NUMBER 0) (instance ?NUMBER RealNumber))) |
Merge.kif 2009-2013 | 数量 是 正实数 的 instance 若且唯若 那个 数量 是 greaterThan 0 和 那个 数量 是 实数 的 instance |
| (=> (average ?LIST ?AVERAGE) (forall (?LISTITEM) (=> (inList ?LISTITEM ?LIST) (instance ?LISTITEM RealNumber)))) |
Merge.kif 5465-5470 |
|
|
|
