TreeView Knowledge Base Browser

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 simplified definition (without tree view)
Show simplified definition (with tree view)

KB Term:			Term intersection

English Word: