| appearance as argument number 1 |
|
| (documentation FloorFn ChineseLanguage "(FloorFn ?NUMBER) 得出小于或等于 RealNumber ?NUMBER 的最大 Integer。") | chinese_format.kif 2234-2235 | |
| (documentation FloorFn EnglishLanguage "(FloorFn ?NUMBER) returns the largest Integer less than or equal to the RealNumber ?NUMBER.") | Merge.kif 4735-4736 | |
| (domain FloorFn 1 RealNumber) | Merge.kif 4732-4732 | |
| (instance FloorFn TotalValuedRelation) | Merge.kif 4731-4731 | |
| (instance FloorFn UnaryFunction) | Merge.kif 4730-4730 | |
| (range FloorFn Integer) | Merge.kif 4733-4733 |
| appearance as argument number 2 |
|
|
| (format ChineseLanguage FloorFn "取 %1 的底整数") | chinese_format.kif 698-698 | |
| (format EnglishLanguage FloorFn "the largest integer less than or equal to %1") | english_format.kif 700-700 | |
| (termFormat ChineseLanguage FloorFn "地板") | domainEnglishFormat.kif 24255-24255 | |
| (termFormat ChineseLanguage FloorFn "底整数函数") | chinese_format.kif 699-699 | |
| (termFormat ChineseTraditionalLanguage FloorFn "地板") | domainEnglishFormat.kif 24254-24254 | |
| (termFormat EnglishLanguage FloorFn "floor") | domainEnglishFormat.kif 24253-24253 |
| antecedent |
|
|
| (=> (and (not (equal ?NUMBER2 0)) (equal (AdditionFn (MultiplicationFn (FloorFn (DivisionFn ?NUMBER1 ?NUMBER2)) ?NUMBER2) ?NUMBER) ?NUMBER1)) (equal (RemainderFn ?NUMBER1 ?NUMBER2) ?NUMBER)) |
Merge.kif 5021-5032 |
| consequent |
|
|
| (=> (and (equal (RemainderFn ?NUMBER1 ?NUMBER2) ?NUMBER) (not (equal ?NUMBER2 0))) (equal (AdditionFn (MultiplicationFn (FloorFn (DivisionFn ?NUMBER1 ?NUMBER2)) ?NUMBER2) ?NUMBER) ?NUMBER1)) |
Merge.kif 5008-5019 |
|
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 3.0 is open source software produced by Articulate Software and its partners