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。')

Merge.kif 8152-8155
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 8148-8151
s__domain(s__temporalPart__m,1,s__TimePosition)

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

Merge.kif 8146-8146 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 8142-8142 temporal part is an instance of binary predicate
s__instance(s__PartialOrderingRelation,s__SetOrClass)

s__instance(s__temporalPart__m,s__PartialOrderingRelation)

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

s__instance(s__TemporalRelation,s__SetOrClass)

Merge.kif 8143-8143 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 253-253
s__relatedInternalConcept(s__typicalTemporalPart__m,s__temporalPart__m)

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

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

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

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

chinese_format.kif 418-418 "时间部分" is the printable form of temporal part in ChineseLanguage
s__termFormat(s__EnglishLanguage,s__temporalPart__m,'temporal part')

domainEnglishFormat.kif 9999-9999 "temporal part" is the printable form of temporal part in english language

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


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

Merge.kif 8186-8188 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 8171-8175
( ! [V__COLL,V__SITE,V__AGENT,V__LISTING,V__TIME] :
   ((s__instance(V__COLL,s__Collection)s__and__ms__instance(V__SITE,s__WebSite)s__and__ms__instance(V__AGENT,s__Agent)s__and__ms__instance(V__LISTING,s__WebListing)s__and__ms__instance(V__TIME,s__TimePoint)s__and__ms__listingSeller(V__LISTING,V__AGENT)
    s__and__m(s__not__ms__member(V__LISTING,V__COLL))
s__and__m(s__forall__m[V__ITEM] :
((s__instance(V__ITEM,s__WebListing)s__and__ms__member(V__ITEM,s__SellersItemsFn(V__AGENT,V__SITE))
s__and__ms__temporalPart(V__TIME,s__WhenFn(V__ITEM))
s__and__m(s__not__m(V__ITEMs__equal__mV__LISTING)))
s__=>s__member(V__ITEM,V__COLL)))
s__and__m(s__forall__m[V__MEMBER] :
(s__member(V__MEMBER,V__COLL)
s__=>(s__temporalPart(V__TIME,s__WhenFn(V__ITEM))
s__and__ms__instance(V__MEMBER,s__WebListing)))))
s__=>(s__SellersOtherItemsFn(V__AGENT,V__SITE,V__LISTING,V__TIME)
s__equal__mV__COLL))
)

UXExperimentalTerms.kif 1229-1256
( ! [V__D,V__M] :
   ((s__instance(V__D,s__EasterSunday)s__and__ms__temporalPart(V__D,V__M)
    s__and__ms__instance(V__M,s__Month))
  s__=>(s__instance(V__M,s__March)s__or__ms__instance(V__M,s__April)s__or__ms__instance(V__M,s__May)))
)

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

Merge.kif 9324-9331
( ! [V__DAY1,V__DAY2,V__WEEK] :
   ((s__instance(V__DAY1,s__Monday)s__and__ms__instance(V__DAY2,s__Tuesday)s__and__ms__instance(V__WEEK,s__Week)s__and__ms__temporalPart(V__DAY1,V__WEEK)
    s__and__ms__temporalPart(V__DAY2,V__WEEK))
s__=>s__meetsTemporally(V__DAY1,V__DAY2))
)

Merge.kif 9272-9279
( ! [V__DAY1,V__DAY2,V__WEEK] :
   ((s__instance(V__DAY1,s__Saturday)s__and__ms__instance(V__DAY2,s__Sunday)s__and__ms__instance(V__WEEK,s__Week)s__and__ms__temporalPart(V__DAY1,V__WEEK)
    s__and__ms__temporalPart(V__DAY2,V__WEEK))
s__=>s__meetsTemporally(V__DAY1,V__DAY2))
)

Merge.kif 9337-9344
( ! [V__DAY1,V__DAY2,V__WEEK1,V__WEEK2] :
   ((s__instance(V__DAY1,s__Sunday)s__and__ms__instance(V__DAY2,s__Monday)s__and__ms__instance(V__WEEK1,s__Week)s__and__ms__instance(V__WEEK2,s__Week)s__and__ms__temporalPart(V__DAY1,V__WEEK1)
    s__and__ms__temporalPart(V__DAY2,V__WEEK2)
  s__and__ms__meetsTemporally(V__WEEK1,V__WEEK2))
s__=>s__meetsTemporally(V__DAY1,V__DAY2))
)

Merge.kif 9346-9355
( ! [V__DAY1,V__DAY2,V__WEEK] :
   ((s__instance(V__DAY1,s__Thursday)s__and__ms__instance(V__DAY2,s__Friday)s__and__ms__instance(V__WEEK,s__Week)s__and__ms__temporalPart(V__DAY1,V__WEEK)
    s__and__ms__temporalPart(V__DAY2,V__WEEK))
s__=>s__meetsTemporally(V__DAY1,V__DAY2))
)

Merge.kif 9311-9318
( ! [V__DAY1,V__DAY2,V__WEEK] :
   ((s__instance(V__DAY1,s__Tuesday)s__and__ms__instance(V__DAY2,s__Wednesday)s__and__ms__instance(V__WEEK,s__Week)s__and__ms__temporalPart(V__DAY1,V__WEEK)
    s__and__ms__temporalPart(V__DAY2,V__WEEK))
s__=>s__meetsTemporally(V__DAY1,V__DAY2))
)

Merge.kif 9285-9292
( ! [V__DAY1,V__DAY2,V__WEEK] :
   ((s__instance(V__DAY1,s__Wednesday)s__and__ms__instance(V__DAY2,s__Thursday)s__and__ms__instance(V__WEEK,s__Week)s__and__ms__temporalPart(V__DAY1,V__WEEK)
    s__and__ms__temporalPart(V__DAY2,V__WEEK))
s__=>s__meetsTemporally(V__DAY1,V__DAY2))
)

Merge.kif 9298-9305
No TPTP formula. May not be expressible in strict first order. Cars.kif 1448-1465
No TPTP formula. May not be expressible in strict first order. Cars.kif 1488-1505

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


( ! [V__INTERVAL2,V__INTERVAL1] :
   ((s__instance(V__INTERVAL2,s__TimeInterval)s__and__ms__instance(V__INTERVAL1,s__TimeInterval))
    s__=>(s__overlapsTemporally(V__INTERVAL1,V__INTERVAL2)
    s__<=>
    (s__exists__m[V__INTERVAL3] :
       (s__instance(V__INTERVAL3,s__TimeInterval)s__and__ms__temporalPart(V__INTERVAL3,V__INTERVAL1)
      s__and__ms__temporalPart(V__INTERVAL3,V__INTERVAL2)))))
)

Merge.kif 8405-8411 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__and__ms__instance(V__Y1,s__TimeInterval)s__and__ms__instance(V__Y2,s__TimeInterval))
    s__=>((s__birthdate(s__JesusOfNazareth,V__DAY)
      s__and__ms__instance(V__Y1,s__YearFn(-6))
  s__and__ms__instance(V__Y2,s__YearFn(4)))
s__=>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__and__ms__instance(V__Y1,s__TimeInterval)s__and__ms__instance(V__Y2,s__TimeInterval))
    s__=>((s__deathdate(s__JesusOfNazareth,V__DAY)
      s__and__ms__instance(V__Y1,s__YearFn(29))
  s__and__ms__instance(V__Y2,s__YearFn(36)))
s__=>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__and__ms__instance(V__PLACE,s__Agent)s__and__ms__subclass(V__YEAR,s__Year)s__and__ms__instance(V__YEAR,s__TimePosition)s__and__ms__subclass(V__PERIOD,s__TimeInterval)s__and__ms__instance(V__PERIOD,s__SetOrClass))
    s__=>(((V__FYs__equal__ms__FiscalYearStartingFn(V__PLACE,V__YEAR))
      s__and__ms__fiscalYearPeriod(V__PLACE,V__PERIOD)
    s__and__ms__instance(V__FY,V__PERIOD))
s__=>(s__exists__m[V__DAY] :
   (s__instance(V__DAY,s__Day)s__and__ms__starts(V__DAY,V__FY)
  s__and__ms__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 12640-12652
No TPTP formula. May not be expressible in strict first order. Mid-level-ontology.kif 14604-14616
( ! [V__B,V__H] :
   (s__instance(V__B,s__TimePoint)s__=>((s__instance(V__H,s__Hanukkah)s__and__m(V__Bs__equal__ms__BeginFn(V__H)))
  s__=>(s__exists__m[V__M] :
     (s__temporalPart(V__B,V__M)
    s__and__ms__instance(V__M,s__Month)s__and__m(s__instance(V__M,s__November)s__or__ms__instance(V__M,s__December))))))
)

Media.kif 587-597
No TPTP formula. May not be expressible in strict first order. Merge.kif 12114-12122
No TPTP formula. May not be expressible in strict first order. Mid-level-ontology.kif 20087-20100
( ! [V__POINT1,V__POINT2,V__INTERVAL] :
   ((s__instance(V__POINT1,s__TimePoint)s__and__ms__instance(V__POINT2,s__TimePoint)s__and__ms__instance(V__INTERVAL,s__TimeInterval)s__and__m(s__TimeIntervalFn(V__POINT1,V__POINT2)
    s__equal__mV__INTERVAL))
  s__=>(s__forall__m[V__POINT] :
     (s__instance(V__POINT,s__TimePoint)s__=>(s__temporallyBetweenOrEqual(V__POINT1,V__POINT,V__POINT2)
      s__<=>
      s__temporalPart(V__POINT,V__INTERVAL)))))
)

Merge.kif 8530-8539
No TPTP formula. May not be expressible in strict first order. Mid-level-ontology.kif 15843-15877
( ! [V__T1,V__T2] :
   ((s__instance(V__T1,s__TimeInterval)s__and__ms__instance(V__T2,s__TimeInterval))
    s__=>((s__instance(V__T1,s__YearFn(26))
    s__and__ms__instance(V__T2,s__YearFn(100)))
s__=>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__and__ms__instance(V__Date,s__TimePoint)s__and__ms__instance(V__Exercise,s__Physical)s__and__ms__instance(V__Option,s__Agreement))
    s__=>((s__property(V__Option,s__EuropeanStyleOption)s__and__ms__agreementExpirationDate(V__Option,V__Date))
    s__=>(s__exists__m[V__Period,V__Time] :
       (s__instance(V__Time,s__TimeInterval)s__and__m(s__instance(V__Period,s__TimeInterval)s__and__ms__finishes(V__Period,V__Date)
      s__and__m((s__instance(V__Exercise,s__ExerciseAnOption)s__and__m(s__WhenFn(V__Exercise)
      s__equal__mV__Time))
    s__=>s__temporalPart(V__Time,V__Period)))))))
)

FinancialOntology.kif 2728-2740
( ! [V__PAPER,V__WEEK] :
   (s__instance(V__PAPER,s__SetOrClass)s__=>((s__subclass(V__PAPER,s__Newspaper)s__and__ms__instance(V__WEEK,s__Week))
      s__=>(s__exists__m[V__PUBLICATION,V__ISSUE] :
         (s__instance(V__PUBLICATION,s__Publication)s__and__ms__temporalPart(s__WhenFn(V__PUBLICATION)
        ,V__WEEK)
      s__and__ms__result(V__PUBLICATION,V__ISSUE)
    s__and__ms__instance(V__ISSUE,V__PAPER)))))
)

Mid-level-ontology.kif 12533-12542
No TPTP formula. May not be expressible in strict first order. Merge.kif 746-753
No TPTP formula. May not be expressible in strict first order. WMD.kif 890-901
( ! [V__BIG,V__SMALL] :
   ((s__instance(V__BIG,s__TimeInterval)s__and__ms__instance(V__SMALL,s__TimeInterval))
    s__=>(s__during(V__SMALL,V__BIG)
    s__=>s__temporalPart(V__SMALL,V__BIG)))
)

Merge.kif 8420-8422
( ! [V__INTERVAL,V__POINT] :
   ((s__instance(V__INTERVAL,s__TimeInterval)s__and__ms__instance(V__POINT,s__TimePoint))
    s__=>((s__BeginFn(V__INTERVAL)
      s__equal__mV__POINT)s__=>(s__forall__m[V__OTHERPOINT] :
         (s__instance(V__OTHERPOINT,s__TimePoint)s__=>((s__temporalPart(V__OTHERPOINT,V__INTERVAL)
            s__and__m(s__not__m(V__OTHERPOINTs__equal__mV__POINT)))
        s__=>s__before(V__POINT,V__OTHERPOINT))))))
)

Merge.kif 8205-8212
( ! [V__INTERVAL,V__POINT] :
   ((s__instance(V__INTERVAL,s__TimeInterval)s__and__ms__instance(V__POINT,s__TimePoint))
    s__=>((s__EndFn(V__INTERVAL)
      s__equal__mV__POINT)s__=>(s__forall__m[V__OTHERPOINT] :
         (s__instance(V__OTHERPOINT,s__TimePoint)s__=>((s__temporalPart(V__OTHERPOINT,V__INTERVAL)
            s__and__m(s__not__m(V__OTHERPOINTs__equal__mV__POINT)))
        s__=>s__before(V__OTHERPOINT,V__POINT))))))
)

Merge.kif 8224-8231
( ! [V__INTERVAL,V__INTERVAL_TYPE,V__CLASS] :
   ((s__instance(V__INTERVAL,s__TimeInterval)s__and__ms__subclass(V__INTERVAL_TYPE,s__TimeInterval)s__and__ms__subclass(V__CLASS,s__TimeInterval)s__and__ms__instance(V__CLASS,s__SetOrClass))
    s__=>((s__TemporalCompositionFn(V__INTERVAL,V__INTERVAL_TYPE)
      s__equal__mV__CLASS)s__=>(s__forall__m[V__TIME] :
         ((s__instance(V__TIME,s__TimePoint)s__and__ms__temporalPart(V__TIME,V__INTERVAL))
        s__=>(s__exists__m[V__INSTANCE] :
           (s__instance(V__INSTANCE,s__TimePosition)s__and__m(s__instance(V__INSTANCE,V__CLASS)
          s__and__ms__temporalPart(V__TIME,V__INSTANCE))))))))
)

Merge.kif 9476-9486
No TPTP formula. May not be expressible in strict first order. Merge.kif 8132-8140
No TPTP formula. May not be expressible in strict first order. Mid-level-ontology.kif 20012-20023
No TPTP formula. May not be expressible in strict first order. Merge.kif 14417-14423
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 2.99c (>= 2017/11/20) is open source software produced by Articulate Software and its partners