| RealNumber
| |
| appearance as argument number 1 |
|
|
| (documentation RealNumber ChineseLanguage "任何可以表达为一个（可能是无限的)十进制的 Number， 即任何在数字线上佔有一席位 Number。") | chinese_format.kif 1737-1738 | |
| (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 1841-1843 | |
| (externalImage RealNumber "http://upload.wikimedia.org/wikipedia/commons/ 0/ 09/ Number-line.gif") | pictureList.kif 11751-11751 | |
| (externalImage RealNumber "http://upload.wikimedia.org/wikipedia/commons/ 9/ 98/ Real_Number_Line.PNG") | pictureList.kif 10233-10233 | |
| (externalImage RealNumber "http://upload.wikimedia.org/wikipedia/commons/ f/ fd/ Recta_real_entero_o_decimal_exacto.png") | pictureList.kif 11750-11750 | |
| (partition RealNumber NegativeRealNumber NonnegativeRealNumber) | Merge.kif 1838-1838 | |
| (partition RealNumber RationalNumber IrrationalNumber) | Merge.kif 1839-1839 | |
| (subclass RealNumber Number) | Merge.kif 1837-1837 |
| appearance as argument number 2 |
|
|
| appearance as argument number 3 |
|
|
| (domain AbsoluteValueFn 1 RealNumber) | Merge.kif 4672-4672 | |
| (domain AdditionFn 1 RealNumber) | Merge.kif 4622-4622 | |
| (domain AdditionFn 2 RealNumber) | Merge.kif 4623-4623 | |
| (domain ArcCosineFn 1 RealNumber) | Merge.kif 5165-5165 | |
| (domain ArcSineFn 1 RealNumber) | Merge.kif 5175-5175 | |
| (domain ArcTangentFn 1 RealNumber) | Merge.kif 5155-5155 | |
| (domain CeilingFn 1 RealNumber) | Merge.kif 4693-4693 | |
| (domain DenominatorFn 1 RealNumber) | Merge.kif 4720-4720 | |
| (domain DivisionFn 1 RealNumber) | Merge.kif 4652-4652 | |
| (domain DivisionFn 2 RealNumber) | Merge.kif 4653-4653 | |
| (domain ExponentiationFn 1 RealNumber) | Merge.kif 4729-4729 | |
| (domain FloorFn 1 RealNumber) | Merge.kif 4738-4738 | |
| (domain IntegerSquareRootFn 1 RealNumber) | Merge.kif 4833-4833 | |
| (domain LogFn 1 RealNumber) | Merge.kif 4885-4885 | |
| (domain MeasureFn 1 RealNumber) | Merge.kif 6258-6258 | |
| (domain MultiplicationFn 1 RealNumber) | Merge.kif 4609-4609 | |
| (domain MultiplicationFn 2 RealNumber) | Merge.kif 4610-4610 | |
| (domain NumeratorFn 1 RealNumber) | Merge.kif 4946-4946 | |
| (domain ReciprocalFn 1 RealNumber) | Merge.kif 4980-4980 | |
| (domain RoundFn 1 RealNumber) | Merge.kif 5076-5076 | |
| (domain SignumFn 1 RealNumber) | Merge.kif 5095-5095 | |
| (domain SineFn 1 RealNumber) | Merge.kif 5117-5117 | |
| (domain SquareRootFn 1 RealNumber) | Merge.kif 5125-5125 | |
| (domain SubtractionFn 1 RealNumber) | Merge.kif 4636-4636 | |
| (domain SubtractionFn 2 RealNumber) | Merge.kif 4637-4637 | |
| Display limited to 25 items. Show next 25 | ||
| Display limited to 25 items. Show next 25 |
| 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.0 ?NUMBER1))))) |
Merge.kif 4678-4689 | |
| (=> (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 3447-3467 | |
| (=> (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 ?SELLING ?ITEM)))))))) (equal (ASPFn ?SELLINGS) (DivisionFn ?GMV ?TOTAL))) |
UXExperimentalTerms.kif 3490-3510 | |
| (=> (instance ?DEGREE RealNumber) (equal (TangentFn ?DEGREE) (DivisionFn (SineFn ?DEGREE) (CosineFn ?DEGREE)))) |
Merge.kif 5145-5151 | |
| (=> (instance ?N RealNumber) (equal (MeasureFn ?N Horsepower) (MeasureFn (MultiplicationFn ?N 746) Watt))) |
Merge.kif 6812-6816 |
| consequent |
|
|
| (<=> (instance ?NUMBER NegativeRealNumber) (and (lessThan ?NUMBER 0) (instance ?NUMBER RealNumber))) |
Merge.kif 1894-1898 | |
| (<=> (instance ?NUMBER NonnegativeRealNumber) (and (greaterThanOrEqualTo ?NUMBER 0) (instance ?NUMBER RealNumber))) |
Merge.kif 1872-1876 | |
| (<=> (instance ?NUMBER PositiveRealNumber) (and (greaterThan ?NUMBER 0) (instance ?NUMBER RealNumber))) |
Merge.kif 1883-1887 | |
| (=> (average ?LIST ?AVERAGE) (forall (?LISTITEM) (=> (inList ?LISTITEM ?LIST) (instance ?LISTITEM RealNumber)))) |
Merge.kif 5275-5280 |
|
|
|