Browsing Interface : Welcome guest : log in
Home |  Graph |  ]  KB:  Language:   

Formal Language: 



KB Term:  Term intersection
English Word: 

Sigma KEE - FloorFn
FloorFn

appearance as argument number 1
-------------------------


s__documentation(s__FloorFn__m,s__ChineseLanguage,'"(FloorFn ?NUMBER) 得出小于或等于 RealNumber ?NUMBER 的最大 Integer。"')

chinese_format.kif 2234-2235
s__documentation(s__FloorFn__m,s__EnglishLanguage,'"(FloorFn ?NUMBER) returns the largest Integer less than or equal to the RealNumber ?NUMBER."')

Merge.kif 4691-4692
s__domain(s__FloorFn__m,n__1,s__RealNumber)

Merge.kif 4688-4688 The number 1 argument of floor is an instance of real number
s__instance(s__TotalValuedRelation,s__SetOrClass)

s__instance(s__FloorFn__m,s__TotalValuedRelation)

Merge.kif 4687-4687 Floor is an instance of total valued relation
s__instance(s__FloorFn__m,s__UnaryFunction)

s__instance(s__UnaryFunction,s__SetOrClass)

Merge.kif 4686-4686 Floor is an instance of unary function
s__range(s__FloorFn__m,s__Integer)

Merge.kif 4689-4689 The range of floor is an instance of integer

appearance as argument number 2
-------------------------


s__format(s__ChineseLanguage,s__FloorFn__m,'"取 %1 的底整数"')

chinese_format.kif 698-698
s__format(s__EnglishLanguage,s__FloorFn__m,'"the largest integer less than or equal to %1"')

english_format.kif 703-703
s__termFormat(s__ChineseLanguage,s__FloorFn__m,'"地板"')

domainEnglishFormat.kif 24255-24255
s__termFormat(s__ChineseLanguage,s__FloorFn__m,'"底整数函数"')

chinese_format.kif 699-699
s__termFormat(s__ChineseTraditionalLanguage,s__FloorFn__m,'"地板"')

domainEnglishFormat.kif 24254-24254
s__termFormat(s__EnglishLanguage,s__FloorFn__m,'"floor"')

domainEnglishFormat.kif 24253-24253

consequent
-------------------------


( ! [V__NUMBER1,V__NUMBER2,V__NUMBER] :
   (((s__instance(V__NUMBER1,s__Integer) &
         s__instance(V__NUMBER2,s__Integer) &
         s__instance(V__NUMBER,s__Integer))
       =>
       ((((s__RemainderFn(V__NUMBER1,V__NUMBER2)
             = V__NUMBER)
           =>
           (s__AdditionFn(s__MultiplicationFn(s__FloorFn(s__DivisionFn(V__NUMBER1,V__NUMBER2))
        ,V__NUMBER2)
      ,V__NUMBER)
     = V__NUMBER1))
&
((s__AdditionFn(s__MultiplicationFn(s__FloorFn(s__DivisionFn(V__NUMBER1,V__NUMBER2))
,V__NUMBER2)
,V__NUMBER)
= V__NUMBER1)
=>
(s__RemainderFn(V__NUMBER1,V__NUMBER2)
= V__NUMBER)))))
)
)

Merge.kif 4941-4943 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


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