Browsing Interface : Welcome guest : log in
|
Browsing Interface : Welcome guest : log in |
[
Home |
Graph |
LogLearn |
Editor |
]
KB:
Language:
Formal Language:
|
| disjointDecomposition |
| appearance as argument number 1 |
|
| appearance as argument number 2 |
|
|
| (termFormat EnglishLanguage disjointDecomposition "disjoint decomposition") | domainEnglishFormat.kif 19854-19854 | |
| (termFormat ChineseTraditionalLanguage disjointDecomposition "不相交分解") | domainEnglishFormat.kif 19855-19855 | |
| (termFormat ChineseLanguage disjointDecomposition "不相交分解") | domainEnglishFormat.kif 19856-19856 | |
| (format EnglishLanguage disjointDecomposition "%1 is %n disjointly decomposed into %*{2-}[,]") | english_format.kif 292-292 |
| antecedent |
|
|
| (=> (disjointDecomposition @ROW) (=> (inList ?ELEMENT (ListFn @ROW)) (instance ?ELEMENT Class))) |
Merge.kif 566-570 | Assuming @ROW is disjointly decomposed into @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 |
| (=> (disjointDecomposition ?CLASS @ROW) (forall (?ITEM) (=> (inList ?ITEM (ListFn @ROW)) (subclass ?ITEM ?CLASS)))) |
Merge.kif 3061-3066 | If X is disjointly decomposed into @ROW, then For all Class Z: if Z is a member of (@ROW), then Z is a subclass of X |
| (=> (disjointDecomposition ?CLASS @ROW) (forall (?ITEM1 ?ITEM2) (=> (and (inList ?ITEM1 (ListFn @ROW)) (inList ?ITEM2 (ListFn @ROW)) (not (equal ?ITEM1 ?ITEM2))) (disjoint ?ITEM1 ?ITEM2)))) |
Merge.kif 3068-3077 | If X is disjointly decomposed into @ROW, then For all Classes Z and W: if Z is a member of (@ROW), W is a member of (@ROW), and equal Z and W, then Z is disjoint from W |
| (=> (disjointDecomposition ?CLASS ?ROW1 ?ROW2 ?ROW3) (and (disjoint ?ROW1 ?ROW2) (disjoint ?ROW2 ?ROW3) (disjoint ?ROW3 ?ROW1))) |
Merge.kif 3079-3084 | If X is disjointly decomposed into Y, Z, and W, then Y is disjoint from Z, Z is disjoint from W, and W is disjoint from Y |
| consequent |
|
|
| (=> (partition @ROW) (and (exhaustiveDecomposition @ROW) (disjointDecomposition @ROW))) |
Merge.kif 582-586 | 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 |
|
|
|