Browsing Interface : Welcome guest : log in
|
Browsing Interface : Welcome guest : log in |
[
Home |
Graph |
LogLearn |
Editor |
]
KB:
Language:
Formal Language:
|
| SignumFn |
| appearance as argument number 1 |
|
| (instance SignumFn UnaryFunction) | Merge.kif 5299-5299 | Signum is an instance of unary function |
| (instance SignumFn TotalValuedRelation) | Merge.kif 5300-5300 | Signum is an instance of total valued relation |
| (domain SignumFn 1 RealNumber) | Merge.kif 5301-5301 | The number 1 argument of signum is an instance of real number |
| (range SignumFn Integer) | Merge.kif 5302-5302 | The range of signum is an instance of integer |
| (documentation SignumFn EnglishLanguage "(SignumFn ?NUMBER) denotes the sign of ?NUMBER. This is one of the following values: -1, 1, or 0.") | Merge.kif 5304-5305 | The range of signum is an instance of integer |
| appearance as argument number 2 |
|
|
| consequent |
|
|
| (=> (and (equal (RemainderFn ?NUMBER1 ?NUMBER2) ?NUMBER) (not (equal ?NUMBER 0)) (not (equal ?NUMBER1 0)) (not (equal ?NUMBER2 0))) (equal (SignumFn ?NUMBER2) (SignumFn ?NUMBER))) |
Merge.kif 5242-5254 | If equal X mod Y and Z, equal Z and 0, equal X and 0, and equal Y and 0, then equal the sign of Y and the sign of Z |
| (=> (instance ?NUMBER NonnegativeRealNumber) (or (equal (SignumFn ?NUMBER) 1) (equal (SignumFn ?NUMBER) 0))) |
Merge.kif 5307-5311 | If X is an instance of nonnegative real number, then equal the sign of X and 1 or equal the sign of X and 0 |
| (=> (instance ?NUMBER PositiveRealNumber) (equal (SignumFn ?NUMBER) 1)) |
Merge.kif 5313-5315 | If X is an instance of positive real number, then equal the sign of X and 1 |
| (=> (instance ?NUMBER NegativeRealNumber) (equal (SignumFn ?NUMBER) -1)) |
Merge.kif 5317-5319 | If X is an instance of negative real number, then equal the sign of X and -1 |
|