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

Formal Language: 



KB Term:  Term intersection
English Word: 

Sigma KEE - disjointDecomposition
disjointDecomposition

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


s__documentation(s__disjointDecomposition__m,s__ChineseLanguage,'"C ClassdisjointDecomposition 是C的一组相互 disjoint 的子类别。"')

chinese_format.kif 1515-1516
s__documentation(s__disjointDecomposition__m,s__EnglishLanguage,'"A disjointDecomposition of a Class C is a set of subclasses of C that are mutually disjoint."')

Merge.kif 572-573
s__domain(s__disjointDecomposition__m,n__1,s__Class)

Merge.kif 567-567 The number 1 argument of disjoint decomposition is an instance of class
s__domain(s__disjointDecomposition__m,n__2,s__Class)

Merge.kif 568-568 The number 2 argument of disjoint decomposition is an instance of class
s__instance(s__Predicate,s__SetOrClass)

s__instance(s__disjointDecomposition__m,s__Predicate)

Merge.kif 565-565 disjoint decomposition is an instance of predicate
s__instance(s__VariableArityRelation,s__SetOrClass)

s__instance(s__disjointDecomposition__m,s__VariableArityRelation)

Merge.kif 566-566 disjoint decomposition is an instance of variable arity relation
s__relatedInternalConcept(s__disjointDecomposition__m,s__disjoint__m)

Merge.kif 570-570 disjoint decomposition is internally related to disjoint
s__relatedInternalConcept(s__disjointDecomposition__m,s__exhaustiveDecomposition__m)

Merge.kif 569-569 disjoint decomposition is internally related to exhaustive decomposition

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


s__format(s__ChineseLanguage,s__disjointDecomposition__m,'"%1 %n 分拆成不相交的 %*{2-}[,]"')

chinese_format.kif 287-287
s__format(s__EnglishLanguage,s__disjointDecomposition__m,'"%1 is %n disjointly decomposed into %*{2-}[,]"')

english_format.kif 295-295
s__termFormat(s__ChineseLanguage,s__disjointDecomposition__m,'"不相交分解"')

domainEnglishFormat.kif 19845-19845
s__termFormat(s__ChineseLanguage,s__disjointDecomposition__m,'"不相交的分拆"')

chinese_format.kif 288-288
s__termFormat(s__ChineseTraditionalLanguage,s__disjointDecomposition__m,'"不相交分解"')

domainEnglishFormat.kif 19844-19844
s__termFormat(s__EnglishLanguage,s__disjointDecomposition__m,'"disjoint decomposition"')

domainEnglishFormat.kif 19843-19843

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


( ! [V__ROW3,V__ROW1,V__ROW2,V__CLASS] :
   (((s__instance(V__ROW3,s__Class) &
         s__instance(V__ROW1,s__Class) &
         s__instance(V__ROW2,s__Class) &
         s__instance(V__CLASS,s__Class))
       =>
       ((s__disjointDecomposition__4(V__CLASS,V__ROW1,V__ROW2,V__ROW3)
         =>
         ((s__disjoint(V__ROW1,V__ROW2)
           &
           s__disjoint(V__ROW2,V__ROW3)
         &
         s__disjoint(V__ROW3,V__ROW1))))))
)
)

Merge.kif 2897-2902
( ! [V__ROW7,V__ROW5,V__ROW6,V__ROW3,V__ROW4,V__ROW2,V__CLASS] :
   (((s__instance(V__ROW7,s__Class) &
         s__instance(V__ROW5,s__Class) &
         s__instance(V__ROW6,s__Class) &
         s__instance(V__ROW3,s__Class) &
         s__instance(V__ROW4,s__Class) &
         s__instance(V__ROW2,s__Class) &
         s__instance(V__CLASS,s__Class))
       =>
       ((s__disjointDecomposition__7(V__CLASS,V__ROW2,V__ROW3,V__ROW4,V__ROW5,V__ROW6,V__ROW7)
         =>
         (( ! [V__ITEM] :
             ((s__instance(V__ITEM,s__Class) =>
                 ((s__inList(V__ITEM,s__ListFn__6Fn(V__ROW2,V__ROW3,V__ROW4,V__ROW5,V__ROW6,V__ROW7))
                 =>
                 (s__subclass(V__ITEM,V__CLASS)))))))))))
)
)

( ! [V__ROW3,V__ROW4,V__ROW2,V__CLASS] :
   (((s__instance(V__ROW3,s__Class) &
         s__instance(V__ROW4,s__Class) &
         s__instance(V__ROW2,s__Class) &
         s__instance(V__CLASS,s__Class))
       =>
       ((s__disjointDecomposition__4(V__CLASS,V__ROW2,V__ROW3,V__ROW4)
         =>
         (( ! [V__ITEM] :
             ((s__instance(V__ITEM,s__Class) =>
                 ((s__inList(V__ITEM,s__ListFn__3Fn(V__ROW2,V__ROW3,V__ROW4))
                 =>
                 (s__subclass(V__ITEM,V__CLASS)))))))))))
)
)

( ! [V__ROW3,V__ROW2,V__CLASS] :
   (((s__instance(V__ROW3,s__Class) &
         s__instance(V__ROW2,s__Class) &
         s__instance(V__CLASS,s__Class))
       =>
       ((s__disjointDecomposition__3(V__CLASS,V__ROW2,V__ROW3)
         =>
         (( ! [V__ITEM] :
             ((s__instance(V__ITEM,s__Class) =>
                 ((s__inList(V__ITEM,s__ListFn__2Fn(V__ROW2,V__ROW3))
                 =>
                 (s__subclass(V__ITEM,V__CLASS)))))))))))
)
)

( ! [V__ROW5,V__ROW6,V__ROW3,V__ROW4,V__ROW2,V__CLASS] :
   (((s__instance(V__ROW5,s__Class) &
         s__instance(V__ROW6,s__Class) &
         s__instance(V__ROW3,s__Class) &
         s__instance(V__ROW4,s__Class) &
         s__instance(V__ROW2,s__Class) &
         s__instance(V__CLASS,s__Class))
       =>
       ((s__disjointDecomposition__6(V__CLASS,V__ROW2,V__ROW3,V__ROW4,V__ROW5,V__ROW6)
         =>
         (( ! [V__ITEM] :
             ((s__instance(V__ITEM,s__Class) =>
                 ((s__inList(V__ITEM,s__ListFn__5Fn(V__ROW2,V__ROW3,V__ROW4,V__ROW5,V__ROW6))
                 =>
                 (s__subclass(V__ITEM,V__CLASS)))))))))))
)
)

( ! [V__ROW5,V__ROW3,V__ROW4,V__ROW2,V__CLASS] :
   (((s__instance(V__ROW5,s__Class) &
         s__instance(V__ROW3,s__Class) &
         s__instance(V__ROW4,s__Class) &
         s__instance(V__ROW2,s__Class) &
         s__instance(V__CLASS,s__Class))
       =>
       ((s__disjointDecomposition__5(V__CLASS,V__ROW2,V__ROW3,V__ROW4,V__ROW5)
         =>
         (( ! [V__ITEM] :
             ((s__instance(V__ITEM,s__Class) =>
                 ((s__inList(V__ITEM,s__ListFn__4Fn(V__ROW2,V__ROW3,V__ROW4,V__ROW5))
                 =>
                 (s__subclass(V__ITEM,V__CLASS)))))))))))
)
)

( ! [V__ROW2,V__CLASS] :
   (((s__instance(V__ROW2,s__Class) &
         s__instance(V__CLASS,s__Class))
       =>
       ((s__disjointDecomposition__2(V__CLASS,V__ROW2)
         =>
         (( ! [V__ITEM] :
             ((s__instance(V__ITEM,s__Class) =>
                 ((s__inList(V__ITEM,s__ListFn__1Fn(V__ROW2))
                 =>
                 (s__subclass(V__ITEM,V__CLASS)))))))))))
)
)

Merge.kif 2879-2884
( ! [V__ROW5,V__ROW6,V__ROW3,V__ROW4,V__ROW2,V__CLASS] :
   (((s__instance(V__ROW5,s__Class) &
         s__instance(V__ROW6,s__Class) &
         s__instance(V__ROW3,s__Class) &
         s__instance(V__ROW4,s__Class) &
         s__instance(V__ROW2,s__Class) &
         s__instance(V__CLASS,s__Class))
       =>
       ((s__disjointDecomposition__6(V__CLASS,V__ROW2,V__ROW3,V__ROW4,V__ROW5,V__ROW6)
         =>
         (( ! [V__ITEM1, V__ITEM2] :
             (((s__instance(V__ITEM1,s__Class) &
                   s__instance(V__ITEM2,s__Class))
                 =>
                 (((s__inList(V__ITEM1,s__ListFn__5Fn(V__ROW2,V__ROW3,V__ROW4,V__ROW5,V__ROW6))
                   &
                   s__inList(V__ITEM2,s__ListFn__5Fn(V__ROW2,V__ROW3,V__ROW4,V__ROW5,V__ROW6))
               &
               ~((V__ITEM1 = V__ITEM2)))
             =>
             (s__disjoint(V__ITEM1,V__ITEM2)))))))))))
)
)

( ! [V__ROW2,V__CLASS] :
   (((s__instance(V__ROW2,s__Class) &
         s__instance(V__CLASS,s__Class))
       =>
       ((s__disjointDecomposition__2(V__CLASS,V__ROW2)
         =>
         (( ! [V__ITEM1, V__ITEM2] :
             (((s__instance(V__ITEM1,s__Class) &
                   s__instance(V__ITEM2,s__Class))
                 =>
                 (((s__inList(V__ITEM1,s__ListFn__1Fn(V__ROW2))
                   &
                   s__inList(V__ITEM2,s__ListFn__1Fn(V__ROW2))
               &
               ~((V__ITEM1 = V__ITEM2)))
             =>
             (s__disjoint(V__ITEM1,V__ITEM2)))))))))))
)
)

( ! [V__ROW3,V__ROW2,V__CLASS] :
   (((s__instance(V__ROW3,s__Class) &
         s__instance(V__ROW2,s__Class) &
         s__instance(V__CLASS,s__Class))
       =>
       ((s__disjointDecomposition__3(V__CLASS,V__ROW2,V__ROW3)
         =>
         (( ! [V__ITEM1, V__ITEM2] :
             (((s__instance(V__ITEM1,s__Class) &
                   s__instance(V__ITEM2,s__Class))
                 =>
                 (((s__inList(V__ITEM1,s__ListFn__2Fn(V__ROW2,V__ROW3))
                   &
                   s__inList(V__ITEM2,s__ListFn__2Fn(V__ROW2,V__ROW3))
               &
               ~((V__ITEM1 = V__ITEM2)))
             =>
             (s__disjoint(V__ITEM1,V__ITEM2)))))))))))
)
)

( ! [V__ROW5,V__ROW3,V__ROW4,V__ROW2,V__CLASS] :
   (((s__instance(V__ROW5,s__Class) &
         s__instance(V__ROW3,s__Class) &
         s__instance(V__ROW4,s__Class) &
         s__instance(V__ROW2,s__Class) &
         s__instance(V__CLASS,s__Class))
       =>
       ((s__disjointDecomposition__5(V__CLASS,V__ROW2,V__ROW3,V__ROW4,V__ROW5)
         =>
         (( ! [V__ITEM1, V__ITEM2] :
             (((s__instance(V__ITEM1,s__Class) &
                   s__instance(V__ITEM2,s__Class))
                 =>
                 (((s__inList(V__ITEM1,s__ListFn__4Fn(V__ROW2,V__ROW3,V__ROW4,V__ROW5))
                   &
                   s__inList(V__ITEM2,s__ListFn__4Fn(V__ROW2,V__ROW3,V__ROW4,V__ROW5))
               &
               ~((V__ITEM1 = V__ITEM2)))
             =>
             (s__disjoint(V__ITEM1,V__ITEM2)))))))))))
)
)

( ! [V__ROW3,V__ROW4,V__ROW2,V__CLASS] :
   (((s__instance(V__ROW3,s__Class) &
         s__instance(V__ROW4,s__Class) &
         s__instance(V__ROW2,s__Class) &
         s__instance(V__CLASS,s__Class))
       =>
       ((s__disjointDecomposition__4(V__CLASS,V__ROW2,V__ROW3,V__ROW4)
         =>
         (( ! [V__ITEM1, V__ITEM2] :
             (((s__instance(V__ITEM1,s__Class) &
                   s__instance(V__ITEM2,s__Class))
                 =>
                 (((s__inList(V__ITEM1,s__ListFn__3Fn(V__ROW2,V__ROW3,V__ROW4))
                   &
                   s__inList(V__ITEM2,s__ListFn__3Fn(V__ROW2,V__ROW3,V__ROW4))
               &
               ~((V__ITEM1 = V__ITEM2)))
             =>
             (s__disjoint(V__ITEM1,V__ITEM2)))))))))))
)
)

( ! [V__ROW7,V__ROW5,V__ROW6,V__ROW3,V__ROW4,V__ROW2,V__CLASS] :
   (((s__instance(V__ROW7,s__Class) &
         s__instance(V__ROW5,s__Class) &
         s__instance(V__ROW6,s__Class) &
         s__instance(V__ROW3,s__Class) &
         s__instance(V__ROW4,s__Class) &
         s__instance(V__ROW2,s__Class) &
         s__instance(V__CLASS,s__Class))
       =>
       ((s__disjointDecomposition__7(V__CLASS,V__ROW2,V__ROW3,V__ROW4,V__ROW5,V__ROW6,V__ROW7)
         =>
         (( ! [V__ITEM1, V__ITEM2] :
             (((s__instance(V__ITEM1,s__Class) &
                   s__instance(V__ITEM2,s__Class))
                 =>
                 (((s__inList(V__ITEM1,s__ListFn__6Fn(V__ROW2,V__ROW3,V__ROW4,V__ROW5,V__ROW6,V__ROW7))
                   &
                   s__inList(V__ITEM2,s__ListFn__6Fn(V__ROW2,V__ROW3,V__ROW4,V__ROW5,V__ROW6,V__ROW7))
               &
               ~((V__ITEM1 = V__ITEM2)))
             =>
             (s__disjoint(V__ITEM1,V__ITEM2)))))))))))
)
)

Merge.kif 2886-2895
( ! [V__ROW7,V__ROW8,V__ROW5,V__ROW6,V__ELEMENT,V__ROW3,V__ROW4,V__ROW2] :
   (((s__instance(V__ROW7,s__Class) &
         s__instance(V__ROW8,s__Class) &
         s__instance(V__ROW5,s__Class) &
         s__instance(V__ROW6,s__Class) &
         s__instance(V__ROW3,s__Class) &
         s__instance(V__ROW4,s__Class) &
         s__instance(V__ROW2,s__Class))
       =>
       ((s__disjointDecomposition__7(V__ROW2,V__ROW3,V__ROW4,V__ROW5,V__ROW6,V__ROW7,V__ROW8)
         =>
         ((s__inList(V__ELEMENT,s__ListFn__7Fn(V__ROW2,V__ROW3,V__ROW4,V__ROW5,V__ROW6,V__ROW7,V__ROW8))
         =>
         (s__instance(V__ELEMENT,s__Class)))))))
)
)

( ! [V__ELEMENT,V__ROW2] :
   ((s__instance(V__ROW2,s__Class) =>
       ((s__disjointDecomposition__1(V__ROW2)
         =>
         ((s__inList(V__ELEMENT,s__ListFn__1Fn(V__ROW2))
         =>
         (s__instance(V__ELEMENT,s__Class)))))))
)
)

( ! [V__ROW7,V__ROW5,V__ROW6,V__ELEMENT,V__ROW3,V__ROW4,V__ROW2] :
   (((s__instance(V__ROW7,s__Class) &
         s__instance(V__ROW5,s__Class) &
         s__instance(V__ROW6,s__Class) &
         s__instance(V__ROW3,s__Class) &
         s__instance(V__ROW4,s__Class) &
         s__instance(V__ROW2,s__Class))
       =>
       ((s__disjointDecomposition__6(V__ROW2,V__ROW3,V__ROW4,V__ROW5,V__ROW6,V__ROW7)
         =>
         ((s__inList(V__ELEMENT,s__ListFn__6Fn(V__ROW2,V__ROW3,V__ROW4,V__ROW5,V__ROW6,V__ROW7))
         =>
         (s__instance(V__ELEMENT,s__Class)))))))
)
)

( ! [V__ROW5,V__ROW6,V__ELEMENT,V__ROW3,V__ROW4,V__ROW2] :
   (((s__instance(V__ROW5,s__Class) &
         s__instance(V__ROW6,s__Class) &
         s__instance(V__ROW3,s__Class) &
         s__instance(V__ROW4,s__Class) &
         s__instance(V__ROW2,s__Class))
       =>
       ((s__disjointDecomposition__5(V__ROW2,V__ROW3,V__ROW4,V__ROW5,V__ROW6)
         =>
         ((s__inList(V__ELEMENT,s__ListFn__5Fn(V__ROW2,V__ROW3,V__ROW4,V__ROW5,V__ROW6))
         =>
         (s__instance(V__ELEMENT,s__Class)))))))
)
)

( ! [V__ELEMENT,V__ROW3,V__ROW2] :
   (((s__instance(V__ROW3,s__Class) &
         s__instance(V__ROW2,s__Class))
       =>
       ((s__disjointDecomposition__2(V__ROW2,V__ROW3)
         =>
         ((s__inList(V__ELEMENT,s__ListFn__2Fn(V__ROW2,V__ROW3))
         =>
         (s__instance(V__ELEMENT,s__Class)))))))
)
)

( ! [V__ELEMENT,V__ROW3,V__ROW4,V__ROW2] :
   (((s__instance(V__ROW3,s__Class) &
         s__instance(V__ROW4,s__Class) &
         s__instance(V__ROW2,s__Class))
       =>
       ((s__disjointDecomposition__3(V__ROW2,V__ROW3,V__ROW4)
         =>
         ((s__inList(V__ELEMENT,s__ListFn__3Fn(V__ROW2,V__ROW3,V__ROW4))
         =>
         (s__instance(V__ELEMENT,s__Class)))))))
)
)

( ! [V__ROW5,V__ELEMENT,V__ROW3,V__ROW4,V__ROW2] :
   (((s__instance(V__ROW5,s__Class) &
         s__instance(V__ROW3,s__Class) &
         s__instance(V__ROW4,s__Class) &
         s__instance(V__ROW2,s__Class))
       =>
       ((s__disjointDecomposition__4(V__ROW2,V__ROW3,V__ROW4,V__ROW5)
         =>
         ((s__inList(V__ELEMENT,s__ListFn__4Fn(V__ROW2,V__ROW3,V__ROW4,V__ROW5))
         =>
         (s__instance(V__ELEMENT,s__Class)))))))
)
)

Merge.kif 575-579

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


( ! [V__ROW3,V__ROW2] :
   (((s__instance(V__ROW3,s__Class) &
         s__instance(V__ROW2,s__Class))
       =>
       (((s__partition__2(V__ROW2,V__ROW3)
           =>
           (s__exhaustiveDecomposition__2(V__ROW2,V__ROW3)
           &
           s__disjointDecomposition__2(V__ROW2,V__ROW3)))
     &
     ((s__exhaustiveDecomposition__2(V__ROW2,V__ROW3)
       &
       s__disjointDecomposition__2(V__ROW2,V__ROW3))
   =>
   s__partition__2(V__ROW2,V__ROW3)))))
)
)

( ! [V__ROW3,V__ROW4,V__ROW2] :
   (((s__instance(V__ROW3,s__Class) &
         s__instance(V__ROW4,s__Class) &
         s__instance(V__ROW2,s__Class))
       =>
       (((s__partition__3(V__ROW2,V__ROW3,V__ROW4)
           =>
           (s__exhaustiveDecomposition__3(V__ROW2,V__ROW3,V__ROW4)
           &
           s__disjointDecomposition__3(V__ROW2,V__ROW3,V__ROW4)))
     &
     ((s__exhaustiveDecomposition__3(V__ROW2,V__ROW3,V__ROW4)
       &
       s__disjointDecomposition__3(V__ROW2,V__ROW3,V__ROW4))
   =>
   s__partition__3(V__ROW2,V__ROW3,V__ROW4)))))
)
)

( ! [V__ROW7,V__ROW8,V__ROW5,V__ROW6,V__ROW3,V__ROW4,V__ROW2] :
   (((s__instance(V__ROW7,s__Class) &
         s__instance(V__ROW8,s__Class) &
         s__instance(V__ROW5,s__Class) &
         s__instance(V__ROW6,s__Class) &
         s__instance(V__ROW3,s__Class) &
         s__instance(V__ROW4,s__Class) &
         s__instance(V__ROW2,s__Class))
       =>
       (((s__partition__7(V__ROW2,V__ROW3,V__ROW4,V__ROW5,V__ROW6,V__ROW7,V__ROW8)
           =>
           (s__exhaustiveDecomposition__7(V__ROW2,V__ROW3,V__ROW4,V__ROW5,V__ROW6,V__ROW7,V__ROW8)
           &
           s__disjointDecomposition__7(V__ROW2,V__ROW3,V__ROW4,V__ROW5,V__ROW6,V__ROW7,V__ROW8)))
     &
     ((s__exhaustiveDecomposition__7(V__ROW2,V__ROW3,V__ROW4,V__ROW5,V__ROW6,V__ROW7,V__ROW8)
       &
       s__disjointDecomposition__7(V__ROW2,V__ROW3,V__ROW4,V__ROW5,V__ROW6,V__ROW7,V__ROW8))
   =>
   s__partition__7(V__ROW2,V__ROW3,V__ROW4,V__ROW5,V__ROW6,V__ROW7,V__ROW8)))))
)
)

( ! [V__ROW5,V__ROW6,V__ROW3,V__ROW4,V__ROW2] :
   (((s__instance(V__ROW5,s__Class) &
         s__instance(V__ROW6,s__Class) &
         s__instance(V__ROW3,s__Class) &
         s__instance(V__ROW4,s__Class) &
         s__instance(V__ROW2,s__Class))
       =>
       (((s__partition__5(V__ROW2,V__ROW3,V__ROW4,V__ROW5,V__ROW6)
           =>
           (s__exhaustiveDecomposition__5(V__ROW2,V__ROW3,V__ROW4,V__ROW5,V__ROW6)
           &
           s__disjointDecomposition__5(V__ROW2,V__ROW3,V__ROW4,V__ROW5,V__ROW6)))
     &
     ((s__exhaustiveDecomposition__5(V__ROW2,V__ROW3,V__ROW4,V__ROW5,V__ROW6)
       &
       s__disjointDecomposition__5(V__ROW2,V__ROW3,V__ROW4,V__ROW5,V__ROW6))
   =>
   s__partition__5(V__ROW2,V__ROW3,V__ROW4,V__ROW5,V__ROW6)))))
)
)

( ! [V__ROW5,V__ROW3,V__ROW4,V__ROW2] :
   (((s__instance(V__ROW5,s__Class) &
         s__instance(V__ROW3,s__Class) &
         s__instance(V__ROW4,s__Class) &
         s__instance(V__ROW2,s__Class))
       =>
       (((s__partition__4(V__ROW2,V__ROW3,V__ROW4,V__ROW5)
           =>
           (s__exhaustiveDecomposition__4(V__ROW2,V__ROW3,V__ROW4,V__ROW5)
           &
           s__disjointDecomposition__4(V__ROW2,V__ROW3,V__ROW4,V__ROW5)))
     &
     ((s__exhaustiveDecomposition__4(V__ROW2,V__ROW3,V__ROW4,V__ROW5)
       &
       s__disjointDecomposition__4(V__ROW2,V__ROW3,V__ROW4,V__ROW5))
   =>
   s__partition__4(V__ROW2,V__ROW3,V__ROW4,V__ROW5)))))
)
)

( ! [V__ROW2] :
   ((s__instance(V__ROW2,s__Class) =>
       (((s__partition__1(V__ROW2)
           =>
           (s__exhaustiveDecomposition__1(V__ROW2)
           &
           s__disjointDecomposition__1(V__ROW2)))
     &
     ((s__exhaustiveDecomposition__1(V__ROW2)
       &
       s__disjointDecomposition__1(V__ROW2))
   =>
   s__partition__1(V__ROW2)))))
)
)

( ! [V__ROW7,V__ROW5,V__ROW6,V__ROW3,V__ROW4,V__ROW2] :
   (((s__instance(V__ROW7,s__Class) &
         s__instance(V__ROW5,s__Class) &
         s__instance(V__ROW6,s__Class) &
         s__instance(V__ROW3,s__Class) &
         s__instance(V__ROW4,s__Class) &
         s__instance(V__ROW2,s__Class))
       =>
       (((s__partition__6(V__ROW2,V__ROW3,V__ROW4,V__ROW5,V__ROW6,V__ROW7)
           =>
           (s__exhaustiveDecomposition__6(V__ROW2,V__ROW3,V__ROW4,V__ROW5,V__ROW6,V__ROW7)
           &
           s__disjointDecomposition__6(V__ROW2,V__ROW3,V__ROW4,V__ROW5,V__ROW6,V__ROW7)))
     &
     ((s__exhaustiveDecomposition__6(V__ROW2,V__ROW3,V__ROW4,V__ROW5,V__ROW6,V__ROW7)
       &
       s__disjointDecomposition__6(V__ROW2,V__ROW3,V__ROW4,V__ROW5,V__ROW6,V__ROW7))
   =>
   s__partition__6(V__ROW2,V__ROW3,V__ROW4,V__ROW5,V__ROW6,V__ROW7)))))
)
)

Merge.kif 591-595 @ROW is exhaustively partitioned into @ROW if and only if @ROW is covered by @ROW and @ROW is disjointly decomposed into @ROW

appearance as argument number 0
-------------------------


s__disjointDecomposition__6(s__Abstract,s__Quantity,s__Attribute,s__Relation,s__Proposition,s__List)

Merge.kif 1613-1613 Abstract is disjointly decomposed into quantity, attribute, relation, proposition, and list
s__disjointDecomposition__5(s__Arthropod,s__Arachnid,s__Myriapod,s__Insect,s__Crustacean)

Merge.kif 13873-13873 Arthropod is disjointly decomposed into arachnid, myriapod, insect, and crustacean
s__disjointDecomposition__4(s__ColdBloodedVertebrate,s__Amphibian,s__Fish,s__Reptile)

Merge.kif 13895-13895 Cold blooded vertebrate is disjointly decomposed into amphibian, fish, and reptile
s__disjointDecomposition__4(s__CommissionedOfficerRank,s__FlagOfficerRank,s__FieldGradeOfficerRank,s__CompanyGradeRank)

Military.kif 283-284 Commissioned officer rank is disjointly decomposed into flag officer rank, field grade officer rank, and company grade rank
s__disjointDecomposition__4(s__ComputerStatus,s__HostReady,s__HostDown,s__Booting)

ComputingBrands.kif 3191-3191 Computer status is disjointly decomposed into host ready, host down, and booting up
s__disjointDecomposition__3(s__DifferentialEquation,s__FirstOrderDifferentialEquation,s__HigherOrderDifferentialEquation)

engineering.kif 179-179 Differential equation is disjointly decomposed into first order differential equation and higher order differential equation
s__disjointDecomposition__3(s__DifferentialEquation,s__OrdinaryDifferentialEquation,s__PartialDifferentialEquation)

engineering.kif 189-189 Differential equation is disjointly decomposed into ordinary differential equation and partial differential equation
s__disjointDecomposition__3(s__EnlistedSoldierRank,s__PrivateRank,s__NonCommissionedOfficerRank)

Military.kif 269-269 Enlisted soldier rank is disjointly decomposed into private rank and non commissioned officer rank
s__disjointDecomposition__3(s__Expressing,s__ExpressingApproval,s__ExpressingDisapproval)

Mid-level-ontology.kif 12141-12141 Expressing is disjointly decomposed into expressing approval and expressing disapproval
s__disjointDecomposition__3(s__GameArtifact,s__GameBoard,s__GamePiece)

Mid-level-ontology.kif 16077-16077 Game artifact is disjointly decomposed into game board and game piece
s__disjointDecomposition__4(s__Invertebrate,s__Worm,s__Mollusk,s__Arthropod)

Merge.kif 13852-13852 Invertebrate is disjointly decomposed into worm, mollusk, and arthropod
s__disjointDecomposition__4(s__LAN,s__BusNetwork,s__StarNetwork,s__RingNetwork)

QoSontology.kif 37-37 LAN is disjointly decomposed into bus network, star network, and ring network
s__disjointDecomposition__4(s__Language,s__AnimalLanguage,s__HumanLanguage,s__ComputerLanguage)

Merge.kif 1321-1321 Language is disjointly decomposed into animal language, human language, and computer language
s__disjointDecomposition__6(s__Mammal,s__AquaticMammal,s__HoofedMammal,s__Marsupial,s__Rodent,s__Primate)

Merge.kif 13929-13929 Mammal is disjointly decomposed into aquatic mammal, hoofed mammal, marsupial, rodent, and primate
s__disjointDecomposition__3(s__NonCommissionedOfficerRank,s__JuniorNCORank,s__SeniorNCORank)

Military.kif 306-306 Non commissioned officer rank is disjointly decomposed into juniorNCO rank and seniorNCO rank
s__disjointDecomposition__4(s__NonFloweringPlant,s__Alga,s__Fern,s__Moss)

Merge.kif 13758-13758 Non flowering plant is disjointly decomposed into alga, fern, and moss
s__disjointDecomposition__4(s__Nutrient,s__Protein,s__Carbohydrate,s__Vitamin)

Merge.kif 14030-14030 Nutrient is disjointly decomposed into protein, carbohydrate, and vitamin
s__disjointDecomposition__4(s__Phrase,s__VerbPhrase,s__NounPhrase,s__PrepositionalPhrase)

Merge.kif 14633-14633 Phrase is disjointly decomposed into verb phrase, noun phrase, and PrepositionalPhrase
s__disjointDecomposition__5(s__PowerGeneration,s__FossilFuelPowerGeneration,s__HydroElectricPowerGeneration,s__NuclearPowerGeneration,s__OtherSourcePowerGeneration)

Economy.kif 2091-2091 Power generation is disjointly decomposed into fossil fuel power generation, hydro electric power generation, nuclear power generation, and other source power generation
s__disjointDecomposition__4(s__Primate,s__Ape,s__Monkey,s__Hominid)

Merge.kif 13975-13975 Primate is disjointly decomposed into ape, monkey, and hominid
s__disjointDecomposition__6(s__Relation,s__BinaryRelation,s__TernaryRelation,s__QuaternaryRelation,s__QuintaryRelation,s__VariableArityRelation)

Merge.kif 2107-2108 Relation is disjointly decomposed into binary relation, ternary relation, quaternary relation, quintary relation, and variable arity relation
s__disjointDecomposition__3(s__Residence,s__PermanentResidence,s__TemporaryResidence)

Merge.kif 15108-15108 Residence is disjointly decomposed into permanent residence and temporary residence
s__disjointDecomposition__6(s__Sentence,s__Statement,s__Supposition,s__Question,s__Request,s__Order)

Mid-level-ontology.kif 13422-13422 Sentence is disjointly decomposed into statement, supposition, question, request, and order
s__disjointDecomposition__5(s__Tissue,s__ConnectiveTissue,s__MuscleTissue,s__NervousTissue,s__EpithelialTissue)

Merge.kif 14469-14469 Tissue is disjointly decomposed into connective tissue, MuscleTissue, nervous tissue, and epithelial tissue


Show full definition with tree view
Show simplified definition (without tree view)
Show simplified definition (with tree view)



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