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 7715-7718
s__domain(s__temporalPart__m,n__1,s__TimePosition)

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

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

s__instance(s__temporalPart__m,s__BinaryPredicate)

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

s__instance(s__temporalPart__m,s__PartialOrderingRelation)

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

s__instance(s__temporalPart__m,s__TemporalRelation)

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

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

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

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

Merge.kif 7806-7806 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 57418-57418
s__termFormat(s__EnglishLanguage,s__temporalPart__m,'"temporal part"')

domainEnglishFormat.kif 57417-57417

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 7749-7751 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 7734-7738
( ! [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 8936-8943
( ! [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 8884-8891
( ! [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 8949-8956
( ! [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 8958-8967
( ! [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 8923-8930
( ! [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 8897-8904
( ! [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 8910-8917
No TPTP formula. May not be expressible in strict first order. Cars.kif 1453-1470
No TPTP formula. May not be expressible in strict first order. Cars.kif 1493-1510

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 7959-7965 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 12126-12139
No TPTP formula. May not be expressible in strict first order. Mid-level-ontology.kif 16325-16337
( ! [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 11620-11628
No TPTP formula. May not be expressible in strict first order. Mid-level-ontology.kif 21570-21583
( ! [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 8080-8089
No TPTP formula. May not be expressible in strict first order. Mid-level-ontology.kif 17390-17424
( ! [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 2769-2781
( ! [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 14113-14122
No TPTP formula. May not be expressible in strict first order. Merge.kif 683-690
( ! [V__A2,V__COURSE,V__A1] :
   (((s__instance(V__A2,s__Human) &
         s__instance(V__COURSE,s__EducationalCourse) &
         s__instance(V__A1,s__Human))
       =>
       ((s__classmate(V__A1,V__A2,V__COURSE)
         =>
         (( ? [V__CLASS, V__EDU, V__TIME] :
             ((s__instance(V__TIME,s__TimePosition) &
                 (s__instance(V__CLASS,s__GroupOfPeople) &
                   s__instance(V__EDU,s__EducationalProcess) &
                   s__realization(V__EDU,V__COURSE)
                 &
                 s__patient(V__EDU,V__CLASS)
               &
               s__temporalPart(V__TIME,s__WhenFn(V__EDU))
           &
           s__memberAtTime(V__A1,V__CLASS,V__TIME)
         &
         s__memberAtTime(V__A1,V__CLASS,V__TIME)))))))))
)
)

Mid-level-ontology.kif 16091-16102
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 7974-7976
( ! [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 7772-7779
( ! [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 7790-7797
( ! [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 9084-9094
No TPTP formula. May not be expressible in strict first order. Merge.kif 7697-7707
No TPTP formula. May not be expressible in strict first order. Mid-level-ontology.kif 21513-21524
No TPTP formula. May not be expressible in strict first order. Merge.kif 13736-13742

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