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 7615-7617
s__domain(s__finishes__m,n__1,s__TimeInterval)

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

Merge.kif 7613-7613 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 7610-7610 finishes is an instance of irreflexive relation
s__instance(s__finishes__m,s__TemporalRelation)

s__instance(s__TemporalRelation,s__SetOrClass)

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

s__instance(s__TotalValuedRelation,s__SetOrClass)

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

s__instance(s__TransitiveRelation,s__SetOrClass)

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

Merge.kif 7607-7607 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 23803-23803
s__termFormat(s__ChineseTraditionalLanguage,s__finishes__m,'"飾面"')

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

domainEnglishFormat.kif 23801-23801

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 601-605 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 7619-7627 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 2838-2854
( ! [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 660-672
No TPTP formula. May not be expressible in strict first order. Mid-level-ontology.kif 19112-19127
( ! [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 2142-2149
No TPTP formula. May not be expressible in strict first order. Mid-level-ontology.kif 14026-14035
( ! [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 13978-13983
No TPTP formula. May not be expressible in strict first order. Mid-level-ontology.kif 159-170
( ! [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 10531-10554
No TPTP formula. May not be expressible in strict first order. Mid-level-ontology.kif 14041-14050
No TPTP formula. May not be expressible in strict first order. Cars.kif 3684-3724
No TPTP formula. May not be expressible in strict first order. Mid-level-ontology.kif 18118-18127
( ! [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__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 3913-3917
( ! [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__TimeInterval) &
         (s__instance(V__TIME,V__CLASS)
         &
         s__finishes(V__TIME,V__INTERVAL)))))
)
)

Merge.kif 8825-8830
( ! [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__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 8832-8842
( ! [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 16880-16887
( ! [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 14873-14879
No TPTP formula. May not be expressible in strict first order. Mid-level-ontology.kif 1405-1414
( ! [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 8297-8304
( ! [V__INTERVAL,V__TIMECLASS2,V__TIMECLASS1] :
   ((s__instance(V__INTERVAL,s__TimeInterval) &
       s__subclass(V__TIMECLASS2,s__TimeInterval) &
       s__instance(V__TIMECLASS2,s__SetOrClass) &
       s__subclass(V__TIMECLASS1,s__TimeInterval) &
       s__instance(V__TIMECLASS1,s__SetOrClass))
     =>
     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 7882-7889
( ! [V__INTERVAL] :
   (s__instance(V__INTERVAL,s__TimeInterval) =>
     s__finishes(s__ImmediatePastFn(V__INTERVAL)
  ,s__PastFn(V__INTERVAL))
)
)

Merge.kif 7930-7932
( ! [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 8232-8237
No TPTP formula. May not be expressible in strict first order. ArabicCulture.kif 272-286
No TPTP formula. May not be expressible in strict first order. ArabicCulture.kif 292-306
No TPTP formula. May not be expressible in strict first order. Mid-level-ontology.kif 17493-17499

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 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