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 7494-7497
s__domain(s__temporalPart__m,n__1,s__TimePosition)

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

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

s__instance(s__temporalPart__m,s__PartialOrderingRelation)

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

s__instance(s__TemporalRelation,s__SetOrClass)

Merge.kif 7489-7489 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 1429-1429 typicalTemporalPart is internally related to temporal part
s__relatedInternalConcept(s__typicallyContainsTemporalPart__m,s__temporalPart__m)

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

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

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

domainEnglishFormat.kif 57331-57331

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 7528-7530 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 7513-7517
( ! [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] :
     ((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)))
&
( ! [V__MEMBER] :
(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 1226-1253
( ! [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 8708-8715
( ! [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 8656-8663
( ! [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 8721-8728
( ! [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 8730-8739
( ! [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 8695-8702
( ! [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 8669-8676
( ! [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 8682-8689
No TPTP formula. May not be expressible in strict first order. Cars.kif 1449-1466
No TPTP formula. May not be expressible in strict first order. Cars.kif 1489-1506

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 7738-7744 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__SetOrClass))
     =>
     ((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 11758-11770
No TPTP formula. May not be expressible in strict first order. Mid-level-ontology.kif 14605-14617
( ! [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 11293-11301
No TPTP formula. May not be expressible in strict first order. Mid-level-ontology.kif 20100-20113
( ! [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 7856-7865
No TPTP formula. May not be expressible in strict first order. Mid-level-ontology.kif 15844-15878
( ! [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 2729-2741
( ! [V__WEEK,V__PAPER] :
   (s__instance(V__PAPER,s__SetOrClass) =>
     (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 12533-12542
No TPTP formula. May not be expressible in strict first order. Merge.kif 682-689
No TPTP formula. May not be expressible in strict first order. WMD.kif 899-910
( ! [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 7753-7755
( ! [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 7551-7558
( ! [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 7569-7576
( ! [V__INTERVAL,V__INTERVAL_TYPE,V__CLASS] :
   ((s__instance(V__INTERVAL,s__TimeInterval) &
       s__subclass(V__INTERVAL_TYPE,s__TimeInterval) &
       s__subclass(V__CLASS,s__TimeInterval) &
       s__instance(V__CLASS,s__SetOrClass))
     =>
     (s__TemporalCompositionFn(V__INTERVAL,V__INTERVAL_TYPE)
     = 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 8856-8866
No TPTP formula. May not be expressible in strict first order. Merge.kif 7478-7486
No TPTP formula. May not be expressible in strict first order. Mid-level-ontology.kif 20025-20036
No TPTP formula. May not be expressible in strict first order. Merge.kif 13314-13320
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