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

Formal Language: 



KB Term:  Term intersection
English Word: 

  finishes

Sigma KEE - finishes
finishes

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


s__documentation(s__finishes__m,s__ChineseLanguage,'"(finishes ?INTERVAL1 ?INTERVAL2) 的意思是 ?INTERVAL1 和 ?INTERVAL 2两个是 TimeInterval 有共同的结束 TimePoint,而 ?INTERVAL2 比 ?INTERVAL1 先开始。"')

chinese_format.kif 2704-2706
s__documentation(s__finishes__m,s__EnglishLanguage,'"(finishes ?INTERVAL1 ?INTERVAL2) means that ?INTERVAL1 and ?INTERVAL2 are both TimeIntervals that have the same ending TimePoint and that ?INTERVAL2 begins before ?INTERVAL1."')

Merge.kif 7828-7830
s__domain(s__finishes__m,n__1,s__TimeInterval)

Merge.kif 7825-7825 The number 1 argument of finishes is an instance of time interval
s__domain(s__finishes__m,n__2,s__TimeInterval)

Merge.kif 7826-7826 The number 2 argument of finishes is an instance of time interval
s__instance(s__IrreflexiveRelation,s__Class)

s__instance(s__finishes__m,s__IrreflexiveRelation)

Merge.kif 7823-7823 finishes is an instance of irreflexive relation
s__instance(s__finishes__m,s__TemporalRelation)

s__instance(s__TemporalRelation,s__Class)

Merge.kif 7821-7821 finishes is an instance of temporal relation
s__instance(s__finishes__m,s__TotalValuedRelation)

s__instance(s__TotalValuedRelation,s__Class)

Merge.kif 7824-7824 finishes is an instance of total valued relation
s__instance(s__finishes__m,s__TransitiveRelation)

s__instance(s__TransitiveRelation,s__Class)

Merge.kif 7822-7822 finishes is an instance of transitive relation
s__subrelation(s__finishes__m,s__temporalPart__m)

Merge.kif 7820-7820 finishes is a subrelation of temporal part

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


s__format(s__ChineseLanguage,s__finishes__m,'"%1 %n finishes了才到 %2"')

chinese_format.kif 421-421
s__format(s__EnglishLanguage,s__finishes__m,'"%1 %n{doesnt} finish%p{es} %2"')

english_format.kif 430-430
s__termFormat(s__ChineseLanguage,s__finishes__m,'"完成"')

chinese_format.kif 422-422
s__termFormat(s__ChineseLanguage,s__finishes__m,'"饰面"')

domainEnglishFormat.kif 23871-23871
s__termFormat(s__ChineseTraditionalLanguage,s__finishes__m,'"飾面"')

domainEnglishFormat.kif 23870-23870
s__termFormat(s__EnglishLanguage,s__finishes__m,'"finishes"')

domainEnglishFormat.kif 23869-23869

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


( ! [V__Period,V__End,V__Account] :
   (((s__instance(V__Period,s__TimeInterval) &
         s__instance(V__End,s__Day) &
         s__instance(V__Account,s__FinancialAccount))
       =>
       ((((s__agreementPeriod(V__Account,V__Period)
             &
             s__finishes(V__End,V__Period))
         =>
         s__maturityDate(V__Account,V__End))
     &
     (s__maturityDate(V__Account,V__End)
     =>
     (s__agreementPeriod(V__Account,V__Period)
     &
     s__finishes(V__End,V__Period))))))
)
)

FinancialOntology.kif 602-606 A time interval is an agreement period of a financial account and a day finishes the time interval if and only if the day is a maturity date of the financial account
( ! [V__INTERVAL2,V__INTERVAL1] :
   (((s__instance(V__INTERVAL2,s__TimeInterval) &
         s__instance(V__INTERVAL1,s__TimeInterval))
       =>
       (((s__finishes(V__INTERVAL1,V__INTERVAL2)
           =>
           (s__before(s__BeginFn(V__INTERVAL2)
          ,s__BeginFn(V__INTERVAL1))
       &
       (s__EndFn(V__INTERVAL2)
       = s__EndFn(V__INTERVAL1))))
&
((s__before(s__BeginFn(V__INTERVAL2)
,s__BeginFn(V__INTERVAL1))
&
(s__EndFn(V__INTERVAL2)
= s__EndFn(V__INTERVAL1)))
=>
s__finishes(V__INTERVAL1,V__INTERVAL2)))))
)
)

Merge.kif 7832-7840 A time interval finishes another time interval if and only if the beginning of the other time interval happens before the beginning of the time interval and the end of the other time interval is equal to the end of the time interval
( ! [V__A,V__E,V__I,V__Y] :
   ((s__instance(V__I,s__TimeInterval) =>
       (((s__instance(V__Y,s__Year) &
             s__instance(V__E,s__EasterSunday) &
             s__instance(V__A,s__AscensionThursday) &
             s__during(V__E,V__Y)
           &
           s__during(V__A,V__Y)
         &
         s__starts(V__E,V__I)
       &
       s__finishes(V__A,V__I))
   =>
   (s__duration(V__I,s__MeasureFn(n__40,s__DayDuration))))))
)
)

Media.kif 538-547
( ! [V__P,V__E,V__I,V__Y] :
   ((s__instance(V__I,s__TimeInterval) =>
       (((s__instance(V__Y,s__Year) &
             s__instance(V__E,s__EasterSunday) &
             s__instance(V__P,s__PalmSunday) &
             s__during(V__E,V__Y)
           &
           s__during(V__P,V__Y)
         &
         s__starts(V__P,V__I)
       &
       s__finishes(V__E,V__I))
   =>
   (s__duration(V__I,s__MeasureFn(n__8,s__DayDuration))))))
)
)

Media.kif 473-482
( ! [V__P,V__E,V__I,V__Y] :
   ((s__instance(V__I,s__TimeInterval) =>
       (((s__instance(V__Y,s__Year) &
             s__instance(V__E,s__EasterSunday) &
             s__instance(V__P,s__Pentecost) &
             s__during(V__E,V__Y)
           &
           s__during(V__P,V__Y)
         &
         s__starts(V__E,V__I)
       &
       s__finishes(V__P,V__I))
   =>
   (s__duration(V__I,s__MeasureFn(n__50,s__DayDuration))))))
)
)

Media.kif 559-568
( ! [V__Time,V__Process1,V__Program1,V__Process2,V__Delay,V__Program2] :
   (((s__instance(V__Time,s__TimeInterval) &
         s__instance(V__Program1,s__ComputerProgram) &
         s__instance(V__Delay,s__TimeDuration) &
         s__instance(V__Program2,s__ComputerProgram))
       =>
       ((( ? [V__Time1, V__Time2] :
             ((s__instance(V__Time1,s__TimeInterval) &
                 s__instance(V__Time2,s__TimeInterval) &
                 (s__dependencyDelay(V__Program1,V__Delay)
                 &
                 s__dependencyType(V__Program1,s__ShutdownBlock) &
                 s__hasDependency(V__Program1,V__Program2)
               &
               s__instance(V__Process1,s__ComputerProcess) &
               s__programRunning(V__Process1,V__Program1)
             &
             s__instance(V__Process2,s__ComputerProcess) &
             s__programRunning(V__Process2,V__Program2)
           &
           (s__WhenFn(V__Process2)
           = V__Time2)
         &
         s__finishes(V__Time,V__Time1)
       &
       (s__WhenFn(V__Process2)
       = V__Time2)
     &
     (s__BeginFn(V__Time)
     = s__EndFn(V__Time2))))))
=>
(s__duration(V__Time,V__Delay)))))
)
)

QoSontology.kif 1275-1289

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


( ! [V__Order,V__Period,V__End,V__Time] :
   (((s__instance(V__Order,s__Agreement) &
         s__instance(V__Order,s__Object) &
         s__instance(V__Period,s__TimeInterval) &
         s__instance(V__End,s__TimeInterval) &
         s__instance(V__Time,s__TimeInterval))
       =>
       (((s__attribute(V__Order,s__GTCOrder) &
             s__agreementPeriod(V__Order,V__Period))
         =>
         ((( ? [V__Execute] :
               ((s__instance(V__Execute,s__FillingAnOrder) &
                   s__patient(V__Execute,V__Order)
                 &
                 (s__WhenFn(V__Execute)
                 = V__Time)
               &
               s__overlapsTemporally(V__Time,V__Period))))
       |
       ( ? [V__Cancel] :
         ((s__instance(V__Cancel,s__CancellingAnOrder) &
             s__patient(V__Cancel,V__Order)
           &
           (s__WhenFn(V__Cancel)
           = V__End)
         &
         s__finishes(V__End,V__Period)))))))))
)
)

FinancialOntology.kif 2878-2894
( ! [V__AMBULATE,V__DURATION] :
   ((s__instance(V__DURATION,s__TimeInterval) =>
       (((s__instance(V__AMBULATE,s__Ambulating) &
             (V__DURATION = s__WhenFn(V__AMBULATE)))
         =>
         (( ? [V__STEP1, V__STEPN] :
             ((s__instance(V__STEP1,s__Stepping) &
                 s__instance(V__STEPN,s__Stepping) &
                 s__subProcess(V__STEP1,V__AMBULATE)
               &
               s__subProcess(V__STEPN,V__AMBULATE)
             &
             s__starts(s__WhenFn(V__STEP1)
          ,V__DURATION)
         &
         s__finishes(s__WhenFn(V__STEPN)
      ,V__DURATION)
     &
     ~((V__STEP1 = V__STEPN)))))))))
)
)

Mid-level-ontology.kif 458-470
No TPTP formula. May not be expressible in strict first order. Mid-level-ontology.kif 20436-20451
( ! [V__CHECKIN,V__CHECKOUT,V__SERVICE] :
   ((s__instance(V__SERVICE,s__Process) =>
       (((s__instance(V__CHECKIN,s__CheckInService) &
             s__causes(V__CHECKIN,V__SERVICE)
           &
           s__instance(V__CHECKOUT,s__CheckOutService))
         =>
         (s__finishes(s__WhenFn(V__CHECKOUT)
        ,s__WhenFn(V__SERVICE))))))
)
)

Hotel.kif 2169-2176
No TPTP formula. May not be expressible in strict first order. Mid-level-ontology.kif 15522-15531
( ! [V__OP,V__ORG] :
   (((s__instance(V__OP,s__CeasingOperations) &
         s__instance(V__ORG,s__Organization) &
         s__agent(V__OP,V__ORG))
     =>
     (s__finishes(V__OP,s__WhenFn(V__ORG))))
)
)

Mid-level-ontology.kif 15473-15478
No TPTP formula. May not be expressible in strict first order. Mid-level-ontology.kif 43-54
( ! [V__O1,V__P,V__D1,V__T1,V__T2,V__D2] :
   (((s__instance(V__O1,s__Object) &
         s__instance(V__P,s__Agent) &
         s__instance(V__D1,s__Object))
       =>
       (((s__instance(V__T1,s__Translocation) &
             s__instance(V__T2,s__Translocation) &
             s__origin(V__T1,V__O1)
           &
           s__origin(V__T2,V__D1)
         &
         s__destination(V__T1,V__D1)
       &
       s__destination(V__T2,V__D2)
     &
     s__experiencer(V__T1,V__P)
   &
   s__experiencer(V__T2,V__P))
=>
(( ? [V__T] :
   ((s__instance(V__T,s__Translocation) &
       s__origin(V__T,V__O1)
     &
     s__destination(V__T,V__D2)
   &
   s__subProcess(V__T1,V__T)
&
s__subProcess(V__T2,V__T)
&
s__experiencer(V__T,V__P)
&
s__starts(s__WhenFn(V__T1)
,s__WhenFn(V__T))
&
s__finishes(s__WhenFn(V__T2)
,s__WhenFn(V__T)))))))))
)
)

Merge.kif 10847-10870
No TPTP formula. May not be expressible in strict first order. Mid-level-ontology.kif 15537-15546
No TPTP formula. May not be expressible in strict first order. Cars.kif 3714-3754
No TPTP formula. May not be expressible in strict first order. Mid-level-ontology.kif 19362-19371
( ! [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__Period,V__Date,V__Statement] :
   (((s__instance(V__Period,s__TimeInterval) &
         s__instance(V__Date,s__Day) &
         s__instance(V__Statement,s__BankStatement))
       =>
       (((s__statementPeriod(V__Statement,V__Period)
           &
           s__dateOfStatement(V__Statement,V__Date))
       =>
       (s__finishes(V__Date,V__Period)))))
)
)

FinancialOntology.kif 3982-3986
( ! [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__TimeInterval) &
                 (s__instance(V__TIME,V__CLASS)
                 &
                 s__finishes(V__TIME,V__INTERVAL)))))))))
)
)

Merge.kif 9043-9048
( ! [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__TIME1] :
             ((s__instance(V__TIME1,s__TimeInterval) =>
                 (((s__instance(V__TIME1,V__CLASS)
                     &
                     ~(s__finishes(V__TIME1,V__INTERVAL)))
                 =>
                 (( ? [V__TIME2] :
                     ((s__instance(V__TIME2,s__TimeInterval) &
                         (s__instance(V__TIME2,V__CLASS)
                         &
                         s__meetsTemporally(V__TIME1,V__TIME2)))))))))))))))
)
)

Merge.kif 9050-9060
No TPTP formula. May not be expressible in strict first order. Mid-level-ontology.kif 19568-19578
( ! [V__AM] :
   ((s__instance(V__AM,s__AnteMeridiem) =>
       (( ? [V__D, V__HOUR1, V__HOUR2] :
           ((s__subclass(V__D,s__Day) &
               s__instance(V__HOUR1,s__TimeInterval) &
               s__instance(V__HOUR2,s__TimeInterval) &
               (s__instance(V__HOUR1,s__HourFn(n__24,V__D))
             &
             s__starts(V__HOUR1,V__AM)
           &
           s__instance(V__HOUR2,s__HourFn(n__12,V__D))
       &
       s__finishes(V__HOUR2,V__AM)))))))
)
)

Mid-level-ontology.kif 18128-18135
( ! [V__ARRIVE] :
   ((s__instance(V__ARRIVE,s__Arriving) =>
       (( ? [V__GO] :
           ((s__instance(V__GO,s__Translocation) &
               s__subProcess(V__ARRIVE,V__GO)
             &
             s__finishes(s__WhenFn(V__ARRIVE)
          ,s__WhenFn(V__GO)))))))
)
)

Mid-level-ontology.kif 16410-16416
No TPTP formula. May not be expressible in strict first order. Mid-level-ontology.kif 965-974
( ! [V__DAY] :
   ((s__instance(V__DAY,s__DayTime) =>
       (( ? [V__RISE, V__SET] :
           ((s__instance(V__RISE,s__Sunrise) &
               s__instance(V__SET,s__Sunset) &
               s__starts(V__RISE,V__DAY)
             &
             s__finishes(V__SET,V__DAY))))))
)
)

Merge.kif 8514-8521
( ! [V__INTERVAL,V__TIMECLASS2,V__TIMECLASS1] :
   (((s__instance(V__INTERVAL,s__TimeInterval) &
         s__subclass(V__TIMECLASS2,s__TimeInterval) &
         s__instance(V__TIMECLASS2,s__Class) &
         s__subclass(V__TIMECLASS1,s__TimeInterval) &
         s__instance(V__TIMECLASS1,s__Class))
       =>
       ((s__instance(V__INTERVAL,s__RecurrentTimeIntervalFn(V__TIMECLASS1,V__TIMECLASS2))
       =>
       (( ? [V__TIME1, V__TIME2] :
           ((s__instance(V__TIME1,s__TimeInterval) &
               s__instance(V__TIME2,s__TimeInterval) &
               (s__instance(V__TIME1,V__TIMECLASS1)
               &
               s__instance(V__TIME2,V__TIMECLASS2)
             &
             s__starts(V__TIME1,V__INTERVAL)
           &
           s__finishes(V__TIME2,V__INTERVAL)))))))))
)
)

Merge.kif 8098-8105
( ! [V__INTERVAL] :
   ((s__instance(V__INTERVAL,s__TimeInterval) =>
       (s__finishes(s__ImmediatePastFn(V__INTERVAL)
      ,s__PastFn(V__INTERVAL))))
)
)

Merge.kif 8146-8148
( ! [V__DAY,V__MORNING] :
   ((s__subclass(V__DAY,s__Day) =>
       ((s__instance(V__MORNING,s__Morning) =>
           (( ? [V__HOUR] :
               ((s__instance(V__HOUR,s__TimeInterval) &
                   (s__instance(V__HOUR,s__HourFn(n__12,V__DAY))
                 &
                 s__finishes(V__HOUR,V__MORNING)))))))))
)
)

Merge.kif 8449-8454
No TPTP formula. May not be expressible in strict first order. ArabicCulture.kif 274-288
No TPTP formula. May not be expressible in strict first order. ArabicCulture.kif 294-308

Display limited to 25 items. Show next 25

Display limited to 25 items. Show next 25

statement
-------------------------


No TPTP formula. May not be expressible in strict first order. Media.kif 1972-1980 There exists a time interval such that the time interval is an instance of time interval and the time interval finishes the time of existence of JesusOfNazareth and the time interval starts the time of existence of TwelveApostles and for all an entity


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