| appearance as argument number 1 |
|
| (documentation RemainderFn ChineseLanguage "(RemainderFn ?NUMBER ?DIVISOR)是数字 ?NUMBER 除以数字 ?DIVISOR 的余数，商数的正负值与 ?DIVISOR 相同。") | chinese_format.kif 2267-2268 | |
| (documentation RemainderFn EnglishLanguage "(RemainderFn ?NUMBER ?DIVISOR) is the remainder of the number ?NUMBER divided by the number ?DIVISOR. The result has the same sign as ?DIVISOR.") | Merge.kif 4846-4848 | |
| (domain RemainderFn 1 Integer) | Merge.kif 4842-4842 | The number 1 argument of remainder is an instance of integer |
| (domain RemainderFn 2 Integer) | Merge.kif 4843-4843 | The number 2 argument of remainder is an instance of integer |
| (instance RemainderFn BinaryFunction) | Merge.kif 4839-4839 | Remainder is an instance of binary function |
| (instance RemainderFn PartialValuedRelation) | Merge.kif 4841-4841 | Remainder is an instance of partial valued relation |
| (range RemainderFn Integer) | Merge.kif 4844-4844 | The range of remainder is an instance of integer |
| appearance as argument number 2 |
|
|
| (format ChineseLanguage RemainderFn "%1 模除 %2") | chinese_format.kif 722-722 | |
| (format EnglishLanguage RemainderFn "%1 mod %2") | english_format.kif 727-727 | |
| (termFormat ChineseLanguage RemainderFn "余函数") | chinese_format.kif 723-723 | |
| (termFormat ChineseLanguage RemainderFn "剩余") | domainEnglishFormat.kif 49340-49340 | |
| (termFormat ChineseTraditionalLanguage RemainderFn "剩餘") | domainEnglishFormat.kif 49339-49339 | |
| (termFormat EnglishLanguage RemainderFn "remainder") | domainEnglishFormat.kif 49338-49338 |
| antecedent |
|
|
| (<=> (equal (RemainderFn ?NUMBER1 ?NUMBER2) ?NUMBER) (equal (AdditionFn (MultiplicationFn (FloorFn (DivisionFn ?NUMBER1 ?NUMBER2)) ?NUMBER2) ?NUMBER) ?NUMBER1)) |
Merge.kif 4850-4852 | An integer mod another integer is equal to a third integer if and only if (the largest integer less than or equal to the integer and the other integer and the other integer and the third integer) is equal to the integer |
| (=> (equal (RemainderFn ?NUMBER1 ?NUMBER2) ?NUMBER) (equal (SignumFn ?NUMBER2) (SignumFn ?NUMBER))) |
Merge.kif 4854-4856 |
|
| consequent |
|
|
| (=> (and (instance ?LEAP LeapYear) (instance ?LEAP (YearFn ?NUMBER))) (or (and (equal (RemainderFn ?NUMBER 4) 0) (not (equal (RemainderFn ?NUMBER 100) 0))) (equal (RemainderFn ?NUMBER 400) 0))) |
Merge.kif 8412-8420 |
|
| (=> (equal (GreatestCommonDivisorFn @ROW) ?NUMBER) (forall (?ELEMENT) (=> (inList ?ELEMENT (ListFn @ROW)) (equal (RemainderFn ?ELEMENT ?NUMBER) 0)))) |
Merge.kif 4630-4635 |
|
| (=> (equal (GreatestCommonDivisorFn @ROW) ?NUMBER) (not (exists (?GREATER) (and (greaterThan ?GREATER ?NUMBER) (forall (?ELEMENT) (=> (inList ?ELEMENT (ListFn @ROW)) (equal (RemainderFn ?ELEMENT ?GREATER) 0))))))) |
Merge.kif 4637-4645 |
|
| (=> (equal (LeastCommonMultipleFn @ROW) ?NUMBER) (forall (?ELEMENT) (=> (inList ?ELEMENT (ListFn @ROW)) (equal (RemainderFn ?NUMBER ?ELEMENT) 0)))) |
Merge.kif 4703-4708 |
|
| (=> (equal (LeastCommonMultipleFn @ROW) ?NUMBER) (not (exists (?LESS) (and (lessThan ?LESS ?NUMBER) (forall (?ELEMENT) (=> (inList ?ELEMENT (ListFn @ROW)) (equal (RemainderFn ?LESS ?ELEMENT) 0))))))) |
Merge.kif 4710-4718 |
|
| (=> (instance ?NUMBER EvenInteger) (equal (RemainderFn ?NUMBER 2) 0)) |
Merge.kif 4858-4860 |
|
| (=> (instance ?NUMBER OddInteger) (equal (RemainderFn ?NUMBER 2) 1)) |
Merge.kif 4862-4864 |
|
| (=> (instance ?PRIME PrimeNumber) (forall (?NUMBER) (=> (equal (RemainderFn ?PRIME ?NUMBER) 0) (or (equal ?NUMBER 1) (equal ?NUMBER ?PRIME))))) |
Merge.kif 4866-4873 |
|
|
Show full definition with tree view
Show simplified definition (without tree view)
Show simplified definition (with tree view)
|
|
Sigma web home Suggested Upper Merged Ontology (SUMO) web home
Sigma version 2.99c (>= 2017/11/20) is open source software produced by Articulate Software and its partners