Browsing Interface : Welcome guest : log in
|
Browsing Interface : Welcome guest : log in |
[
Home |
Graph |
LogLearn |
Editor |
]
KB:
Language:
Formal Language:
|
| partition |
| appearance as argument number 1 |
|
| (instance partition Predicate) | Merge.kif 572-572 | partition is an instance of predicate |
| (instance partition VariableArityRelation) | Merge.kif 573-573 | partition is an instance of variable arity relation |
| (domain partition 1 Class) | Merge.kif 574-574 | The number 1 argument of partition is an instance of class |
| (domain partition 2 Class) | Merge.kif 575-575 | The number 2 argument of partition is an instance of class |
| (documentation partition EnglishLanguage "A partition of a Class C is a set of mutually disjoint classes (a subclass partition) which covers C. Every instance of C is an instance of exactly one of the subclasses in the partition.") | Merge.kif 577-580 | The number 2 argument of partition is an instance of class |
| appearance as argument number 2 |
|
|
| (relatedInternalConcept exhaustiveDecomposition partition) | Merge.kif 542-542 | exhaustive decomposition is internally related to partition |
| (termFormat EnglishLanguage partition "partition") | domainEnglishFormat.kif 44561-44561 | exhaustive decomposition is internally related to partition |
| (termFormat ChineseTraditionalLanguage partition "劃分") | domainEnglishFormat.kif 44562-44562 | exhaustive decomposition is internally related to partition |
| (termFormat ChineseLanguage partition "划分") | domainEnglishFormat.kif 44563-44563 | exhaustive decomposition is internally related to partition |
| (format EnglishLanguage partition "%1 is %n exhaustively partitioned into %*{2-}[,]") | english_format.kif 316-316 | exhaustive decomposition is internally related to partition |
| antecedent |
|
|
| (=> (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 |
| (=> (partition ?SUPER ?SUB1 ?SUB2) (partition ?SUPER ?SUB2 ?SUB1)) |
Merge.kif 594-596 | If X is exhaustively partitioned into Y and Z, then X is exhaustively partitioned into Z and Y |
| (=> (and (partition ?SUPER ?SUB1 ?SUB2) (instance ?INST ?SUPER) (not (instance ?INST ?SUB1))) (instance ?INST ?SUB2)) |
Merge.kif 598-604 | If X is exhaustively partitioned into Y and Z, W is an instance of X, and W is not an instance of Y, then W is an instance of Z |
| consequent |
|
|
| (=> (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 |
| (=> (partition ?SUPER ?SUB1 ?SUB2) (partition ?SUPER ?SUB2 ?SUB1)) |
Merge.kif 594-596 | If X is exhaustively partitioned into Y and Z, then X is exhaustively partitioned into Z and Y |
| appearance as argument number 0 |
|
|
|