Browsing Interface : Welcome guest : log in
|
Browsing Interface : Welcome guest : log in |
[
Home |
Graph |
LogLearn |
Editor |
]
KB:
Language:
Formal Language:
|
| BeginFn |
| appearance as argument number 1 |
|
| s__instance(s__BeginFn,s__TemporalRelation)
|
Merge.kif 8153-8153 | Begin is an instance of temporal relation |
| s__instance(s__BeginFn,s__UnaryFunction)
|
Merge.kif 8154-8154 | Begin is an instance of unary function |
| s__instance(s__BeginFn,s__TotalValuedRelation)
|
Merge.kif 8155-8155 | Begin is an instance of total valued relation |
| s__domain(s__BeginFn,n__1,s__TimeInterval)
|
Merge.kif 8156-8156 | The number 1 argument of begin is an instance of timeframe |
| s__range(s__BeginFn,s__TimePoint)
|
Merge.kif 8157-8157 | The range of begin is an instance of time point |
| s__documentation(s__BeginFn, s__EnglishLanguage, "A UnaryFunction that maps a TimeInterval to the TimePoint at which the interval begins_") | Merge.kif 8159-8160 | The range of begin is an instance of time point |
| appearance as argument number 2 |
|
|
| antecedent |
|
|
| ! [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 8172-8179 | If equal the beginning of X and Y, then For all TimePoint Z: if Z is a part of X and equal Z and Y, then Y happens before Z |
| ! [V__OBJ : $i,V__PROC : $i,V__QUANT1 : $real,V__QUANT2 : $real] : (((s__resource(V__PROC, V__OBJ) & s__holdsDuring(s__BeginFn(s__WhenFn(V__PROC)), s__measure(V__OBJ, V__QUANT1)) & s__holdsDuring(s__EndFn(s__WhenFn(V__PROC)), s__measure(V__OBJ, V__QUANT2))) => ($greater(V__QUANT1,V__QUANT2)))) | Merge.kif 8199-8204 | If X is a resource for Y, the measure of X is Z holds during the beginning of the time of existence of Y, and the measure of X is W holds during the end of the time of existence of Y, then Z is greater than W |
| ! [V__INTERVAL1,V__INTERVAL2] : (((s__instance(V__INTERVAL1,s__TimeInterval) & s__instance(V__INTERVAL2,s__TimeInterval)) => (((s__BeginFn(V__INTERVAL1) = s__BeginFn(V__INTERVAL2)) & s__before(s__EndFn(V__INTERVAL1) ,s__EndFn(V__INTERVAL2))) => s__starts(V__INTERVAL1,V__INTERVAL2))) )
|
Merge.kif 8228-8236 | If equal the beginning of X and the beginning of Y and the end of X happens before the end of Y, then X starts Y |
| ! [V__INTERVAL2,V__INTERVAL1] : (((s__instance(V__INTERVAL2,s__TimeInterval) & s__instance(V__INTERVAL1,s__TimeInterval)) => ((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 8260-8268 | If the beginning of X happens before the beginning of Y and equal the end of X and the end of Y, then Y finishes X |
| ! [V__PHYS,V__TIME] : (((s__instance(V__PHYS,s__Physical) & s__instance(V__TIME,s__TimePoint)) => (s__temporallyBetweenOrEqual(s__BeginFn(s__WhenFn(V__PHYS)) ,V__TIME,s__EndFn(s__WhenFn(V__PHYS))) => (s__time(V__PHYS,V__TIME) & s__instance(V__TIME,s__TimePoint)))) )
|
Merge.kif 8414-8423 | If X is between or at the beginning of the time of existence of Y and the end of the time of existence of Y, then Y exists during X and X is an instance of time point |
| ! [V__S,V__E,V__TI] : (((s__instance(V__S,s__TimePoint) & s__instance(V__E,s__TimePoint)) => ((s__instance(V__TI,s__TimeInterval) & (V__S = s__BeginFn(V__TI)) & (V__E = s__EndFn(V__TI))) => s__before(V__S,V__E))) )
|
Merge.kif 8464-8469 | If X is an instance of timeframe, equal Y and the beginning of X, and equal Z and the end of X, then Y happens before Z |
| ! [V__TI1,V__TI2] : (((s__instance(V__TI1,s__TimeInterval) & s__instance(V__TI2,s__TimeInterval) & s__beforeOrEqual(s__BeginFn(V__TI2) ,s__BeginFn(V__TI1)) & s__before(s__BeginFn(V__TI1) ,s__EndFn(V__TI2))) => s__overlapsTemporally(V__TI2,V__TI1)) )
|
Merge.kif 8471-8481 | If X is an instance of timeframe, Y is an instance of timeframe, the beginning of Y happens before or at the beginning of X, and the beginning of X happens before the end of Y, then X overlaps Y |
| ! [V__INTERVAL1,V__INTERVAL2] : (((s__instance(V__INTERVAL1,s__TimeInterval) & s__instance(V__INTERVAL2,s__TimeInterval)) => ((s__EndFn(V__INTERVAL1) = s__BeginFn(V__INTERVAL2)) => s__meetsTemporally(V__INTERVAL1,V__INTERVAL2))) )
|
Merge.kif 8541-8545 | If equal the end of X and the beginning of Y, then X meets Y |
| ! [V__INTERVAL1,V__INTERVAL2] : (((s__instance(V__INTERVAL1,s__TimeInterval) & s__instance(V__INTERVAL2,s__TimeInterval) & (s__BeginFn(V__INTERVAL1) = s__BeginFn(V__INTERVAL2)) & (s__EndFn(V__INTERVAL1) = s__EndFn(V__INTERVAL2))) => (V__INTERVAL1 = V__INTERVAL2)) )
|
Merge.kif 8556-8566 | If X is an instance of timeframe, Y is an instance of timeframe, equal the beginning of X and the beginning of Y, and equal the end of X and the end of Y, then equal X and Y |
| ! [V__INTERVAL1,V__INTERVAL2] : (((s__instance(V__INTERVAL1,s__TimeInterval) & s__instance(V__INTERVAL2,s__TimeInterval)) => (s__before(s__EndFn(V__INTERVAL1) ,s__BeginFn(V__INTERVAL2)) => s__earlier(V__INTERVAL1,V__INTERVAL2))) )
|
Merge.kif 8584-8586 | If the end of X happens before the beginning of Y, then X happens earlier than Y |
| ! [V__Y1,V__N1,V__Y2,V__N2,V__T1,V__T2] : (((s__instance(V__Y1,s__TimeInterval) & s__instance(V__N1,s__Integer) & s__instance(V__Y2,s__TimeInterval) & s__instance(V__N2,s__Integer) & s__instance(V__T1,s__TimePoint) & s__instance(V__T2,s__TimePoint)) => ((s__instance(V__Y1,s__YearFn(V__N1)) & s__instance(V__Y2,s__YearFn(V__N2)) & (V__T1 = s__BeginFn(V__Y1)) & (V__T2 = s__BeginFn(V__Y2)) & s__greaterThan(V__N2,V__N1)) => s__before(V__T1,V__T2))) )
|
Merge.kif 8892-8899 | If X is an instance of the year Y, Z is an instance of the year W, equal V and the beginning of X, equal U and the beginning of Z, and W is greater than Y, then V happens before U |
| ! [V__M1,V__N1,V__Y,V__M2,V__N2,V__T1,V__T2] : (((s__instance(V__M1,s__TimeInterval) & s__instance(V__N1,s__Class) & s__subclass(V__N1,s__Month) & s__instance(V__Y,s__Integer) & s__instance(V__M2,s__TimeInterval) & s__instance(V__N2,s__Class) & s__subclass(V__N2,s__Month) & s__instance(V__T1,s__TimePoint) & s__instance(V__T2,s__TimePoint)) => ((s__instance(V__M1,s__MonthFn(V__N1,s__YearFn(V__Y))) & s__instance(V__M2,s__MonthFn(V__N2,s__YearFn(V__Y))) & (V__T1 = s__BeginFn(V__M1)) & (V__T2 = s__BeginFn(V__M2)) & s__successorClass(V__N1,V__N2)) => s__before(V__T1,V__T2))) )
|
Merge.kif 8908-8915 | If X is an instance of the month Y, Z is an instance of the month W, equal V and the beginning of X, equal U and the beginning of Z, and W is the successor class of Y., then V happens before U |
| ! [V__D1,V__N1,V__M,V__Y,V__D2,V__N2,V__T1,V__T2] : (((s__instance(V__D1,s__TimeInterval) & s__instance(V__N1,s__PositiveInteger) & s__subclass(V__M,s__Month) & s__instance(V__Y,s__Integer) & s__instance(V__D2,s__TimeInterval) & s__instance(V__N2,s__PositiveInteger) & s__instance(V__T1,s__TimePoint) & s__instance(V__T2,s__TimePoint)) => ((s__instance(V__D1,s__DayFn(V__N1,s__MonthFn(V__M,s__YearFn(V__Y)))) & s__instance(V__D2,s__DayFn(V__N2,s__MonthFn(V__M,s__YearFn(V__Y)))) & (V__T1 = s__BeginFn(V__D1)) & (V__T2 = s__BeginFn(V__D2)) & s__greaterThan(V__N2,V__N1)) => s__before(V__T1,V__T2))) )
|
Merge.kif 8924-8931 | If X is an instance of the day Y of month the month Z, W is an instance of the day V of month the month Z, equal U and the beginning of X, equal T and the beginning of W, and V is greater than Y, then U happens before T |
| ! [V__AGENT1 : $i,V__AGENT2 : $i,V__CHANGE : $i,V__OBJ : $i] : (((s__instance(V__CHANGE, s__ChangeOfPossession) & s__patient(V__CHANGE, V__OBJ) & s__holdsDuring(s__BeginFn(s__WhenFn(V__CHANGE)), s__possesses(V__AGENT1, V__OBJ)) & s__holdsDuring(s__EndFn(s__WhenFn(V__CHANGE)), s__possesses(V__AGENT2, V__OBJ))) => ~(V__AGENT1 = V__AGENT2))) | Merge.kif 11923-11930 | If X is an instance of change of possession, Y is a patient of X, Z possesses Y holds during the beginning of the time of existence of X, and W possesses Y holds during the end of the time of existence of X, then equal Z and W |
| ! [V__A : $i,V__O1 : $i,V__O2 : $i] : (((s__instance(V__A, s__Attaching) & s__patient(V__A, V__O1) & s__patient(V__A, V__O2) & s__holdsDuring(s__BeginFn(s__WhenFn(V__A)), ~(s__connected(V__O1, V__O2))) & s__holdsDuring(s__EndFn(s__WhenFn(V__A)), s__connected(V__O1, V__O2))) => (s__objectAttached(V__A, V__O1) & s__objectAttached(V__A, V__O2)))) | Merge.kif 12671-12685 | If X is an instance of attaching, Y is a patient of X, Z is a patient of X, Y is not connected to Z holds during the beginning of the time of existence of X, and Y is connected to Z holds during the end of the time of existence of X, then X attaches Y to another object and X attaches Z to another object |
| ! [V__A : $i,V__D : $i,V__O1 : $i,V__O2 : $i] : (((s__instance(V__D, s__Detaching) & s__patient(V__D, V__O1) & s__patient(V__D, V__O2) & s__holdsDuring(s__BeginFn(s__WhenFn(V__D)), s__connected(V__O1, V__O2)) & s__holdsDuring(s__EndFn(s__WhenFn(V__A)), ~(s__connected(V__O1, V__O2)))) => (s__objectDetached(V__A, V__O1) & s__objectDetached(V__A, V__O2)))) | Merge.kif 12721-12730 | If X is an instance of detaching, Y is a patient of X, Z is a patient of X, Y is connected to Z holds during the beginning of the time of existence of X, and Y is not connected to Z holds during the end of the time of existence of W, then W detaches Y from another object and W detaches Z from another object |
| ! [V__PROCESS,V__PATIENT] : (((s__instance(V__PROCESS,s__Process) & s__instance(V__PATIENT,s__Physical)) => ((s__patient(V__PROCESS,V__PATIENT) & s__time(V__PATIENT,s__EndFn(s__WhenFn(V__PROCESS))) & ~(s__time(V__PATIENT,s__BeginFn(s__WhenFn(V__PROCESS))))) => s__instance(V__PROCESS,s__Creation))) )
|
Merge.kif 13094-13100 | If X is a patient of Y, X exists during the end of the time of existence of Y, and X doesn't exist during the beginning of the time of existence of Y, then Y is an instance of creation |
| ! [V__S1START,V__S2START,V__A,V__S1,V__S2] : (((s__instance(V__S1START,s__TimePoint) & s__instance(V__S2START,s__TimePoint)) => ((s__instance(V__A,s__Ambulating) & s__subProcess(V__S1,V__A) & s__instance(V__S1,s__Stepping) & s__subProcess(V__S2,V__A) & s__instance(V__S2,s__Stepping) & (V__S1START = s__BeginFn(s__WhenFn(V__S1))) & (V__S2START = s__BeginFn(s__WhenFn(V__S2))) & ~((s__before(V__S1START,V__S2START) | s__before(V__S2START,V__S1START)))) => (V__S1 = V__S2))) )
|
Mid-level-ontology.kif 484-497 | If All of the following hold: (1) X is an instance of ambulating (2) Y is a subprocess of X (3) Y is an instance of stepping (4) Z is a subprocess of X (5) Z is an instance of stepping (6) equal W and the beginning of the time of existence of Y (7) equal V and the beginning of the time of existence of Z (8) ~{ W happens before V } and ~{ V happens before W }, then equal Y and Z |
| ! [V__PROC : $i,V__QUANT : $i,V__RES : $i,V__U : $i,V__X : $real,V__Y : $real] : (((s__resourceConsumption(V__PROC, V__QUANT) & s__instance(V__QUANT, s__ConstantQuantity) & s__resource(V__PROC, V__RES) & s__holdsDuring(s__BeginFn(s__WhenFn(V__PROC)), s__measure(V__RES, s__MeasureFn(V__X, V__U))) & s__holdsDuring(s__EndFn(s__WhenFn(V__PROC)), s__measure(V__RES, s__MeasureFn(V__Y, V__U)))) => V__QUANT = s__MeasureFn($difference(V__X ,V__Y), V__U))) | Mid-level-ontology.kif 18901-18917 | If X amount as resource for the Process Y, X is an instance of constant quantity, Z is a resource for Y, the measure of Z is W V(s) holds during the beginning of the time of existence of Y, and the measure of Z is U V(s) holds during the end of the time of existence of Y, then equal X and (W and U) V(s) |
| ! [V__DC : $real,V__DU : $i,V__PROC : $i,V__Q : $real,V__QUANT : $i,V__RES : $i,V__T : $real,V__U : $i,V__X : $real,V__Y : $i] : (((s__resourceConsumption(V__PROC, V__QUANT) & s__instance(V__QUANT, s__FunctionQuantity) & s__resource(V__PROC, V__RES) & V__QUANT = s__PerFn(s__MeasureFn(V__Q, V__U), s__MeasureFn(V__DC, V__DU)) & s__duration(s__WhenFn(V__PROC), s__MeasureFn(V__T, V__DU)) & s__holdsDuring(s__BeginFn(s__WhenFn(V__PROC)), s__measure(V__RES, s__MeasureFn(V__X, V__U))) & s__holdsDuring(s__EndFn(s__WhenFn(V__PROC)), s__measure(V__RES, s__MeasureFn(V__Y, V__U)))) => V__Y = s__MeasureFn($difference(V__X ,$product(V__T ,s__DivisionFn(V__Q, V__DC))), V__U))) | Mid-level-ontology.kif 18957-18983 | If All of the following hold: (1) X amount as resource for the Process Y (2) X is an instance of function quantity (3) Z is a resource for Y (4) equal X and the per of W V(s) and U T(s) (5) duration of the time of existence of Y is S T(s) (6) the measure of Z is R V(s) holds during the beginning of the time of existence of Y (7) the measure of Z is Q V(s) holds during the end of the time of existence of Y, then equal Q and (R and S and W and U) V(s) |
| ! [V__BOTTOM : $i,V__OBJ : $i,V__REVERSE : $i,V__TOP : $i] : (((s__instance(V__REVERSE, s__Reversing) & s__patient(V__REVERSE, V__OBJ) & s__holdsDuring(s__BeginFn(s__WhenFn(V__REVERSE)), (s__top(V__TOP, V__OBJ) & s__bottom(V__BOTTOM, V__OBJ)))) => s__holdsDuring(s__EndFn(s__WhenFn(V__REVERSE)), (s__top(V__BOTTOM, V__OBJ) & s__bottom(V__TOP, V__OBJ))))) | Mid-level-ontology.kif 19437-19442 | If X is an instance of reversing, Y is a patient of X, and the top of Y is Z and the bottom of Y is W holds during the beginning of the time of existence of X, then the top of Y is W and the bottom of Y is Z holds during the end of the time of existence of X |
| ! [V__A : $i,V__ALOC : $i,V__D : $i,V__O : $i,V__P : $i] : (((s__instance(V__P, s__Pushing) & s__origin(V__P, V__O) & s__agent(V__P, V__A) & s__holdsDuring(s__BeginFn(V__P), s__located(V__A, V__ALOC)) & s__destination(V__P, V__D)) => s__holdsDuring(s__ImmediateFutureFn(s__BeginFn(V__P)), ( ? [V__LARGER:$real, V__U:$i, V__SMALLER:$real] : ((s__distance(V__ALOC, V__D, s__MeasureFn(V__SMALLER, V__U)) & s__distance(V__ALOC, V__O, s__MeasureFn(V__LARGER, V__U)) & ($greater(V__LARGER,V__SMALLER)))))))) | Mid-level-ontology.kif 19536-19554 | If X is an instance of pushing, X originates at Y, Z is an agent of X, Z is located at W holds during the beginning of X, and X ends up at V, then there exist U, T and S such that the distance between W and V is S T(s) and the distance between W and Y is U T(s) and U is greater than S holds during immediately after the beginning of X |
| ! [V__A : $i,V__ALOC : $i,V__D : $i,V__O : $i,V__P : $i] : (((s__instance(V__P, s__Pulling) & s__origin(V__P, V__O) & s__agent(V__P, V__A) & s__holdsDuring(s__BeginFn(V__P), s__located(V__A, V__ALOC)) & s__destination(V__P, V__D)) => s__holdsDuring(s__ImmediateFutureFn(s__BeginFn(V__P)), ( ? [V__LARGER:$real, V__U:$i, V__SMALLER:$real] : ((s__distance(V__ALOC, V__D, s__MeasureFn(V__SMALLER, V__U)) & s__distance(V__ALOC, V__O, s__MeasureFn(V__LARGER, V__U)) & ($greater(V__LARGER,V__SMALLER)))))))) | Mid-level-ontology.kif 19558-19576 | If X is an instance of pulling, X originates at Y, Z is an agent of X, Z is located at W holds during the beginning of X, and X ends up at V, then there exist U, T and S such that the distance between W and V is S T(s) and the distance between W and Y is U T(s) and U is greater than S holds during immediately after the beginning of X |
| ! [V__L : $int,V__R : $i,V__S : $i] : (((s__instance(V__R, s__ChemicalReduction) & s__patient(V__R, V__S) & s__holdsDuring(s__BeginFn(s__WhenFn(V__R)), s__electronNumber(V__S, V__L))) => ( ? [V__G:$int] : ((($greater(V__G,V__L)) & s__holdsDuring(s__EndFn(s__WhenFn(V__R)), s__electronNumber(V__S, V__G))))))) | Mid-level-ontology.kif 21465-21477 | If X is an instance of chemical reduction, Y is a patient of X, and Z is an electron number of Y holds during the beginning of the time of existence of X, then there exists W such that W is greater than Z and W is an electron number of Y holds during the end of the time of existence of X |
| ! [V__G : $int,V__O : $i,V__S : $i] : (((s__instance(V__O, s__Oxidation) & s__patient(V__O, V__S) & s__holdsDuring(s__BeginFn(s__WhenFn(V__O)), s__electronNumber(V__S, V__G))) => ( ? [V__L:$int] : ((($less(V__L,V__G)) & s__holdsDuring(s__EndFn(s__WhenFn(V__O)), s__electronNumber(V__S, V__L))))))) | Mid-level-ontology.kif 21483-21495 | If X is an instance of oxidating, Y is a patient of X, and Z is an electron number of Y holds during the beginning of the time of existence of X, then there exists W such that W is less than Z and W is an electron number of Y holds during the end of the time of existence of X |
| Display limited to 25 items. Show next 25 | ||
| Display limited to 25 items. Show next 25 |
| consequent |
|
|
| ! [V__SIT1 : $i,V__SIT2 : $i,V__T1 : $i,V__T2 : $i] : (((s__holdsDuring(V__T2, V__SIT2) & s__holdsDuring(V__T1, V__SIT1) & s__instance(V__T1, s__TimeInterval) & s__instance(V__T2, s__TimeInterval) & s__causesProposition(V__SIT1, V__SIT2)) => s__beforeOrEqual(s__BeginFn(V__T1), s__BeginFn(V__T2)))) | Merge.kif 3940-3947 | If X holds during Y, Z holds during W, W is an instance of timeframe, Y is an instance of timeframe, and X is a causes proposition of Z, then the beginning of W happens before or at the beginning of Y |
| ! [V__DURATION : $i,V__OBJ : $i,V__TIME : $i] : (((s__instance(V__TIME, s__TimePoint) & s__holdsDuring(V__TIME, s__age(V__OBJ, V__DURATION))) => s__duration(s__TimeIntervalFn(s__BeginFn(s__WhenFn(V__OBJ)), V__TIME), V__DURATION))) | Merge.kif 7662-7666 | If X is an instance of time point and the age of Y is Z holds during X, then duration of interval between the beginning of the time of existence of Y and X is Z |
| ! [V__PROCESS,V__OBJ] : (((s__instance(V__PROCESS,s__Process) & s__instance(V__OBJ,s__Object)) => (s__origin(V__PROCESS,V__OBJ) => s__eventLocated(s__WhereFn(V__PROCESS,s__BeginFn(s__WhenFn(V__PROCESS))) ,s__WhereFn(V__OBJ,s__BeginFn(s__WhenFn(V__OBJ)))))) )
|
Merge.kif 8162-8170 | If X originates at Y, then the place where X was at the beginning of the time of existence of X is located at the place where Y was at the beginning of the time of existence of Y |
| ! [V__INTERVAL1,V__INTERVAL2] : (((s__instance(V__INTERVAL1,s__TimeInterval) & s__instance(V__INTERVAL2,s__TimeInterval)) => (s__starts(V__INTERVAL1,V__INTERVAL2) => ((s__BeginFn(V__INTERVAL1) = s__BeginFn(V__INTERVAL2)) & s__before(s__EndFn(V__INTERVAL1) ,s__EndFn(V__INTERVAL2))))) )
|
Merge.kif 8218-8226 | If X starts Y, then equal the beginning of X and the beginning of Y and the end of X happens before the end of Y |
| ! [V__INTERVAL1,V__INTERVAL2] : (((s__instance(V__INTERVAL1,s__TimeInterval) & s__instance(V__INTERVAL2,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))))) )
|
Merge.kif 8250-8258 | If X finishes Y, then the beginning of Y happens before the beginning of X and equal the end of Y and the end of X |
| ! [V__INTERVAL1,V__INTERVAL2] : (((s__instance(V__INTERVAL1,s__TimeInterval) & s__instance(V__INTERVAL2,s__TimeInterval)) => (s__finishesDuring(V__INTERVAL1,V__INTERVAL2) => s__temporallyBetween(s__BeginFn(V__INTERVAL2) ,s__EndFn(V__INTERVAL1) ,s__EndFn(V__INTERVAL2)))) )
|
Merge.kif 8279-8281 | If finishes during X and Y, then the end of X is between the beginning of Y and the end of Y |
| ! [V__INTERVAL1,V__INTERVAL2] : (((s__instance(V__INTERVAL1,s__TimeInterval) & s__instance(V__INTERVAL2,s__TimeInterval)) => (s__startsDuring(V__INTERVAL1,V__INTERVAL2) => s__temporallyBetween(s__BeginFn(V__INTERVAL2) ,s__BeginFn(V__INTERVAL1) ,s__EndFn(V__INTERVAL2)))) )
|
Merge.kif 8292-8294 | If starts during X and Y, then the beginning of X is between the beginning of Y and the end of Y |
| ! [V__PROC,V__OBJ] : (((s__instance(V__PROC,s__Process) & s__instance(V__OBJ,s__Physical)) => (s__result(V__PROC,V__OBJ) => (! [V__TIME] : ((s__instance(V__TIME,s__TimePoint) => (s__before(V__TIME,s__BeginFn(s__WhenFn(V__PROC))) => ~(s__time(V__OBJ,V__TIME)))))))) )
|
Merge.kif 8326-8332 | If X is a result of Y, then For all TimePoint Z: if Z happens before the beginning of the time of existence of Y, then X doesn't exist during Z |
| ! [V__INTERVAL] : ((s__instance(V__INTERVAL,s__TimeInterval) => s__before(s__BeginFn(V__INTERVAL) ,s__EndFn(V__INTERVAL))) )
|
Merge.kif 8334-8336 | If X is an instance of timeframe, then the beginning of X happens before the end of X |
| ! [V__PHYS,V__TIME] : ((s__instance(V__PHYS,s__Physical) => ((s__time(V__PHYS,V__TIME) & s__instance(V__TIME,s__TimePoint)) => s__temporallyBetweenOrEqual(s__BeginFn(s__WhenFn(V__PHYS)) ,V__TIME,s__EndFn(s__WhenFn(V__PHYS))))) )
|
Merge.kif 8408-8412 | If X exists during Y and Y is an instance of time point, then Y is between or at the beginning of the time of existence of X and the end of the time of existence of X |
| ! [V__INTERVAL1,V__INTERVAL2] : (((s__instance(V__INTERVAL1,s__TimeInterval) & s__instance(V__INTERVAL2,s__TimeInterval)) => (s__during(V__INTERVAL1,V__INTERVAL2) => (s__before(s__EndFn(V__INTERVAL1) ,s__EndFn(V__INTERVAL2)) & s__before(s__BeginFn(V__INTERVAL2) ,s__BeginFn(V__INTERVAL1))))) )
|
Merge.kif 8517-8521 | If X takes place during Y, then the end of X happens before the end of Y and the beginning of Y happens before the beginning of X |
| ! [V__INTERVAL1,V__INTERVAL2] : (((s__instance(V__INTERVAL1,s__TimeInterval) & s__instance(V__INTERVAL2,s__TimeInterval)) => (s__meetsTemporally(V__INTERVAL1,V__INTERVAL2) => (s__EndFn(V__INTERVAL1) = s__BeginFn(V__INTERVAL2)))) )
|
Merge.kif 8535-8539 | If X meets Y, then equal the end of X and the beginning of Y |
| ! [V__INTERVAL1,V__INTERVAL2] : (((s__instance(V__INTERVAL1,s__TimeInterval) & s__instance(V__INTERVAL2,s__TimeInterval)) => (s__earlier(V__INTERVAL1,V__INTERVAL2) => s__before(s__EndFn(V__INTERVAL1) ,s__BeginFn(V__INTERVAL2)))) )
|
Merge.kif 8580-8582 | If X happens earlier than Y, then the end of X happens before the beginning of Y |
| ! [V__POINT1,V__POINT2,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)) => ((s__BeginFn(V__INTERVAL) = V__POINT1) & (s__EndFn(V__INTERVAL) = V__POINT2))) )
|
Merge.kif 8622-8630 | If X is an instance of time point, Y is an instance of time point, Z is an instance of timeframe, and equal interval between X, Y, and Z, then equal the beginning of Z and X and equal the end of Z and Y |
| ! [V__INTERVAL] : ((s__instance(V__INTERVAL,s__TimeInterval) => (s__PastFn(V__INTERVAL) = s__TimeIntervalFn(s__NegativeInfinity,s__BeginFn(V__INTERVAL)))) )
|
Merge.kif 8692-8694 | If X is an instance of timeframe, then equal before X, interval between negative infinity, and the beginning of X |
| ! [V__A] : ((s__instance(V__A,s__Afternoon) => (? [V__N] : ((s__instance(V__N,s__Noon) & (s__BeginFn(V__A) = V__N))))) )
|
Merge.kif 9049-9054 | If X is an instance of afternoon, then there exists Y such that Y is an instance of noon, equal the beginning of X, and Y |
| ! [V__JOIN : $i,V__ORG : $i,V__PERSON : $i] : (((s__instance(V__JOIN, s__JoiningAnOrganization) & s__instance(V__ORG, s__Organization) & s__agent(V__JOIN, V__PERSON) & s__patient(V__JOIN, V__ORG)) => (s__holdsDuring(s__BeginFn(s__WhenFn(V__JOIN)), ~(s__member(V__PERSON, V__ORG))) & s__holdsDuring(s__EndFn(s__WhenFn(V__JOIN)), s__member(V__PERSON, V__ORG))))) | Merge.kif 10824-10832 | If X is an instance of joining an organization, Y is an instance of organization, Z is an agent of X, and Y is a patient of X, then Z is not a member of Y holds during the beginning of the time of existence of X and Z is a member of Y holds during the end of the time of existence of X |
| ! [V__JOIN : $i,V__ORG : $i,V__PERSON : $i] : (((s__instance(V__JOIN, s__Hiring) & s__instance(V__ORG, s__Organization) & s__agent(V__JOIN, V__ORG) & s__patient(V__JOIN, V__PERSON)) => (s__holdsDuring(s__BeginFn(s__WhenFn(V__JOIN)), ~(s__member(V__PERSON, V__ORG))) & s__holdsDuring(s__EndFn(s__WhenFn(V__JOIN)), s__member(V__PERSON, V__ORG))))) | Merge.kif 10857-10865 | If X is an instance of hiring, Y is an instance of organization, Y is an agent of X, and Z is a patient of X, then Z is not a member of Y holds during the beginning of the time of existence of X and Z is a member of Y holds during the end of the time of existence of X |
| ! [V__LEAVE : $i,V__ORG : $i,V__PERSON : $i] : (((s__instance(V__LEAVE, s__LeavingAnOrganization) & s__instance(V__ORG, s__Organization) & s__agent(V__LEAVE, V__PERSON) & s__patient(V__LEAVE, V__ORG)) => (s__holdsDuring(s__BeginFn(s__WhenFn(V__LEAVE)), s__member(V__PERSON, V__ORG)) & s__holdsDuring(s__EndFn(s__WhenFn(V__LEAVE)), ~(s__member(V__PERSON, V__ORG)))))) | Merge.kif 10898-10906 | If X is an instance of leaving an organization, Y is an instance of organization, Z is an agent of X, and Y is a patient of X, then Z is a member of Y holds during the beginning of the time of existence of X and Z is not a member of Y holds during the end of the time of existence of X |
| ! [V__LEAVE : $i,V__ORG : $i,V__P : $i] : (((s__instance(V__LEAVE, s__Firing) & s__instance(V__ORG, s__Organization) & s__agent(V__LEAVE, V__ORG) & s__patient(V__LEAVE, V__P)) => (s__holdsDuring(s__BeginFn(s__WhenFn(V__LEAVE)), s__member(V__P, V__ORG)) & s__holdsDuring(s__EndFn(s__WhenFn(V__LEAVE)), ~(s__member(V__P, V__ORG)))))) | Merge.kif 10930-10938 | If X is an instance of firing, Y is an instance of organization, Y is an agent of X, and Z is a patient of X, then Z is a member of Y holds during the beginning of the time of existence of X and Z is not a member of Y holds during the end of the time of existence of X |
| ! [V__HIRE : $i,V__ORG : $i,V__PERSON : $i] : (((s__instance(V__HIRE, s__Hiring) & s__instance(V__ORG, s__Organization) & s__agent(V__HIRE, V__ORG) & s__patient(V__HIRE, V__PERSON)) => (s__holdsDuring(s__BeginFn(s__WhenFn(V__HIRE)), ~(s__employs(V__ORG, V__PERSON))) & s__holdsDuring(s__EndFn(s__WhenFn(V__HIRE)), s__employs(V__ORG, V__PERSON))))) | Merge.kif 10971-10979 | If X is an instance of hiring, Y is an instance of organization, Y is an agent of X, and Z is a patient of X, then Y doesn't employ Z holds during the beginning of the time of existence of X and Y employs Z holds during the end of the time of existence of X |
| ! [V__FIRE : $i,V__ORG : $i,V__PERSON : $i] : (((s__instance(V__FIRE, s__TerminatingEmployment) & s__instance(V__ORG, s__Organization) & s__agent(V__FIRE, V__ORG) & s__patient(V__FIRE, V__PERSON)) => (s__holdsDuring(s__BeginFn(s__WhenFn(V__FIRE)), s__employs(V__ORG, V__PERSON)) & s__holdsDuring(s__EndFn(s__WhenFn(V__FIRE)), ~(s__employs(V__ORG, V__PERSON)))))) | Merge.kif 10987-10995 | If X is an instance of terminating employment, Y is an instance of organization, Y is an agent of X, and Z is a patient of X, then Y employs Z holds during the beginning of the time of existence of X and Y doesn't employ Z holds during the end of the time of existence of X |
| ! [V__HEAT : $i,V__OBJ : $real] : (((s__instance(V__HEAT, s__Heating) & s__patient(V__HEAT, V__OBJ)) => ( ? [V__UNIT:$i, V__QUANT1:$real, V__QUANT2:$real] : ((s__instance(V__UNIT, s__TemperatureMeasure) & s__holdsDuring(s__BeginFn(s__WhenFn(V__HEAT)), s__MeasureFn(V__OBJ, V__UNIT) = V__QUANT1) & s__holdsDuring(s__EndFn(s__WhenFn(V__HEAT)), s__MeasureFn(V__OBJ, V__UNIT) = V__QUANT2) & ($greater(V__QUANT2,V__QUANT1))))))) | Merge.kif 11172-11185 | If X is an instance of heating and Y is a patient of X, then there exist Z, W and V such that Z is an instance of temperature measure and equal Y Z(s) and W holds during the beginning of the time of existence of X and equal Y Z(s) and V holds during the end of the time of existence of X and V is greater than W |
| ! [V__COOL : $i,V__OBJ : $real] : (((s__instance(V__COOL, s__Cooling) & s__patient(V__COOL, V__OBJ)) => ( ? [V__UNIT:$i, V__QUANT1:$real, V__QUANT2:$real] : ((s__instance(V__UNIT, s__TemperatureMeasure) & s__holdsDuring(s__BeginFn(s__WhenFn(V__COOL)), s__MeasureFn(V__OBJ, V__UNIT) = V__QUANT1) & s__holdsDuring(s__EndFn(s__WhenFn(V__COOL)), s__MeasureFn(V__OBJ, V__UNIT) = V__QUANT2) & ($less(V__QUANT2,V__QUANT1))))))) | Merge.kif 11213-11226 | If X is an instance of cooling and Y is a patient of X, then there exist Z, W and V such that Z is an instance of temperature measure and equal Y Z(s) and W holds during the beginning of the time of existence of X and equal Y Z(s) and V holds during the end of the time of existence of X and V is less than W |
| ! [V__MOTION : $i,V__OBJ : $i,V__PLACE : $i] : (((s__instance(V__MOTION, s__Motion) & s__moves(V__MOTION, V__OBJ) & s__origin(V__MOTION, V__PLACE)) => s__holdsDuring(s__BeginFn(s__WhenFn(V__MOTION)), s__located(V__OBJ, V__PLACE)))) | Merge.kif 11288-11293 | If X is an instance of motion, Y moves during X, and X originates at Z, then Y is located at Z holds during the beginning of the time of existence of X |
| Display limited to 25 items. Show next 25 | ||
| Display limited to 25 items. Show next 25 |
|