multiplicativeFactor - Sigma Knowledge base Browser

appearance as argument number 1

(documentation multiplicativeFactor EnglishLanguage "(multiplicativeFactor ?NUMBER1 ?NUMBER2)means that ?NUMBER1 is a factor of ?NUMBER2, i.e. ?NUMBER1 can be multiplied by some Integer to give ?NUMBER2 as a result.")	Merge.kif 5002-5004
(instance multiplicativeFactor BinaryPredicate)	Merge.kif 5006-5006	multiplicative factor is an instance of binary predicate
(instance multiplicativeFactor TransitiveRelation)	Merge.kif 5007-5007	multiplicative factor is an instance of transitive relation
(domain multiplicativeFactor 1 Integer)	Merge.kif 5008-5008	The number 1 argument of multiplicative factor is an instance of integer
(domain multiplicativeFactor 2 Integer)	Merge.kif 5009-5009	The number 2 argument of multiplicative factor is an instance of integer

appearance as argument number 2

(format EnglishLanguage multiplicativeFactor "%2 is %n a multiplicative factor of %1")	domainEnglishFormat.kif 1765-1765
(format ChineseTraditionalLanguage multiplicativeFactor "%2 %n 是 %1 的 multiplicative 因子")	domainEnglishFormat.kif 1766-1766
(format ChineseLanguage multiplicativeFactor "%2 %n 是 %1 的 multiplicative 因子")	domainEnglishFormat.kif 1767-1767
(termFormat EnglishLanguage multiplicativeFactor "multiplicative factor")	domainEnglishFormat.kif 39193-39193
(termFormat ChineseTraditionalLanguage multiplicativeFactor "乘法因子")	domainEnglishFormat.kif 39194-39194
(termFormat ChineseLanguage multiplicativeFactor "乘法因子")	domainEnglishFormat.kif 39195-39195

antecedent

(=>
    (multiplicativeFactor ?N1 ?N2)
    (exists (?I)
        (and
            (instance ?I Integer)
            (equal ?N2
                (MultiplicationFn ?N1 ?I)))))

If X is a multiplicative factor of Y, then there exists Z such that Z is an instance of integer, equal X, Y, and Z