Browsing Interface : Welcome guest : log in
|
Browsing Interface : Welcome guest : log in |
[
Home |
Graph |
LogLearn |
Editor |
]
KB:
Language:
Formal Language:
|
| ReciprocalFn |
| appearance as argument number 1 |
|
| (instance ReciprocalFn UnaryFunction) | Merge.kif 5179-5179 | 互相 is an instance of unary function |
| (instance ReciprocalFn TotalValuedRelation) | Merge.kif 5181-5181 | 互相 is an instance of total valued relation |
| (domain ReciprocalFn 1 RealNumber) | Merge.kif 5182-5182 | The number 1 argument of 互相 is an instance of real number |
| (range ReciprocalFn RealNumber) | Merge.kif 5183-5183 | The range of 互相 is an instance of real number |
| (documentation ReciprocalFn EnglishLanguage "(ReciprocalFn ?NUMBER) is the reciprocal element of ?NUMBER with respect to the multiplication operator (MultiplicationFn), i.e. 1/ ?NUMBER. Not all numbers have a reciprocal element. For example the number 0 does not. If a number ?NUMBER has a reciprocal ?RECIP, then the product of ?NUMBER and ?RECIP will be 1, e.g. 3*1/ 3 = 1. The reciprocal of an element is equal to applying the ExponentiationFn function to the element to the power -1.") | Merge.kif 5185-5192 | The range of 互相 is an instance of real number |
| appearance as argument number 2 |
|
|
| consequent |
|
|
| (=> (instance ?NUMBER Integer) (equal (ReciprocalFn ?NUMBER) (ExponentiationFn ?NUMBER -1))) |
Merge.kif 5194-5196 | If X is an instance of integer, then equal the reciprocal of X and X raised to the power -1 |
| (=> (and (instance ?NUMBER Integer) (not (equal ?NUMBER 0))) (equal 1 (MultiplicationFn ?NUMBER (ReciprocalFn ?NUMBER)))) |
Merge.kif 5198-5203 | If X is an instance of integer and equal X and 0, then equal 1, X, and the reciprocal of X |
|