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

Formal Language: 



KB Term:  Term intersection
English Word: 

Sigma KEE - temporalPart
temporalPart

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


s__documentation(s__temporalPart__m,s__ChineseLanguage,'"这是类似空间谓词 part 的时间部分。 (temporalPart ?POS1 ?POS2)的意思是 TimePosition ?POS1 是 TimePosition ?POS2 的一部分。 注:因为 temporalPartReflexiveRelation,所以每个 TimePostion 都是它本身的 一个 temporalPart。"')

chinese_format.kif 2693-2696
s__documentation(s__temporalPart__m,s__EnglishLanguage,'"The temporal analogue of the spatial part predicate. (temporalPart ?POS1 ?POS2) means that TimePosition ?POS1 is part of TimePosition ?POS2. Note that since temporalPart is a ReflexiveRelation every TimePostion is a temporalPart of itself."')

Merge.kif 7674-7677
s__domain(s__temporalPart__m,n__1,s__TimePosition)

Merge.kif 7671-7671 The number 1 argument of temporal part is an instance of time position
s__domain(s__temporalPart__m,n__2,s__TimePosition)

Merge.kif 7672-7672 The number 2 argument of temporal part is an instance of time position
s__instance(s__BinaryPredicate,s__SetOrClass)

s__instance(s__temporalPart__m,s__BinaryPredicate)

Merge.kif 7668-7668 temporal part is an instance of binary predicate
s__instance(s__PartialOrderingRelation,s__SetOrClass)

s__instance(s__temporalPart__m,s__PartialOrderingRelation)

Merge.kif 7670-7670 temporal part is an instance of partial ordering relation
s__instance(s__temporalPart__m,s__TemporalRelation)

s__instance(s__TemporalRelation,s__SetOrClass)

Merge.kif 7669-7669 temporal part is an instance of temporal relation

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


s__format(s__ChineseLanguage,s__temporalPart__m,'"%1 时段 %n 是 %2 时段 的一 part"')

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

english_format.kif 426-426
s__relatedInternalConcept(s__typicalTemporalPart__m,s__temporalPart__m)

Cars.kif 1447-1447 typicalTemporalPart is internally related to temporal part
s__relatedInternalConcept(s__typicallyContainsTemporalPart__m,s__temporalPart__m)

Cars.kif 1489-1489 typicallyContainsTemporalPart is internally related to temporal part
s__subrelation(s__finishes__m,s__temporalPart__m)

Merge.kif 7787-7787 finishes is a subrelation of temporal part
s__subrelation(s__starts__m,s__temporalPart__m)

Merge.kif 7765-7765 starts is a subrelation of temporal part
s__termFormat(s__ChineseLanguage,s__temporalPart__m,'"时间部分"')

chinese_format.kif 418-418
s__termFormat(s__ChineseTraditionalLanguage,s__temporalPart__m,'"時間部分"')

domainEnglishFormat.kif 57417-57417
s__termFormat(s__EnglishLanguage,s__temporalPart__m,'"temporal part"')

domainEnglishFormat.kif 57416-57416

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


( ! [V__POS,V__THING] :
   (((s__instance(V__POS,s__TimePosition) &
         s__instance(V__THING,s__Physical))
       =>
       (((s__temporalPart(V__POS,s__WhenFn(V__THING))
         =>
         s__time(V__THING,V__POS))
     &
     (s__time(V__THING,V__POS)
     =>
     s__temporalPart(V__POS,s__WhenFn(V__THING))))))
)
)

Merge.kif 7708-7710 A time position is a part of the time of existence of a physical if and only if the physical exists during the time position
No TPTP formula. May not be expressible in strict first order. Merge.kif 7693-7697
( ! [V__AGENT,V__TIME,V__SITE,V__LISTING,V__COLL] :
   (((s__instance(V__COLL,s__Collection) &
         s__instance(V__SITE,s__WebSite) &
         s__instance(V__AGENT,s__Agent) &
         s__instance(V__LISTING,s__WebListing) &
         s__instance(V__TIME,s__TimePoint) &
         s__listingSeller(V__LISTING,V__AGENT)
       &
       ~(s__member(V__LISTING,V__COLL))
     &
     ( ! [V__ITEM, V__MEMBER] :
       ((((s__instance(V__ITEM,s__WebListing) &
               s__member(V__ITEM,s__SellersItemsFn(V__AGENT,V__SITE))
           &
           s__temporalPart(V__TIME,s__WhenFn(V__ITEM))
       &
       ~((V__ITEM = V__LISTING)))
     =>
     (s__member(V__ITEM,V__COLL)))
&
(s__member(V__MEMBER,V__COLL)
=>
((s__temporalPart(V__TIME,s__WhenFn(V__ITEM))
&
s__instance(V__MEMBER,s__WebListing))))))))
=>
((s__SellersOtherItemsFn(V__AGENT,V__SITE,V__LISTING,V__TIME)
= V__COLL)))
)
)

UXExperimentalTerms.kif 1230-1257
( ! [V__D,V__M] :
   (((s__instance(V__D,s__EasterSunday) &
         s__temporalPart(V__D,V__M)
       &
       s__instance(V__M,s__Month))
     =>
     ((s__instance(V__M,s__March) |
         s__instance(V__M,s__April) |
         s__instance(V__M,s__May))))
   )
)

Media.kif 498-506
( ! [V__DAY2,V__DAY1,V__WEEK] :
   (((s__instance(V__DAY1,s__Friday) &
         s__instance(V__DAY2,s__Saturday) &
         s__instance(V__WEEK,s__Week) &
         s__temporalPart(V__DAY1,V__WEEK)
       &
       s__temporalPart(V__DAY2,V__WEEK))
   =>
   (s__meetsTemporally(V__DAY1,V__DAY2)))
)
)

Merge.kif 8893-8900
( ! [V__DAY2,V__DAY1,V__WEEK] :
   (((s__instance(V__DAY1,s__Monday) &
         s__instance(V__DAY2,s__Tuesday) &
         s__instance(V__WEEK,s__Week) &
         s__temporalPart(V__DAY1,V__WEEK)
       &
       s__temporalPart(V__DAY2,V__WEEK))
   =>
   (s__meetsTemporally(V__DAY1,V__DAY2)))
)
)

Merge.kif 8841-8848
( ! [V__DAY2,V__DAY1,V__WEEK] :
   (((s__instance(V__DAY1,s__Saturday) &
         s__instance(V__DAY2,s__Sunday) &
         s__instance(V__WEEK,s__Week) &
         s__temporalPart(V__DAY1,V__WEEK)
       &
       s__temporalPart(V__DAY2,V__WEEK))
   =>
   (s__meetsTemporally(V__DAY1,V__DAY2)))
)
)

Merge.kif 8906-8913
( ! [V__DAY2,V__DAY1,V__WEEK2,V__WEEK1] :
   (((s__instance(V__DAY1,s__Sunday) &
         s__instance(V__DAY2,s__Monday) &
         s__instance(V__WEEK1,s__Week) &
         s__instance(V__WEEK2,s__Week) &
         s__temporalPart(V__DAY1,V__WEEK1)
       &
       s__temporalPart(V__DAY2,V__WEEK2)
     &
     s__meetsTemporally(V__WEEK1,V__WEEK2))
=>
(s__meetsTemporally(V__DAY1,V__DAY2)))
)
)

Merge.kif 8915-8924
( ! [V__DAY2,V__DAY1,V__WEEK] :
   (((s__instance(V__DAY1,s__Thursday) &
         s__instance(V__DAY2,s__Friday) &
         s__instance(V__WEEK,s__Week) &
         s__temporalPart(V__DAY1,V__WEEK)
       &
       s__temporalPart(V__DAY2,V__WEEK))
   =>
   (s__meetsTemporally(V__DAY1,V__DAY2)))
)
)

Merge.kif 8880-8887
( ! [V__DAY2,V__DAY1,V__WEEK] :
   (((s__instance(V__DAY1,s__Tuesday) &
         s__instance(V__DAY2,s__Wednesday) &
         s__instance(V__WEEK,s__Week) &
         s__temporalPart(V__DAY1,V__WEEK)
       &
       s__temporalPart(V__DAY2,V__WEEK))
   =>
   (s__meetsTemporally(V__DAY1,V__DAY2)))
)
)

Merge.kif 8854-8861
( ! [V__DAY2,V__DAY1,V__WEEK] :
   (((s__instance(V__DAY1,s__Wednesday) &
         s__instance(V__DAY2,s__Thursday) &
         s__instance(V__WEEK,s__Week) &
         s__temporalPart(V__DAY1,V__WEEK)
       &
       s__temporalPart(V__DAY2,V__WEEK))
   =>
   (s__meetsTemporally(V__DAY1,V__DAY2)))
)
)

Merge.kif 8867-8874
No TPTP formula. May not be expressible in strict first order. Cars.kif 1467-1484
No TPTP formula. May not be expressible in strict first order. Cars.kif 1507-1524

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


( ! [V__INTERVAL2,V__INTERVAL1] :
   (((s__instance(V__INTERVAL2,s__TimeInterval) &
         s__instance(V__INTERVAL1,s__TimeInterval))
       =>
       (((s__overlapsTemporally(V__INTERVAL1,V__INTERVAL2)
           =>
           ( ? [V__INTERVAL3] :
             ((s__instance(V__INTERVAL3,s__TimeInterval) &
                 s__temporalPart(V__INTERVAL3,V__INTERVAL1)
               &
               s__temporalPart(V__INTERVAL3,V__INTERVAL2)))))
     &
     (( ? [V__INTERVAL3] :
         ((s__instance(V__INTERVAL3,s__TimeInterval) &
             s__temporalPart(V__INTERVAL3,V__INTERVAL1)
           &
           s__temporalPart(V__INTERVAL3,V__INTERVAL2))))
   =>
   s__overlapsTemporally(V__INTERVAL1,V__INTERVAL2)))))
)
)

Merge.kif 7918-7924 A time interval overlaps another time interval if and only if there exists a time position such that the time position is an instance of time interval and the time position is a part of the other time interval and the time position is a part of the time interval
( ! [V__DAY,V__Y1,V__Y2] :
   (((s__instance(V__DAY,s__Day) &
         s__instance(V__Y1,s__TimeInterval) &
         s__instance(V__Y2,s__TimeInterval))
       =>
       (((s__birthdate(s__JesusOfNazareth,V__DAY)
           &
           s__instance(V__Y1,s__YearFn(n___6))
       &
       s__instance(V__Y2,s__YearFn(n__4)))
=>
(s__temporalPart(V__DAY,s__TimeIntervalFn(s__BeginFn(V__Y1)
,s__EndFn(V__Y2)))))))
)
)

Media.kif 1938-1943
( ! [V__DAY,V__Y1,V__Y2] :
   (((s__instance(V__DAY,s__Day) &
         s__instance(V__Y1,s__TimeInterval) &
         s__instance(V__Y2,s__TimeInterval))
       =>
       (((s__deathdate(s__JesusOfNazareth,V__DAY)
           &
           s__instance(V__Y1,s__YearFn(n__29))
       &
       s__instance(V__Y2,s__YearFn(n__36)))
=>
(s__temporalPart(V__DAY,s__TimeIntervalFn(s__BeginFn(V__Y1)
,s__EndFn(V__Y2)))))))
)
)

Media.kif 1945-1950
( ! [V__FY,V__PLACE,V__YEAR,V__PERIOD] :
   (((s__instance(V__FY,s__TimeInterval) &
         s__instance(V__PLACE,s__Agent) &
         s__subclass(V__YEAR,s__Year) &
         s__instance(V__YEAR,s__TimePosition) &
         s__subclass(V__PERIOD,s__TimeInterval) &
         s__instance(V__PERIOD,s__Class))
       =>
       ((((V__FY = s__FiscalYearStartingFn(V__PLACE,V__YEAR))
           &
           s__fiscalYearPeriod(V__PLACE,V__PERIOD)
         &
         s__instance(V__FY,V__PERIOD))
     =>
     (( ? [V__DAY] :
         ((s__instance(V__DAY,s__Day) &
             s__starts(V__DAY,V__FY)
           &
           s__temporalPart(V__DAY,V__YEAR))))))))
)
)

Economy.kif 3755-3764
No TPTP formula. May not be expressible in strict first order. MilitaryPersons.kif 151-167
No TPTP formula. May not be expressible in strict first order. Merge.kif 12082-12094
No TPTP formula. May not be expressible in strict first order. Mid-level-ontology.kif 15133-15145
( ! [V__B,V__H] :
   ((s__instance(V__B,s__TimePoint) =>
       (((s__instance(V__H,s__Hanukkah) &
             (V__B = s__BeginFn(V__H)))
         =>
         (( ? [V__M] :
             ((s__temporalPart(V__B,V__M)
               &
               s__instance(V__M,s__Month) &
               (s__instance(V__M,s__November) |
                 s__instance(V__M,s__December)))))))))
)
)

Media.kif 587-597
No TPTP formula. May not be expressible in strict first order. Merge.kif 11576-11584
No TPTP formula. May not be expressible in strict first order. Mid-level-ontology.kif 20348-20361
( ! [V__POINT2,V__POINT1,V__INTERVAL] :
   (((s__instance(V__POINT1,s__TimePoint) &
         s__instance(V__POINT2,s__TimePoint) &
         s__instance(V__INTERVAL,s__TimeInterval) &
         (s__TimeIntervalFn(V__POINT1,V__POINT2)
         = V__INTERVAL))
     =>
     (( ! [V__POINT] :
         ((s__instance(V__POINT,s__TimePoint) =>
             (((s__temporallyBetweenOrEqual(V__POINT1,V__POINT,V__POINT2)
                 =>
                 s__temporalPart(V__POINT,V__INTERVAL))
             &
             (s__temporalPart(V__POINT,V__INTERVAL)
             =>
             s__temporallyBetweenOrEqual(V__POINT1,V__POINT,V__POINT2)))))))))
)
)

Merge.kif 8039-8048
No TPTP formula. May not be expressible in strict first order. Mid-level-ontology.kif 16198-16232
( ! [V__T1,V__T2] :
   (((s__instance(V__T1,s__TimeInterval) &
         s__instance(V__T2,s__TimeInterval))
       =>
       (((s__instance(V__T1,s__YearFn(n__26))
         &
         s__instance(V__T2,s__YearFn(n__100)))
   =>
   (s__temporalPart(s__WhenFn(s__TwelveApostles),s__TimeIntervalFn(s__BeginFn(V__T1)
  ,s__EndFn(V__T2)))))))
)
)

Media.kif 1961-1965
( ! [V__Date,V__Exercise,V__Option] :
   (((s__instance(V__Date,s__TimeInterval) &
         s__instance(V__Date,s__TimePoint) &
         s__instance(V__Exercise,s__Physical) &
         s__instance(V__Option,s__Agreement))
       =>
       (((s__property(V__Option,s__EuropeanStyleOption) &
             s__agreementExpirationDate(V__Option,V__Date))
         =>
         (( ? [V__Period, V__Time] :
             ((s__instance(V__Time,s__TimeInterval) &
                 (s__instance(V__Period,s__TimeInterval) &
                   s__finishes(V__Period,V__Date)
                 &
                 ((s__instance(V__Exercise,s__ExerciseAnOption) &
                     (s__WhenFn(V__Exercise)
                     = V__Time))
                 =>
                 (s__temporalPart(V__Time,V__Period)))))))))))
)
)

FinancialOntology.kif 2748-2760
( ! [V__WEEK,V__PAPER] :
   ((s__instance(V__PAPER,s__Class) =>
       (((s__subclass(V__PAPER,s__Newspaper) &
             s__instance(V__WEEK,s__Week))
           =>
           (( ? [V__PUBLICATION, V__ISSUE] :
               ((s__instance(V__PUBLICATION,s__Publication) &
                   s__temporalPart(s__WhenFn(V__PUBLICATION)
                ,V__WEEK)
               &
               s__result(V__PUBLICATION,V__ISSUE)
             &
             s__instance(V__ISSUE,V__PAPER))))))))
)
)

Mid-level-ontology.kif 13028-13037
No TPTP formula. May not be expressible in strict first order. Merge.kif 683-690
No TPTP formula. May not be expressible in strict first order. WMD.kif 932-943
( ! [V__BIG,V__SMALL] :
   (((s__instance(V__BIG,s__TimeInterval) &
         s__instance(V__SMALL,s__TimeInterval))
       =>
       ((s__during(V__SMALL,V__BIG)
         =>
         (s__temporalPart(V__SMALL,V__BIG)))))
)
)

Merge.kif 7933-7935
( ! [V__INTERVAL,V__POINT] :
   (((s__instance(V__INTERVAL,s__TimeInterval) &
         s__instance(V__POINT,s__TimePoint))
       =>
       (((s__BeginFn(V__INTERVAL)
           = V__POINT)
         =>
         (( ! [V__OTHERPOINT] :
             ((s__instance(V__OTHERPOINT,s__TimePoint) =>
                 (((s__temporalPart(V__OTHERPOINT,V__INTERVAL)
                     &
                     ~((V__OTHERPOINT = V__POINT)))
                   =>
                   (s__before(V__POINT,V__OTHERPOINT)))))))))))
)
)

Merge.kif 7731-7738
( ! [V__INTERVAL,V__POINT] :
   (((s__instance(V__INTERVAL,s__TimeInterval) &
         s__instance(V__POINT,s__TimePoint))
       =>
       (((s__EndFn(V__INTERVAL)
           = V__POINT)
         =>
         (( ! [V__OTHERPOINT] :
             ((s__instance(V__OTHERPOINT,s__TimePoint) =>
                 (((s__temporalPart(V__OTHERPOINT,V__INTERVAL)
                     &
                     ~((V__OTHERPOINT = V__POINT)))
                   =>
                   (s__before(V__OTHERPOINT,V__POINT)))))))))))
)
)

Merge.kif 7749-7756
( ! [V__INTERVALTYPE,V__INTERVAL,V__CLASS] :
   (((s__subclass(V__INTERVALTYPE,s__TimeInterval) &
         s__instance(V__INTERVAL,s__TimeInterval) &
         s__subclass(V__CLASS,s__TimeInterval) &
         s__instance(V__CLASS,s__Class))
       =>
       (((s__TemporalCompositionFn(V__INTERVAL,V__INTERVALTYPE)
           = V__CLASS)
         =>
         (( ! [V__TIME] :
             (((s__instance(V__TIME,s__TimePoint) &
                   s__temporalPart(V__TIME,V__INTERVAL))
               =>
               (( ? [V__INSTANCE] :
                   ((s__instance(V__INSTANCE,s__TimePosition) &
                       (s__instance(V__INSTANCE,V__CLASS)
                       &
                       s__temporalPart(V__TIME,V__INSTANCE)))))))))))))
)
)

Merge.kif 9041-9051
No TPTP formula. May not be expressible in strict first order. Merge.kif 7656-7666
No TPTP formula. May not be expressible in strict first order. Mid-level-ontology.kif 20291-20302
No TPTP formula. May not be expressible in strict first order. Merge.kif 13691-13697
No TPTP formula. May not be expressible in strict first order. Media.kif 1834-1841

Display limited to 25 items. Show next 25

Display limited to 25 items. Show next 25


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