| NegativeRealNumber(negative real number)
| | indirect_correlation, negative, negative_correlation |
| appearance as argument number 1 |
|
|
| (documentation NegativeRealNumber ChineseLanguage "这是一个小于零的 RealNumber。") | chinese_format.kif 1747-1747 | |
| (documentation NegativeRealNumber EnglishLanguage "A RealNumber that is less than zero.") | Merge.kif 1945-1946 | |
| (documentation NegativeRealNumber JapaneseLanguage "ゼロ未満の RealNumber 。") | japanese_format.kif 355-355 | |
| (externalImage NegativeRealNumber "http://upload.wikimedia.org/wikipedia/ commons/ 0/ 09/ Number-line.gif") | pictureList.kif 10145-10145 | |
| (subclass NegativeRealNumber RealNumber) | Merge.kif 1943-1943 | Negative real number is a subclass of real number |
| appearance as argument number 2 |
|
|
| antecedent |
|
|
| (<=> (instance ?NUMBER NegativeRealNumber) (and (lessThan ?NUMBER 0) (instance ?NUMBER RealNumber))) |
Merge.kif 1948-1952 | A real number is an instance of negative real number if and only if the real number is less than 0 and the real number is an instance of real number |
| (=> (instance ?NUMBER NegativeRealNumber) (equal (SignumFn ?NUMBER) -1)) |
Merge.kif 5206-5208 |
|
| consequent |
|
|
| (<=> (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 4769-4780 | The absolute value of a real number is equal to a nonnegative real number and the real number is an instance of real number and the nonnegative real number is an instance of real number if and only if the real number is an instance of nonnegative real number and the real number is equal to the nonnegative real number or the real number is an instance of negative real number and the nonnegative real number is equal to (0.0 and the real number) |
|
|
|