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

Formal Language: 



KB Term:  Term intersection
English Word: 

Sigma KEE - exhaustiveDecomposition
exhaustiveDecomposition

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


(documentation exhaustiveDecomposition ChineseLanguage "C ClassexhaustiveDecomposition 是C的一组子类别, 而C的每一个实例就是这个组内其中一个子类别的一个实例。按: 这并不一定是意会着这个组的单元都不相交 (可参考 partition - 一个 partition 是一个已列举尽 不相交的掏空成分。 ") Merge.kif 794-797
(documentation exhaustiveDecomposition EnglishLanguage "An exhaustiveDecomposition of a Class C is a set of subclasses of C such that every instance of C is an instance of one of the subclasses in the set. Note: this does not necessarily mean that the elements of the set are disjoint (see partition - a partition is a disjoint exhaustive decomposition).") Merge.kif 788-792
(documentation exhaustiveDecomposition JapaneseLanguage "Class C の exhaustiveDecomposition は、Cのサブクラスのセットで、Cのすべてのインスタンスはセット内のサブクラスの1つのインスタンスである。 注:これは必ずしもセットの要素が互いに素であることを意味しているわけではない(partitionを参照 - a partition は互いに素な完全分解である)。") Merge.kif 799-802
(documentation exhaustiveDecomposition SpanishLanguage "Una exhaustiveDecomposition de una Class C es un conjunto de la subclase C de tal manera que cada instancia de C es una instancia de una de las subclases del conjunto. Nota: Eso no significa necesariamente que los elementos del conjunto son disjuntos. (Véase partition - una partition es una descomposición exhaustiva y disjunta).") Merge.kif 804-808
(domain exhaustiveDecomposition 1 Class) Merge.kif 784-784
(domain exhaustiveDecomposition 2 Class) Merge.kif 785-785
(instance exhaustiveDecomposition Predicate) Merge.kif 782-782
(instance exhaustiveDecomposition VariableArityRelation) Merge.kif 783-783
(relatedInternalConcept exhaustiveDecomposition partition) Merge.kif 786-786

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


(format ChineseLanguage exhaustiveDecomposition " %*{2-}[,] %n 涵盖 %1") chinese_format.kif 299-299
(format EnglishLanguage exhaustiveDecomposition "%1 is %n covered by %*{2-}[,]") english_format.kif 424-424
(format JapaneseLanguage exhaustiveDecomposition "%1 は %*{2-}[,] によって covered され %n") english_format.kif 425-425
(relatedInternalConcept disjointDecomposition exhaustiveDecomposition) Merge.kif 820-820
(termFormat ChineseLanguage exhaustiveDecomposition "彻底分解") domainEnglishFormat.kif 22705-22705
(termFormat ChineseLanguage exhaustiveDecomposition "彻底的分拆") chinese_format.kif 300-300
(termFormat ChineseTraditionalLanguage exhaustiveDecomposition "徹底分解") domainEnglishFormat.kif 22704-22704
(termFormat EnglishLanguage exhaustiveDecomposition "exhaustive decomposition") domainEnglishFormat.kif 22703-22703

antecedent
-------------------------


(=>
    (exhaustiveDecomposition ?CLASS @ROW)
    (forall (?OBJ)
        (=>
            (instance ?OBJ ?CLASS)
            (exists (?ITEM)
                (and
                    (inList ?ITEM
                        (ListFn @ROW))
                    (instance ?OBJ ?ITEM))))))
Merge.kif 4711-4719
(=>
    (exhaustiveDecomposition @ROW)
    (=>
        (inList ?ELEMENT
            (ListFn @ROW))
        (instance ?ELEMENT Class)))
Merge.kif 810-814

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


(<=>
    (partition @ROW)
    (and
        (exhaustiveDecomposition @ROW)
        (disjointDecomposition @ROW)))
Merge.kif 862-866