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

Formal Language: 



KB Term:  Term intersection
English Word: 

  exhaustiveDecomposition

Sigma KEE - exhaustiveDecomposition
exhaustiveDecomposition

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


(documentation exhaustiveDecomposition ChineseLanguage "C ClassexhaustiveDecomposition 是C的一组子类别, 而C的每一个实例就是这个组内其中一个子类别的一个实例。按: 这并不一定是意会着这个组的单元都不相交 (可参考 partition - 一个 partition 是一个已列举尽 不相交的掏空成分。 ") chinese_format.kif 1511-1514
(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 552-556
(domain exhaustiveDecomposition 1 Class) Merge.kif 548-548 The number 1 argument of exhaustive decomposition is an instance of class
(domain exhaustiveDecomposition 2 Class) Merge.kif 549-549 The number 2 argument of exhaustive decomposition is an instance of class
(instance exhaustiveDecomposition Predicate) Merge.kif 546-546 exhaustive decomposition is an instance of predicate
(instance exhaustiveDecomposition VariableArityRelation) Merge.kif 547-547 exhaustive decomposition is an instance of variable arity relation
(relatedInternalConcept exhaustiveDecomposition partition) Merge.kif 550-550 exhaustive decomposition is internally related to partition

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 307-307
(relatedInternalConcept disjointDecomposition exhaustiveDecomposition) Merge.kif 568-568 disjoint decomposition is internally related to exhaustive decomposition
(termFormat ChineseLanguage exhaustiveDecomposition "彻底分解") domainEnglishFormat.kif 22699-22699
(termFormat ChineseLanguage exhaustiveDecomposition "彻底的分拆") chinese_format.kif 300-300
(termFormat ChineseTraditionalLanguage exhaustiveDecomposition "徹底分解") domainEnglishFormat.kif 22698-22698
(termFormat EnglishLanguage exhaustiveDecomposition "exhaustive decomposition") domainEnglishFormat.kif 22697-22697

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


(=>
    (exhaustiveDecomposition ?CLASS @ROW)
    (forall (?OBJ)
        (=>
            (instance ?OBJ ?CLASS)
            (exists (?ITEM)
                (and
                    (inList ?ITEM
                        (ListFn @ROW))
                    (instance ?OBJ ?ITEM))))))
Merge.kif 2829-2837
(=>
    (exhaustiveDecomposition @ROW)
    (=>
        (inList ?ELEMENT
            (ListFn @ROW))
        (instance ?ELEMENT Class)))
Merge.kif 558-562

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


(<=>
    (partition @ROW)
    (and
        (exhaustiveDecomposition @ROW)
        (disjointDecomposition @ROW)))
Merge.kif 590-594 @ROW is exhaustively partitioned into @ROW if and only if @ROW is covered by @ROW and @ROW is disjointly decomposed into @ROW

Show without tree


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