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

Formal Language: 



KB Term:  Term intersection
English Word: 

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 7795-7797
s__domain(s__finishes__m,n__1,s__TimeInterval)

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

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

s__instance(s__finishes__m,s__IrreflexiveRelation)

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

s__instance(s__TemporalRelation,s__SetOrClass)

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

s__instance(s__TotalValuedRelation,s__SetOrClass)

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

s__instance(s__TransitiveRelation,s__SetOrClass)

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

Merge.kif 7787-7787 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 7799-7807 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 20086-20101
( ! [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 2156-2163
No TPTP formula. May not be expressible in strict first order. Mid-level-ontology.kif 15173-15182
( ! [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 15124-15129
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 10814-10837
No TPTP formula. May not be expressible in strict first order. Mid-level-ontology.kif 15188-15197
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 19012-19021
( ! [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 9010-9015
( ! [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 9017-9027
No TPTP formula. May not be expressible in strict first order. Mid-level-ontology.kif 19218-19228
( ! [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 17779-17786
( ! [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 16061-16067
No TPTP formula. May not be expressible in strict first order. Mid-level-ontology.kif 964-973
( ! [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 8481-8488
( ! [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 8065-8072
( ! [V__INTERVAL] :
   ((s__instance(V__INTERVAL,s__TimeInterval) =>
       (s__finishes(s__ImmediatePastFn(V__INTERVAL)
      ,s__PastFn(V__INTERVAL))))
)
)

Merge.kif 8113-8115
( ! [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 8416-8421
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