exhaustiveDecomposition - Sigma Knowledge base Browser

appearance as argument number 1

(instance exhaustiveDecomposition Predicate)	Merge.kif 538-538	exhaustive decomposition is an instance of predicate
(instance exhaustiveDecomposition VariableArityRelation)	Merge.kif 539-539	exhaustive decomposition is an instance of variable arity relation
(domain exhaustiveDecomposition 1 Class)	Merge.kif 540-540	The number 1 argument of exhaustive decomposition is an instance of class
(domain exhaustiveDecomposition 2 Class)	Merge.kif 541-541	The number 2 argument of exhaustive decomposition is an instance of class
(relatedInternalConcept exhaustiveDecomposition partition)	Merge.kif 542-542	exhaustive decomposition is internally related to partition
(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 544-548	exhaustive decomposition is internally related to partition

appearance as argument number 2

(relatedInternalConcept disjointDecomposition exhaustiveDecomposition)	Merge.kif 560-560	disjoint decomposition is internally related to exhaustive decomposition
(termFormat EnglishLanguage exhaustiveDecomposition "exhaustive decomposition")	domainEnglishFormat.kif 22771-22771	disjoint decomposition is internally related to exhaustive decomposition
(termFormat ChineseTraditionalLanguage exhaustiveDecomposition "徹底分解")	domainEnglishFormat.kif 22772-22772	disjoint decomposition is internally related to exhaustive decomposition
(termFormat ChineseLanguage exhaustiveDecomposition "彻底分解")	domainEnglishFormat.kif 22773-22773	disjoint decomposition is internally related to exhaustive decomposition
(format EnglishLanguage exhaustiveDecomposition "%1 is %n covered by %*{2-}[,]")	english_format.kif 304-304	disjoint decomposition is internally related to exhaustive decomposition

antecedent

(=> (exhaustiveDecomposition @ROW) (=> (inList ?ELEMENT (ListFn @ROW)) (instance ?ELEMENT Class)))	Merge.kif 550-554	Assuming @ROW is covered by @ROW, it follows that: if Y is a member of (@ROW), then Y is an instance of class
(=> (and (exhaustiveDecomposition @ROW) (disjointDecomposition @ROW)) (partition @ROW))	Merge.kif 588-592	If @ROW is covered by @ROW and @ROW is disjointly decomposed into @ROW, then @ROW is exhaustively partitioned into @ROW
(=> (exhaustiveDecomposition ?CLASS @ROW) (forall (?OBJ) (=> (instance ?OBJ ?CLASS) (exists (?ITEM) (and (inList ?ITEM (ListFn @ROW)) (instance ?OBJ ?ITEM))))))	Merge.kif 3051-3059	If X is covered by @ROW, then For all Entity Z: if Z is an instance of X, then there exists W such that W is a member of (@ROW) and Z is an instance of W

consequent

(=>
    (partition @ROW)
    (and
        (exhaustiveDecomposition @ROW)
        (disjointDecomposition @ROW)))

If @ROW is exhaustively partitioned into @ROW, then @ROW is covered by @ROW and @ROW is disjointly decomposed into @ROW

appearance as argument number 0

(exhaustiveDecomposition UniformResourceIdentifier UniformResourceLocator UniformResourceName)	QoSontology.kif 1799-1799	Uniform resource identifier is covered by uniform resource locator and uniform resource name
(exhaustiveDecomposition VacciniaVirion IntracellularMatureVirionVaccinia IntracellularEnvelopedVirionVaccinia ExtracellularEnvelopedVirionVaccinia ProgenyVacciniaVirusImmature)	VirusProteinAndCellPart.kif 198-198	Vaccinia virion is covered by intracellular mature virion vaccinia, intracellular enveloped virion vaccinia, extracellular enveloped virion vaccinia, and progeny vaccinia virus immature