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

Formal Language: 



KB Term:  Term intersection
English Word: 

  part

Sigma KEE - part
part

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


s__documentation(s__part__m,s__ChineseLanguage,'"这是基本的逻辑分体关系。其他所有的逻辑分体关系都是根据它来下 定义的。 (part ?PART ?WHOLE) 的意思就是 Object ?PART 是 Object ?WHOLE 的一部分。 要注意 因为 part 是一个 ReflexiveRelation, 所以每个 Object 都是它自己本身的一部分。"')

chinese_format.kif 1570-1572
s__documentation(s__part__m,s__EnglishLanguage,'"The basic mereological relation. All other mereological relations are defined in terms of this one. (part ?PART ?WHOLE) simply means that the Object ?PART is part of the Object ?WHOLE. Note that, since part is a ReflexiveRelation, every Object is a part of itself."')

Merge.kif 878-882
s__domain(s__part__m,n__1,s__Object)

Merge.kif 875-875 The number 1 argument of part is an instance of object
s__domain(s__part__m,n__2,s__Object)

Merge.kif 876-876 The number 2 argument of part is an instance of object
s__instance(s__BinaryPredicate,s__SetOrClass)

s__instance(s__part__m,s__BinaryPredicate)

Merge.kif 874-874 part is an instance of binary predicate
s__instance(s__part__m,s__PartialOrderingRelation)

s__instance(s__PartialOrderingRelation,s__SetOrClass)

Merge.kif 873-873 part is an instance of partial ordering relation
s__instance(s__SpatialRelation,s__SetOrClass)

s__instance(s__part__m,s__SpatialRelation)

Merge.kif 872-872 part is an instance of spatial relation

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


s__disjointRelation(s__contains__m,s__part__m)

Merge.kif 946-946 contains and part are disjoint
s__format(s__ChineseLanguage,s__part__m,'"%1 %n 是 %2 的 part"')

chinese_format.kif 161-161
s__format(s__EnglishLanguage,s__part__m,'"%1 is %n a part of %2"')

english_format.kif 165-165
s__relatedInternalConcept(s__havePartTypes__m,s__part__m)

Mid-level-ontology.kif 22841-22841 havePartTypes is internally related to part
s__relatedInternalConcept(s__initialPart__m,s__part__m)

Mid-level-ontology.kif 22788-22788 initial part is internally related to part
s__relatedInternalConcept(s__initiallyContainsPart__m,s__part__m)

Mid-level-ontology.kif 22815-22815 initially contains part is internally related to part
s__relatedInternalConcept(s__partTypes__m,s__part__m)

Mid-level-ontology.kif 22858-22858 partTypes is internally related to part
s__relatedInternalConcept(s__typicalPart__m,s__part__m)

Mid-level-ontology.kif 22714-22714 typical part is internally related to part
s__relatedInternalConcept(s__typicallyContainsPart__m,s__part__m)

Mid-level-ontology.kif 22751-22751 typically contains part is internally related to part
s__subrelation(s__component__m,s__part__m)

Merge.kif 916-916 component is a subrelation of part
s__subrelation(s__geneticSubstrateOfVirus__m,s__part__m)

VirusProteinAndCellPart.kif 34-34 genetic substrate of virus is a subrelation of part
s__subrelation(s__half__m,s__part__m)

Mid-level-ontology.kif 12369-12369 half is a subrelation of part
s__subrelation(s__inString__m,s__part__m)

Mid-level-ontology.kif 23396-23396 inString is a subrelation of part
s__subrelation(s__interiorPart__m,s__part__m)

Merge.kif 9296-9296 interior part is a subrelation of part
s__subrelation(s__most__m,s__part__m)

Mid-level-ontology.kif 12412-12412 most is a subrelation of part
s__subrelation(s__pathInSystem__m,s__part__m)

Transportation.kif 2732-2732 path in system is a subrelation of part
s__subrelation(s__physicalEnd__m,s__part__m)

Merge.kif 17222-17222 physical end is a subrelation of part
s__subrelation(s__piece__m,s__part__m)

Merge.kif 900-900 piece is a subrelation of part
s__subrelation(s__properPart__m,s__part__m)

Merge.kif 886-886 proper part is a subrelation of part
s__subrelation(s__quarter__m,s__part__m)

Mid-level-ontology.kif 12403-12403 quarter is a subrelation of part
s__subrelation(s__subCollection__m,s__part__m)

Merge.kif 1223-1223 sub collection is a subrelation of part
s__subrelation(s__subString__m,s__part__m)

Mid-level-ontology.kif 23418-23418 subString is a subrelation of part
s__subrelation(s__third__m,s__part__m)

Mid-level-ontology.kif 12385-12385 third is a subrelation of part
s__termFormat(s__ChineseLanguage,s__part__m,'"部分"')

chinese_format.kif 162-162

Display limited to 25 items. Show next 25

Display limited to 25 items. Show next 25

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


( ! [V__P,V__S,V__PM] :
   (((s__instance(V__P,s__SelfConnectedObject) &
         s__instance(V__S,s__RealNumber))
       =>
       ((((s__instance(V__PM,s__ParticulateMatter) &
               s__part(V__P,V__PM)
             &
             s__approximateDiameter(V__P,s__MeasureFn(V__S,s__Micrometer))
           &
           s__greaterThan(n__10,V__S)
         &
         s__greaterThan(V__S,n__2_5))
     =>
     ( ? [V__PM10] :
       ((s__instance(V__PM10,s__CoarseParticulateMatter) &
           s__part(V__PM10,V__PM)))))
&
(( ? [V__PM10] :
     ((s__instance(V__PM10,s__CoarseParticulateMatter) &
         s__part(V__PM10,V__PM))))
=>
(s__instance(V__PM,s__ParticulateMatter) &
   s__part(V__P,V__PM)
&
s__approximateDiameter(V__P,s__MeasureFn(V__S,s__Micrometer))
&
s__greaterThan(n__10,V__S)
&
s__greaterThan(V__S,n__2_5))))))
)
)

Geography.kif 6998-7009 An object is an instance of PM and a self connected object is a part of the object and the approximate diameter of the self connected object is a real number micrometer(s) and 10 is greater than the real number and the real number is greater than 2.5 if and only if there exists the object10 such that the object10 is an instance of PM10 and the object10 is a part of the object
( ! [V__P,V__S,V__PM] :
   (((s__instance(V__P,s__SelfConnectedObject) &
         s__instance(V__S,s__RealNumber))
       =>
       ((((s__instance(V__PM,s__ParticulateMatter) &
               s__part(V__P,V__PM)
             &
             s__approximateDiameter(V__P,s__MeasureFn(V__S,s__Micrometer))
           &
           s__greaterThanOrEqualTo(V__S,n__2_5))
       =>
       ( ? [V__PM25] :
         ((s__instance(V__PM25,s__FineParticulateMatter) &
             s__part(V__PM25,V__PM)))))
   &
   (( ? [V__PM25] :
       ((s__instance(V__PM25,s__FineParticulateMatter) &
           s__part(V__PM25,V__PM))))
   =>
   (s__instance(V__PM,s__ParticulateMatter) &
     s__part(V__P,V__PM)
   &
   s__approximateDiameter(V__P,s__MeasureFn(V__S,s__Micrometer))
&
s__greaterThanOrEqualTo(V__S,n__2_5))))))
)
)

Geography.kif 7027-7037 An object is an instance of PM and a self connected object is a part of the object and the approximate diameter of the self connected object is a real number micrometer(s) and the real number is greater than or equal to 2.5 if and only if there exists the object25 such that the object25 is an instance of PM2.5 and the object25 is a part of the object
( ! [V__N2,V__S,V__SI,V__U,V__CO,V__N] :
   (((s__instance(V__N2,s__RealNumber) &
         s__subclass(V__S,s__Substance) &
         s__instance(V__S,s__Class) &
         s__instance(V__SI,s__Object) &
         s__instance(V__U,s__UnitOfMeasure) &
         s__instance(V__CO,s__CorpuscularObject) &
         s__instance(V__N,s__RealNumber))
       =>
       (((s__amount(V__S,V__CO,s__MeasureFn(V__N,V__U))
         &
         s__instance(V__SI,V__S)
       &
       s__measure(V__SI,s__MeasureFn(V__N2,V__U))
   &
   s__part(V__SI,V__CO))
=>
(( ? [V__L] :
   ((s__instance(V__L,s__List) &
       (s__inList(s__MeasureFn(V__N2,V__U)
      ,V__L)
     &
     (V__L = s__AmountsFn(V__S,V__CO))
   &
   (s__MeasureFn(V__N,V__U)
   = s__ListSumFn(V__L))))))))))
)
)

Merge.kif 7373-7389
( ! [V__BC,V__AC,V__A,V__B,V__F,V__H,V__PART] :
   (((s__subclass(V__A,s__Muscle) &
         s__instance(V__A,s__Object) &
         s__instance(V__A,s__Class) &
         s__subclass(V__B,s__Muscle) &
         s__instance(V__B,s__Class) &
         s__instance(V__B,s__Object) &
         s__subclass(V__B,s__Process) &
         s__instance(V__PART,s__Object))
       =>
       (((s__antagonistMuscles(V__A,V__B)
           &
           s__instance(V__F,s__Extension) &
           s__instrument(V__F,V__A)
         &
         s__moves(V__F,V__PART)
       &
       s__instance(V__AC,V__A)
     &
     s__instance(V__BC,V__B)
   &
   s__part(V__A,V__H)
&
s__part(V__B,V__H)
&
s__instance(V__H,s__Mammal))
=>
(s__capability(V__B,s__instrument__m,s__Flexion)))))
)
)

Mid-level-ontology.kif 9953-9964
( ! [V__BC,V__AC,V__A,V__B,V__F,V__H,V__PART] :
   (((s__subclass(V__A,s__Muscle) &
         s__instance(V__A,s__Object) &
         s__instance(V__A,s__Class) &
         s__subclass(V__B,s__Muscle) &
         s__instance(V__B,s__Class) &
         s__instance(V__B,s__Object) &
         s__subclass(V__B,s__Process) &
         s__instance(V__PART,s__Object))
       =>
       (((s__antagonistMuscles(V__A,V__B)
           &
           s__instance(V__F,s__Flexion) &
           s__instrument(V__F,V__A)
         &
         s__moves(V__F,V__PART)
       &
       s__instance(V__AC,V__A)
     &
     s__instance(V__BC,V__B)
   &
   s__part(V__A,V__H)
&
s__part(V__B,V__H)
&
s__instance(V__H,s__Mammal))
=>
(s__capability(V__B,s__instrument__m,s__Extension)))))
)
)

Mid-level-ontology.kif 9940-9951
( ! [V__AREA,V__ZONE,V__SLOPE] :
   (((s__instance(V__AREA,s__Object) &
         s__instance(V__ZONE,s__LandArea) &
         s__instance(V__SLOPE,s__NonnegativeRealNumber))
       =>
       (((s__attribute(V__AREA,s__FlatTerrain) &
             s__part(V__ZONE,V__AREA)
           &
           s__slopeGradient(V__ZONE,V__SLOPE))
       =>
       (s__greaterThan(n__0_005,V__SLOPE)))))
)
)

Geography.kif 1725-1730
( ! [V__AREA,V__ZONE,V__SLOPE] :
   (((s__instance(V__AREA,s__Object) &
         s__instance(V__ZONE,s__LandArea) &
         s__instance(V__SLOPE,s__NonnegativeRealNumber))
       =>
       (((s__attribute(V__AREA,s__LowTerrain) &
             s__part(V__ZONE,V__AREA)
           &
           s__slopeGradient(V__ZONE,V__SLOPE))
       =>
       (s__greaterThan(n__0_03,V__SLOPE)))))
)
)

Geography.kif 1737-1742
( ! [V__O,V__P1,V__P2,V__S,V__PL,V__L] :
   (((s__instance(V__O,s__SelfConnectedObject) &
         s__instance(V__P1,s__Object) &
         s__instance(V__P2,s__Object) &
         s__instance(V__S,s__SelfConnectedObject) &
         s__instance(V__PL,s__Object) &
         s__instance(V__L,s__Object))
       =>
       (((s__attribute(V__O,s__Concave) &
             s__surface(V__O,V__S)
           &
           s__part(V__P1,V__S)
         &
         s__part(V__P2,V__S)
       &
       (V__L = s__LineFn(V__P1,V__P2))
     &
     ~((V__P1 = V__P2))
     &
     s__part(V__PL,V__L))
=>
(s__orientation(V__PL,V__O,s__Outside)))))
)
)

ComputingBrands.kif 2652-2663
( ! [V__O,V__P1,V__P2,V__S,V__PL,V__L] :
   (((s__instance(V__O,s__SelfConnectedObject) &
         s__instance(V__P1,s__Object) &
         s__instance(V__P2,s__Object) &
         s__instance(V__S,s__SelfConnectedObject) &
         s__instance(V__PL,s__Object) &
         s__instance(V__L,s__Object))
       =>
       (((s__attribute(V__O,s__Convex) &
             s__surface(V__O,V__S)
           &
           s__part(V__P1,V__S)
         &
         s__part(V__P2,V__S)
       &
       (V__L = s__LineFn(V__P1,V__P2))
     &
     ~((V__P1 = V__P2))
     &
     s__part(V__PL,V__L))
=>
(s__orientation(V__PL,V__O,s__Inside)))))
)
)

ComputingBrands.kif 2624-2635
( ! [V__WORD,V__SYLLABLE] :
   ((s__instance(V__SYLLABLE,s__Object) =>
       (((s__attribute(V__SYLLABLE,s__Stressed) &
             s__instance(V__WORD,s__Word) &
             s__part(V__SYLLABLE,V__WORD))
         =>
         (~(( ? [V__SYLLABLE2] :
               ((s__instance(V__SYLLABLE2,s__Syllable) &
                   s__part(V__SYLLABLE2,V__WORD)
                 &
                 s__attribute(V__SYLLABLE2,s__Stressed) &
                 ~((V__SYLLABLE2 = V__SYLLABLE))))))))))
)
)

Mid-level-ontology.kif 18475-18485
( ! [V__OBJECT,V__BOTTOM,V__PART] :
   (((s__instance(V__OBJECT,s__SelfConnectedObject) &
         s__instance(V__BOTTOM,s__SelfConnectedObject) &
         s__instance(V__PART,s__Object))
       =>
       (((s__bottom(V__BOTTOM,V__OBJECT)
           &
           s__part(V__PART,V__OBJECT)
         &
         ~(s__connected(V__PART,V__BOTTOM)))
     =>
     (s__orientation(V__PART,V__BOTTOM,s__Above)))))
)
)

Merge.kif 9319-9324
( ! [V__X,V__Y,V__Z] :
   (((s__instance(V__X,s__Object) &
         s__instance(V__Y,s__Object) &
         s__instance(V__Z,s__Object))
       =>
       (((s__connected(V__X,V__Y)
           &
           s__part(V__Y,V__Z))
       =>
       (s__connected(V__X,V__Z)))))
)
)

Geography.kif 514-518
( ! [V__CY,V__CI,V__M] :
   ((s__instance(V__M,s__LengthMeasure) =>
       (((s__cylinderBore(V__CY,V__M)
           &
           s__instance(V__CY,s__Cylinder) &
           s__instance(V__CI,s__Circle) &
           s__part(V__CI,V__CY))
       =>
       (s__diameter(V__CI,V__M)))))
)
)

Cars.kif 1538-1544
No TPTP formula. May not be expressible in strict first order. Cars.kif 2585-2603
( ! [V__P1,V__P2,V__L2,V__OP1,V__L,V__OP2] :
   (((s__instance(V__P1,s__Object) &
         s__instance(V__P2,s__Object) &
         s__instance(V__L2,s__Object) &
         s__instance(V__OP1,s__Object) &
         s__instance(V__L,s__Object) &
         s__instance(V__OP2,s__Object))
       =>
       ((((V__L = s__LineFn(V__P1,V__P2))
           &
           s__part(V__OP1,V__L)
         &
         s__part(V__OP2,V__L)
       &
       ~((V__OP1 = V__OP2))
       &
       (V__L2 = s__LineFn(V__OP1,V__OP2)))
   =>
   (s__part(V__L2,V__L)))))
)
)

ComputingBrands.kif 2595-2603
No TPTP formula. May not be expressible in strict first order. Merge.kif 17522-17530
No TPTP formula. May not be expressible in strict first order. Merge.kif 17502-17512
No TPTP formula. May not be expressible in strict first order. Cars.kif 2567-2583
No TPTP formula. May not be expressible in strict first order. Merge.kif 4145-4151
( ! [V__OBJ1,V__HOLE,V__OBJ2] :
   (((s__instance(V__OBJ1,s__SelfConnectedObject) &
         s__instance(V__HOLE,s__Hole) &
         s__instance(V__OBJ2,s__SelfConnectedObject))
       =>
       (((s__hole(V__HOLE,V__OBJ1)
           &
           s__part(V__OBJ1,V__OBJ2))
       =>
       ((s__overlapsSpatially(V__HOLE,V__OBJ2)
         |
         s__hole(V__HOLE,V__OBJ2))))))
)
)

Merge.kif 9504-9510
( ! [V__A,V__S] :
   (((s__instance(V__A,s__Animal) &
         s__instance(V__S,s__AnimalShell) &
         s__part(V__S,V__A))
     =>
     ((s__instance(V__A,s__Invertebrate) |
         s__instance(V__A,s__Reptile))))
   )
)

Mid-level-ontology.kif 10747-10754
No TPTP formula. May not be expressible in strict first order. Mid-level-ontology.kif 9211-9233
No TPTP formula. May not be expressible in strict first order. MilitaryDevices.kif 1619-1630
No TPTP formula. May not be expressible in strict first order. MilitaryDevices.kif 1632-1644
( ! [V__A2,V__S1,V__R1,V__R2,V__A1] :
   (((s__instance(V__R1,s__RealNumber) &
         s__instance(V__R2,s__RealNumber))
       =>
       (((s__instance(V__A1,s__Automobile) &
             s__instance(V__A2,s__Automobile) &
             s__instance(V__S1,s__AutomobileShock) &
             s__part(V__S1,V__A1)
           &
           ~(( ? [V__S2] :
               ((s__instance(V__S2,s__AutomobileShock) &
                   s__part(V__S2,V__A2)))))
         &
         s__dampingRatio(V__A1,V__R1)
       &
       s__dampingRatio(V__A2,V__R2))
   =>
   (s__greaterThan(V__R2,V__R1)))))
)
)

Cars.kif 853-866

Display limited to 25 items. Show next 25

Display limited to 25 items. Show next 25

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


No TPTP formula. May not be expressible in strict first order. Merge.kif 11877-11884 A process is an instance of combining and an object is a resource for the process and an entity is a result of the process if and only if the object is not a part of the entity holds during the beginning of the time of existence of the process and the object is a part of the entity holds during the end of the time of existence of the process
( ! [V__P,V__S,V__PM] :
   (((s__instance(V__P,s__SelfConnectedObject) &
         s__instance(V__S,s__RealNumber))
       =>
       ((((s__instance(V__PM,s__ParticulateMatter) &
               s__part(V__P,V__PM)
             &
             s__approximateDiameter(V__P,s__MeasureFn(V__S,s__Micrometer))
           &
           s__greaterThan(n__10,V__S)
         &
         s__greaterThan(V__S,n__2_5))
     =>
     ( ? [V__PM10] :
       ((s__instance(V__PM10,s__CoarseParticulateMatter) &
           s__part(V__PM10,V__PM)))))
&
(( ? [V__PM10] :
     ((s__instance(V__PM10,s__CoarseParticulateMatter) &
         s__part(V__PM10,V__PM))))
=>
(s__instance(V__PM,s__ParticulateMatter) &
   s__part(V__P,V__PM)
&
s__approximateDiameter(V__P,s__MeasureFn(V__S,s__Micrometer))
&
s__greaterThan(n__10,V__S)
&
s__greaterThan(V__S,n__2_5))))))
)
)

Geography.kif 6998-7009 An object is an instance of PM and a self connected object is a part of the object and the approximate diameter of the self connected object is a real number micrometer(s) and 10 is greater than the real number and the real number is greater than 2.5 if and only if there exists the object10 such that the object10 is an instance of PM10 and the object10 is a part of the object
( ! [V__P,V__S,V__PM] :
   (((s__instance(V__P,s__SelfConnectedObject) &
         s__instance(V__S,s__RealNumber))
       =>
       ((((s__instance(V__PM,s__ParticulateMatter) &
               s__part(V__P,V__PM)
             &
             s__approximateDiameter(V__P,s__MeasureFn(V__S,s__Micrometer))
           &
           s__greaterThanOrEqualTo(V__S,n__2_5))
       =>
       ( ? [V__PM25] :
         ((s__instance(V__PM25,s__FineParticulateMatter) &
             s__part(V__PM25,V__PM)))))
   &
   (( ? [V__PM25] :
       ((s__instance(V__PM25,s__FineParticulateMatter) &
           s__part(V__PM25,V__PM))))
   =>
   (s__instance(V__PM,s__ParticulateMatter) &
     s__part(V__P,V__PM)
   &
   s__approximateDiameter(V__P,s__MeasureFn(V__S,s__Micrometer))
&
s__greaterThanOrEqualTo(V__S,n__2_5))))))
)
)

Geography.kif 7027-7037 An object is an instance of PM and a self connected object is a part of the object and the approximate diameter of the self connected object is a real number micrometer(s) and the real number is greater than or equal to 2.5 if and only if there exists the object25 such that the object25 is an instance of PM2.5 and the object25 is a part of the object
( ! [V__HOLE1] :
   ((s__instance(V__HOLE1,s__Object) =>
       (((s__attribute(V__HOLE1,s__Fillable) =>
             ( ? [V__HOLE2] :
               ((s__instance(V__HOLE2,s__Hole) &
                   s__part(V__HOLE1,V__HOLE2)))))
         &
         (( ? [V__HOLE2] :
             ((s__instance(V__HOLE2,s__Hole) &
                 s__part(V__HOLE1,V__HOLE2))))
         =>
         s__attribute(V__HOLE1,s__Fillable)))))
)
)

Merge.kif 9563-9568 Fillable is an attribute of an object if and only if there exists another object such that the other object is an instance of hole and the object is a part of the other object
( ! [V__BONE] :
   (((s__instance(V__BONE,s__Bone) =>
         ( ? [V__SKELETON] :
           (((s__instance(V__SKELETON,s__Skeleton) |
                 s__instance(V__SKELETON,s__Exoskeleton))
               &
               s__part(V__BONE,V__SKELETON)))))
     &
     (( ? [V__SKELETON] :
         (((s__instance(V__SKELETON,s__Skeleton) |
               s__instance(V__SKELETON,s__Exoskeleton))
             &
             s__part(V__BONE,V__SKELETON))))
     =>
     s__instance(V__BONE,s__Bone)))
)
)

Mid-level-ontology.kif 10898-10905 An object is an instance of bone if and only if there exists another object such that the other object is an instance of skeleton or the other object is an instance of exoskeleton and the object is a part of the other object
( ! [V__OBJ1,V__OBJ2] :
   (((s__instance(V__OBJ1,s__Object) &
         s__instance(V__OBJ2,s__Object))
       =>
       (((s__overlapsPartially(V__OBJ1,V__OBJ2)
           =>
           (~(s__part(V__OBJ1,V__OBJ2))
           &
           ~(s__part(V__OBJ2,V__OBJ1))
         &
         ( ? [V__OBJ3] :
           ((s__instance(V__OBJ3,s__Object) &
               (s__part(V__OBJ3,V__OBJ1)
               &
               s__part(V__OBJ3,V__OBJ2)))))))
&
((~(s__part(V__OBJ1,V__OBJ2))
   &
   ~(s__part(V__OBJ2,V__OBJ1))
&
( ? [V__OBJ3] :
   ((s__instance(V__OBJ3,s__Object) &
       (s__part(V__OBJ3,V__OBJ1)
       &
       s__part(V__OBJ3,V__OBJ2))))))
=>
s__overlapsPartially(V__OBJ1,V__OBJ2)))))
)
)

Merge.kif 9237-9245 An object partially overlaps with another object if and only if the object is not a part of the other object and the other object is not a part of the object and there exists a third object such that the third object is a part of the object and the third object is a part of the other object
( ! [V__OBJ1,V__OBJ2] :
   (((s__instance(V__OBJ1,s__Object) &
         s__instance(V__OBJ2,s__Object))
       =>
       (((s__overlapsSpatially(V__OBJ1,V__OBJ2)
           =>
           ( ? [V__OBJ3] :
             ((s__instance(V__OBJ3,s__Object) &
                 (s__part(V__OBJ3,V__OBJ1)
                 &
                 s__part(V__OBJ3,V__OBJ2))))))
     &
     (( ? [V__OBJ3] :
         ((s__instance(V__OBJ3,s__Object) &
             (s__part(V__OBJ3,V__OBJ1)
             &
             s__part(V__OBJ3,V__OBJ2)))))
   =>
   s__overlapsSpatially(V__OBJ1,V__OBJ2)))))
)
)

Merge.kif 9199-9204 An object and another object is overlapsSpatially if and only if there exists a third object such that the third object is a part of the object and the third object is a part of the other object
( ! [V__OBJ1,V__OBJ2] :
   (((s__instance(V__OBJ1,s__Object) &
         s__instance(V__OBJ2,s__Object))
       =>
       (((s__properPart(V__OBJ1,V__OBJ2)
           =>
           (s__part(V__OBJ1,V__OBJ2)
           &
           ~(s__part(V__OBJ2,V__OBJ1))))
     &
     ((s__part(V__OBJ1,V__OBJ2)
       &
       ~(s__part(V__OBJ2,V__OBJ1)))
   =>
   s__properPart(V__OBJ1,V__OBJ2)))))
)
)

Merge.kif 893-898 An object is a proper part of another object if and only if the object is a part of the other object and the other object is not a part of the object
No TPTP formula. May not be expressible in strict first order. Transportation.kif 1277-1287 A geographic area is total facility type in area the class corresponding to airport with paved runway for a nonnegative integer if and only if the nonnegative integer is a cardinality of the class described by a symbolic string
( ! [V__ACCT,V__SITE] :
   (((s__instance(V__ACCT,s__UserAccount) &
         s__instance(V__SITE,s__Agent) &
         s__instance(V__SITE,s__WebSite))
       =>
       ((s__accountAtSite(V__ACCT,V__SITE)
         =>
         (( ? [V__DATABASE, V__SITE_OWNER] :
             ((s__instance(V__DATABASE,s__Database) &
                 s__instance(V__SITE_OWNER,s__Agent) &
                 s__possesses(V__SITE,V__SITE_OWNER)
               &
               s__possesses(V__DATABASE,V__SITE_OWNER)
             &
             s__part(V__ACCT,V__DATABASE))))))))
)
)

UXExperimentalTerms.kif 784-792
No TPTP formula. May not be expressible in strict first order. Music.kif 313-319
( ! [V__M] :
   (((s__attribute(V__M,s__MashupRecording) &
         s__instance(V__M,s__Recording))
       =>
       (( ? [V__M1, V__M2, V__S1, V__S2] :
           ((s__instance(V__M1,s__MusicRecording) &
               s__instance(V__M2,s__MusicRecording) &
               s__instance(V__S1,s__Music) &
               s__instance(V__S2,s__Music) &
               (s__musicInterpretation(V__M1,V__S1)
               &
               s__musicInterpretation(V__M2,V__S2)
             &
             ~((V__S1 = V__S2))
             &
             s__part(V__M1,V__M)
           &
           s__part(V__M2,V__M)))))))
)
)

Music.kif 423-433
( ! [V__WORD,V__SYLLABLE] :
   ((s__instance(V__SYLLABLE,s__Object) =>
       (((s__attribute(V__SYLLABLE,s__Stressed) &
             s__instance(V__WORD,s__Word) &
             s__part(V__SYLLABLE,V__WORD))
         =>
         (~(( ? [V__SYLLABLE2] :
               ((s__instance(V__SYLLABLE2,s__Syllable) &
                   s__part(V__SYLLABLE2,V__WORD)
                 &
                 s__attribute(V__SYLLABLE2,s__Stressed) &
                 ~((V__SYLLABLE2 = V__SYLLABLE))))))))))
)
)

Mid-level-ontology.kif 18475-18485
( ! [V__X,V__Y] :
   ((s__instance(V__X,s__Object) =>
       (((s__attribute(V__X,V__Y)
           &
           s__instance(V__Y,s__HotelLevelAttribute))
         =>
         ((s__instance(V__X,s__BuildingLevel) &
             ( ? [V__BLDG] :
               ((s__instance(V__BLDG,s__HotelBuilding) &
                   s__part(V__X,V__BLDG)))))))))
)
)

Hotel.kif 1185-1194
( ! [V__X] :
   ((s__instance(V__X,s__Agent) =>
       (((s__attribute(V__X,s__TravelerAccommodation) &
             s__capability(s__RoomCleaningService,s__agent__m,V__X))
         =>
         (( ? [V__MAID, V__HOTELROOM] :
             ((s__instance(V__MAID,s__CognitiveAgent) &
                 (s__employs(V__X,V__MAID)
                 &
                 s__attribute(V__MAID,s__Maid) &
                 s__instance(V__HOTELROOM,s__HotelUnit) &
                 s__part(V__HOTELROOM,s__PropertyFn(V__X))
             &
             s__capability(s__RoomCleaningService,s__patient__m,V__HOTELROOM)
           &
           s__capability(s__RoomCleaningService,s__serviceProvider__m,V__MAID)))))))))
)
)

Hotel.kif 1910-1921
( ! [V__PC,V__MV,V__ROLE] :
   (((s__instance(V__PC,s__Class) &
         s__subclass(V__PC,s__Process) &
         s__instance(V__MV,s__Object) &
         s__instance(V__ROLE,s__CaseRole))
       =>
       (((s__capability(V__PC,V__ROLE,V__MV)
           &
           s__subclass(V__PC,s__Shooting))
         =>
         (( ? [V__WEAPON] :
             ((s__instance(V__WEAPON,s__Weapon) &
                 s__part(V__WEAPON,V__MV)
               &
               s__capability(V__PC,V__ROLE,V__WEAPON))))))))
)
)

MilitaryDevices.kif 48-56
( ! [V__A,V__B,V__G,V__H] :
   (((s__subclass(V__A,s__BodyPart) &
         s__instance(V__A,s__Class) &
         s__subclass(V__B,s__BodyPart) &
         s__instance(V__B,s__Class) &
         s__instance(V__G,s__Object) &
         s__instance(V__H,s__Object))
       =>
       (((s__connectedBodyPart(V__A,V__B)
           &
           s__attribute(V__H,s__Healthy))
         =>
         (( ? [V__AI, V__BI] :
             ((s__instance(V__AI,s__Object) &
                 s__instance(V__BI,s__Object) &
                 (s__instance(V__AI,V__A)
                 &
                 s__instance(V__BI,V__B)
               &
               s__part(V__AI,V__G)
             &
             s__part(V__BI,V__H)
           &
           s__connected(V__AI,V__BI)))))))))
)
)

Mid-level-ontology.kif 11182-11192
( ! [V__ROOM,V__HOTEL] :
   ((s__instance(V__HOTEL,s__Organization) =>
       (((s__element(V__ROOM,s__PropertyFn(V__HOTEL))
         &
         s__attribute(V__ROOM,s__AnnexRoom) &
         s__instance(V__ROOM,s__HotelRoom))
       =>
       (( ? [V__BLDG1, V__BLDG2, V__FRNT] :
           ((s__instance(V__BLDG1,s__Object) &
               s__instance(V__BLDG2,s__Object) &
               (s__subOrganization(V__FRNT,V__HOTEL)
               &
               s__instance(V__FRNT,s__HotelFrontDesk) &
               s__located(V__FRNT,V__BLDG1)
             &
             s__element(V__BLDG1,s__PropertyFn(V__HOTEL))
         &
         s__element(V__BLDG2,s__PropertyFn(V__HOTEL))
     &
     s__part(V__ROOM,V__BLDG2)
   &
   ~((V__BLDG1 = V__BLDG2))))))))))
)
)

Hotel.kif 1105-1118
( ! [V__P1,V__P2,V__L2,V__OP1,V__L,V__OP2] :
   (((s__instance(V__P1,s__Object) &
         s__instance(V__P2,s__Object) &
         s__instance(V__L2,s__Object) &
         s__instance(V__OP1,s__Object) &
         s__instance(V__L,s__Object) &
         s__instance(V__OP2,s__Object))
       =>
       ((((V__L = s__LineFn(V__P1,V__P2))
           &
           s__part(V__OP1,V__L)
         &
         s__part(V__OP2,V__L)
       &
       ~((V__OP1 = V__OP2))
       &
       (V__L2 = s__LineFn(V__OP1,V__OP2)))
   =>
   (s__part(V__L2,V__L)))))
)
)

ComputingBrands.kif 2595-2603
( ! [V__PARTTYPE,V__WHOLE,V__WHOLETYPE,V__PART_TYPE] :
   (((s__instance(V__PARTTYPE,s__Class) &
         s__instance(V__WHOLE,s__Object) &
         s__subclass(V__WHOLETYPE,s__Object) &
         s__instance(V__WHOLETYPE,s__Class) &
         s__subclass(V__PART_TYPE,s__Object))
       =>
       (((s__havePartTypes(V__PART_TYPE,V__WHOLETYPE)
           &
           s__instance(V__WHOLE,V__WHOLETYPE))
       =>
       (( ? [V__PART] :
           ((s__instance(V__PART,s__Object) &
               (s__instance(V__PART,V__PARTTYPE)
               &
               s__part(V__PART,V__WHOLE)))))))))
)
)

Mid-level-ontology.kif 22845-22852
No TPTP formula. May not be expressible in strict first order. Cars.kif 2567-2583
( ! [V__OBJ,V__HOLE1,V__HOLE2] :
   (((s__instance(V__OBJ,s__SelfConnectedObject) &
         s__instance(V__HOLE1,s__Hole) &
         s__instance(V__HOLE2,s__Hole))
       =>
       (((s__hole(V__HOLE1,V__OBJ)
           &
           s__hole(V__HOLE2,V__OBJ))
       =>
       (( ! [V__HOLE3] :
           ((s__instance(V__HOLE3,s__Hole) =>
               ((s__part(V__HOLE3,s__MereologicalSumFn(V__HOLE1,V__HOLE2))
               =>
               (s__hole(V__HOLE3,V__OBJ)))))))))))
)
)

Merge.kif 9495-9502
No TPTP formula. May not be expressible in strict first order. Mid-level-ontology.kif 22800-22809
No TPTP formula. May not be expressible in strict first order. Mid-level-ontology.kif 22827-22835
No TPTP formula. May not be expressible in strict first order. Mid-level-ontology.kif 4284-4298

Display limited to 25 items. Show next 25

Display limited to 25 items. Show next 25

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


( ! [V__PARTTYPE,V__VIR] :
   (((s__subclass(V__PARTTYPE,s__VirusPart) &
         s__instance(V__VIR,s__Virus) &
         s__instance(V__VIR,s__Object))
       =>
       (s__part(s__ViralPartFn(V__VIR,V__PARTTYPE)
      ,V__VIR)))
)
)

VirusProteinAndCellPart.kif 650-650 The viral part of a virus and a kind of virus part is a part of the virus
s__part(s__AtlantaGeorgia,s__Georgia)

CountriesAndRegions.kif 711-711 Atlanta georgia is a part of georgia
s__part(s__Australia,s__Oceania)

CountriesAndRegions.kif 662-662 Australia is a part of oceania
s__part(s__BaltimoreMaryland,s__Maryland)

CountriesAndRegions.kif 714-714 Baltimore maryland is a part of maryland
s__part(s__BostonMassachusetts,s__Massachusetts)

CountriesAndRegions.kif 724-724 Boston, Massachusetts is a part of massachusetts
s__part(s__ChicagoUnitedStates,s__Illinois)

CountriesAndRegions.kif 1611-1611 Chicago united states is a part of illinois
s__part(s__ClevelandOhio,s__Ohio)

CountriesAndRegions.kif 854-854 Cleveland ohio is a part of ohio
s__part(s__Connecticut,s__NewEngland)

CountriesAndRegions.kif 915-915 Connecticut is a part of new england
s__part(s__DallasTexas,s__Texas)

CountriesAndRegions.kif 851-851 Dallas texas is a part of texas
s__part(s__DetroitMichigan,s__Michigan)

CountriesAndRegions.kif 841-841 Detroit michigan is a part of michigan
s__part(s__FargoNorthDakota,s__NorthDakota)

CountriesAndRegions.kif 835-835 Fargo north dakota is a part of north dakota
s__part(s__Germany,s__Europe)

CountriesAndRegions.kif 1242-1242 Germany is a part of europe
s__part(s__Greece,s__Europe)

CountriesAndRegions.kif 1245-1245 Greece is a part of europe
s__part(s__HoustonTexas,s__Texas)

CountriesAndRegions.kif 828-828 Houston texas is a part of texas
s__part(s__HudsonRiver,s__NewYorkState)

CountriesAndRegions.kif 832-832 Hudson river is a part of new york state
s__part(s__KansasCityMissouri,s__Missouri)

CountriesAndRegions.kif 728-728 Kansas city missouri is a part of missouri
s__part(s__KoreanPeninsula,s__Asia)

CountriesAndRegions.kif 820-820 Korean peninsula is a part of asia
s__part(s__LongIsland,s__NewYorkState)

CountriesAndRegions.kif 805-805 Long island is a part of new york state
s__part(s__LosAngelesCalifornia,s__California)

CountriesAndRegions.kif 810-810 Los angeles california is a part of california
s__part(s__ManchesterNewHampshire,s__NewHampshire)

CountriesAndRegions.kif 731-731 Manchester new hampshire is a part of new hampshire
s__part(s__Massachusetts,s__NewEngland)

CountriesAndRegions.kif 989-989 Massachusetts is a part of new england
s__part(s__MemphisTennessee,s__Tennessee)

CountriesAndRegions.kif 733-733 Memphis tennessee is a part of tennessee
s__part(s__MinneapolisMinnesota,s__Minnesota)

CountriesAndRegions.kif 737-737 Minneapolis minnesota is a part of minnesota
s__part(s__MississippiRiver,s__UnitedStates)

CountriesAndRegions.kif 740-740 Mississippi river is a part of united states
s__part(s__MontrealCanada,s__Canada)

CountriesAndRegions.kif 746-746 Montreal canada is a part of canada

Display limited to 25 items. Show next 25

Display limited to 25 items. Show next 25


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

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