Browsing Interface : Welcome guest : log in
|
Browsing Interface : Welcome guest : log in |
[
Home |
Graph |
LogLearn |
Editor |
]
KB:
Language:
Formal Language:
|
| TimeInterval(timeframe) |  | 1920s, 1930s, 1940s, 1950s, 1960s, 1970s, 1980s, 1990s, 24/7, Ab, Adar, Adar_Sheni, Aegean_civilisation, Aegean_civilization, Aegean_culture, Aghan, Allhallowtide, Asadha, Asarh, Asin, Asvina, Augustan, Av, Baisakh, Bhadon, Bhadrapada, Bronze_Age, Caitra, Caliphate, Chait, Chislev, Christian_era, Christmas, Christmastide, Christmastime, Common_era, Cretaceous, Cyclades, Cycladic_civilisation, Cycladic_civilization, Cycladic_culture, Dark_Ages, Depression, Dhu'l-Hijja, Dhu'l-Hijjah, Dhu'l-Qa'dah, Dhu_al-Hijja, Dhu_al-Hijjah, Dhu_al-Qadah, ERA... |
| appearance as argument number 1 |
|
|
| s__subclass(s__TimeInterval,s__TimePosition)
|
Merge.kif 2194-2194 | Timeframe is a subclass of time position |
| s__documentation(s__TimeInterval, s__EnglishLanguage, "An interval of time_ Note that a TimeInterval has both an extent and a location on the universal timeline_ Note too that a TimeInterval has no gaps, i_e_ this class contains only convex time intervals_") | Merge.kif 2196-2199 | Timeframe is a subclass of time position |
| appearance as argument number 2 |
|
|
| appearance as argument number 3 |
|
|
| antecedent |
|
|
| ! [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__INTERVAL] : ((s__instance(V__INTERVAL,s__TimeInterval) => (? [V__POINT] : ((s__instance(V__POINT,s__TimePoint) & s__temporalPart(V__POINT,V__INTERVAL))))) )
|
Merge.kif 8121-8126 | If X is an instance of timeframe, then there exists Y such that Y is an instance of time point and Y is a part of X |
| ! [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__INTERVAL1,V__INTERVAL2,V__INTERVAL3] : (((s__instance(V__INTERVAL1,s__TimeInterval) & s__instance(V__INTERVAL2,s__TimeInterval)) => ((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 8444-8449 | If X is an instance of timeframe, X is a part of Y, and X is a part of Z, then Z overlaps Y |
| ! [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__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__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__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)) => (! [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 8632-8641 | 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 For all TimePoint W: W is between or at X, Y if, and only if W is a part of Z |
| ! [V__INTERVAL] : ((s__instance(V__INTERVAL,s__TimeInterval) => s__meetsTemporally(s__PastFn(V__INTERVAL) ,V__INTERVAL)) )
|
Merge.kif 8688-8690 | If X is an instance of timeframe, then before X meets X |
| ! [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__INTERVAL] : ((s__instance(V__INTERVAL,s__TimeInterval) => s__finishes(s__ImmediatePastFn(V__INTERVAL) ,s__PastFn(V__INTERVAL))) )
|
Merge.kif 8706-8708 | If X is an instance of timeframe, then immediately before X finishes before X |
| ! [V__INTERVAL] : ((s__instance(V__INTERVAL,s__TimeInterval) => s__meetsTemporally(V__INTERVAL,s__FutureFn(V__INTERVAL))) )
|
Merge.kif 8719-8721 | If X is an instance of timeframe, then X meets after X |
| ! [V__INTERVAL] : ((s__instance(V__INTERVAL,s__TimeInterval) => (s__FutureFn(V__INTERVAL) = s__TimeIntervalFn(s__EndFn(V__INTERVAL) ,s__PositiveInfinity))) )
|
Merge.kif 8723-8725 | If X is an instance of timeframe, then equal after X, interval between the end of X, and positive infinity |
| ! [V__INTERVAL] : ((s__instance(V__INTERVAL,s__TimeInterval) => s__starts(s__ImmediateFutureFn(V__INTERVAL) ,s__FutureFn(V__INTERVAL))) )
|
Merge.kif 8737-8739 | If X is an instance of timeframe, then immediately after X starts after X |
| ! [V__P1 : $i,V__P2 : $i,V__T1 : $i] : (((s__holdsDuring(V__T1, s__spouse(V__P1, V__P2)) & s__instance(V__T1, s__TimeInterval)) => ( ? [V__WED:$i] : ((s__instance(V__WED, s__Wedding) & s__patient(V__WED, V__P1) & s__patient(V__WED, V__P2) & s__earlier(s__WhenFn(V__WED), V__T1)))))) | Mid-level-ontology.kif 9293-9303 | If X is the spouse of Y holds during Z and Z is an instance of timeframe, then there exists W such that W is an instance of wedding, X is a patient of W, Y is a patient of W, and the time of existence of W happens earlier than Z |
| ! [V__IMPRISON,V__AGENT,V__INTERVAL] : (((s__instance(V__IMPRISON,s__Imprisoning) & s__detainee(V__IMPRISON,V__AGENT) & s__instance(V__AGENT,s__Human) & s__time(V__IMPRISON,V__INTERVAL) & s__instance(V__INTERVAL,s__TimeInterval)) => (? [V__ARREST,V__TIME] : ((s__instance(V__TIME,s__TimeInterval) & s__time(V__ARREST,V__TIME) & s__earlier(V__TIME,V__INTERVAL) & s__instance(V__ARREST,s__PlacingUnderArrest) & s__arrested(V__ARREST,V__AGENT))))) )
|
Mid-level-ontology.kif 25831-25844 | If X is an instance of imprisoning, Y is a detainee of X, Y is an instance of human, X exists during Z, and Z is an instance of timeframe, then there exist W, V such that V is an instance of timeframe, W exists during V, V happens earlier than Z, W is an instance of placing under arrest, and Y is placed under arrest during W |
| ! [V__AGENT,V__CATALOG,V__TIMEINT,V__CLASS,V__TIME] : (((s__instance(V__AGENT,s__AutonomousAgent) & s__instance(V__CATALOG,s__Catalog) & s__instance(V__TIMEINT,s__TimeInterval) & s__instance(V__CLASS,s__Class) & s__subclass(V__CLASS,s__Process) & s__instance(V__TIME,s__Class) & s__subclass(V__TIME,s__TimeInterval)) => ((s__offersAtTime(V__AGENT,V__CATALOG,V__TIMEINT) & s__catalogItem(V__CLASS,V__CATALOG) & s__subclass(V__CLASS,s__Process) & s__instance(V__TIMEINT,V__TIME) & s__subclass(V__TIME,s__TimeInterval)) => s__capabilityDuring(V__CLASS,s__agent,V__AGENT,V__TIME))) )
|
Catalog.kif 130-137 | If X offers items for sale in Y during Z, W is in Y, W is a subclass of process, Z is an instance of V, and V is a subclass of timeframe, then X is capable of being a agent in W during V |
| ! [V__AGENT,V__CATALOG,V__TIMEINT,V__CLASS,V__PROCESSINSTANCE,V__PROCESS,V__TIME,V__OBJ] : (((s__instance(V__AGENT,s__AutonomousAgent) & s__instance(V__CATALOG,s__Catalog) & s__instance(V__TIMEINT,s__TimeInterval) & s__instance(V__CLASS,s__Class) & s__instance(V__PROCESSINSTANCE,s__Process) & s__instance(V__PROCESS,s__Class) & s__subclass(V__PROCESS,s__Process) & s__instance(V__TIME,s__Class) & s__subclass(V__TIME,s__TimeInterval)) => ((s__offersAtTime(V__AGENT,V__CATALOG,V__TIMEINT) & s__catalogItem(V__CLASS,V__CATALOG) & s__subclass(V__CLASS,s__Object) & s__instance(V__PROCESSINSTANCE,V__PROCESS) & s__subclass(V__PROCESS,s__Process) & s__instance(V__OBJ,V__CLASS) & s__patient(V__PROCESSINSTANCE,V__OBJ) & s__instance(V__TIMEINT,V__TIME) & s__subclass(V__TIME,s__TimeInterval)) => s__capabilityDuring(V__PROCESS,s__agent,V__AGENT,V__TIME))) )
|
Catalog.kif 139-150 | If All of the following hold: (1) X offers items for sale in Y during Z (2) W is in Y (3) W is a subclass of object (4) V is an instance of U (5) U is a subclass of process (6) T is an instance of W (7) T is a patient of V (8) Z is an instance of S (9) S is a subclass of timeframe, then X is capable of being a agent in U during S |
| ! [V__AREA : $i,V__YEAR : $i] : (((s__instance(V__YEAR, s__TimeInterval) & s__holdsDuring(V__YEAR, s__economyType(V__AREA, s__LowIncomeCountry))) => ( ? [V__AMOUNT:$real] : ((s__perCapitaGDPInPeriod(V__AREA, s__MeasureFn(V__AMOUNT, s__UnitedStatesDollar), V__YEAR) & ($less(V__AMOUNT,756.0))))))) | Economy.kif 440-447 | If X is an instance of timeframe and low income country is an economy type of Y holds during X, then there exists Z such that Y is per capitaGDP in period Z united states dollar(s) for X and Z is less than 756.0 |
| ! [V__AREA : $i,V__YEAR : $i] : (((s__instance(V__YEAR, s__TimeInterval) & s__holdsDuring(V__YEAR, s__economyType(V__AREA, s__LowerMiddleIncomeCountry))) => ( ? [V__AMOUNT:$real] : ((s__perCapitaGDPInPeriod(V__AREA, s__MeasureFn(V__AMOUNT, s__UnitedStatesDollar), V__YEAR) & ($greatereq(V__AMOUNT,756.0))))))) | Economy.kif 456-463 | If X is an instance of timeframe and lower middle income country is an economy type of Y holds during X, then there exists Z such that Y is per capitaGDP in period Z united states dollar(s) for X and Z is greater than or equal to 756.0 |
| ! [V__AREA : $i,V__YEAR : $i] : (((s__instance(V__YEAR, s__TimeInterval) & s__holdsDuring(V__YEAR, s__economyType(V__AREA, s__LowerMiddleIncomeCountry))) => ( ? [V__AMOUNT:$real] : ((s__perCapitaGDPInPeriod(V__AREA, s__MeasureFn(V__AMOUNT, s__UnitedStatesDollar), V__YEAR) & ($less(V__AMOUNT,2996.0))))))) | Economy.kif 465-472 | If X is an instance of timeframe and lower middle income country is an economy type of Y holds during X, then there exists Z such that Y is per capitaGDP in period Z united states dollar(s) for X and Z is less than 2996.0 |
| ! [V__AREA : $i,V__YEAR : $i] : (((s__instance(V__YEAR, s__TimeInterval) & s__holdsDuring(V__YEAR, s__economyType(V__AREA, s__UpperMiddleIncomeCountry))) => ( ? [V__AMOUNT:$real] : ((s__perCapitaGDPInPeriod(V__AREA, s__MeasureFn(V__AMOUNT, s__UnitedStatesDollar), V__YEAR) & ($greatereq(V__AMOUNT,2996.0))))))) | Economy.kif 481-488 | If X is an instance of timeframe and upper middle income country is an economy type of Y holds during X, then there exists Z such that Y is per capitaGDP in period Z united states dollar(s) for X and Z is greater than or equal to 2996.0 |
| ! [V__AREA : $i,V__YEAR : $i] : (((s__instance(V__YEAR, s__TimeInterval) & s__holdsDuring(V__YEAR, s__economyType(V__AREA, s__UpperMiddleIncomeCountry))) => ( ? [V__AMOUNT:$real] : ((s__perCapitaGDPInPeriod(V__AREA, s__MeasureFn(V__AMOUNT, s__UnitedStatesDollar), V__YEAR) & ($less(V__AMOUNT,9267.0))))))) | Economy.kif 490-497 | If X is an instance of timeframe and upper middle income country is an economy type of Y holds during X, then there exists Z such that Y is per capitaGDP in period Z united states dollar(s) for X and Z is less than 9267.0 |
| ! [V__Agent : $i,V__ExpDate : $i,V__Option : $i,V__Price : $i,V__Stocks : $i,V__Time : $i] : (((s__instance(V__Option, s__CallOption) & s__optionHolder(V__Option, V__Agent) & s__strikePrice(V__Option, V__Price) & s__agreementExpirationDate(V__Option, V__ExpDate) & s__underlier(V__Option, V__Stocks) & s__price(V__Stocks, V__Price, V__Time) & s__instance(V__Time, s__TimeInterval) & s__before(s__EndFn(V__Time), s__BeginFn(V__ExpDate))) => s__holdsRight(V__Agent, ( ? [V__Buy:$i] : ((s__instance(V__Buy, s__Buying) & s__patient(V__Buy, V__Stocks) & s__time(V__Buy, V__Time) & s__measure(V__Stocks, s__MeasureFn(100, s__ShareUnit)) & s__agent(V__Buy, V__Agent))))))) | FinancialOntology.kif 2652-2670 | If All of the following hold: (1) X is an instance of call option (2) Y holds X (3) Z is a strike price of X (4) X has expiration W (5) V is an underlier of X (6) V is price Z for U (7) U is an instance of timeframe (8) the end of U happens before the beginning of W, then Y has the right to perform %3 |
| Display limited to 25 items. Show next 25 | ||
| Display limited to 25 items. Show next 25 |
| consequent |
|
|
| ! [V__POINT] : ((s__instance(V__POINT,s__TimePoint) => (? [V__INTERVAL] : ((s__instance(V__INTERVAL,s__TimeInterval) & s__temporalPart(V__POINT,V__INTERVAL))))) )
|
Merge.kif 8114-8119 | If X is an instance of time point, then there exists Y such that Y is an instance of timeframe and X is a part of Y |
| ! [V__INTERVAL1,V__INTERVAL2] : (((s__instance(V__INTERVAL1,s__TimeInterval) & s__instance(V__INTERVAL2,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)))))) )
|
Merge.kif 8436-8442 | If X overlaps Y, then there exists Z such that Z is an instance of timeframe, Z is a part of Y, and Z is a part of X |
| ! [V__T1,V__T2] : (((s__instance(V__T1,s__TimeInterval) & s__instance(V__T2,s__TimeInterval)) => (s__meetsTemporally(V__T1,V__T2) => ~((? [V__T3] : ((s__instance(V__T3,s__TimeInterval) & s__temporalPart(V__T3,V__T1) & s__temporalPart(V__T3,V__T2))))))) )
|
Merge.kif 8547-8554 | If X meets Y, then there doesn't exist Z such that Z is an instance of timeframe, Z is a part of X, and Z is a part of Y |
| ! [V__OBJ : $i,V__ORGANISM : $i,V__T1 : $i] : ((s__holdsDuring(V__T1, s__inhabits(V__ORGANISM, V__OBJ)) => ( ? [V__TIME:$i] : ((s__instance(V__TIME, s__TimeInterval) & s__temporalPart(V__TIME, V__T1) & s__holdsDuring(V__TIME, s__located(V__ORGANISM, V__OBJ))))))) | Merge.kif 14688-14694 | If X lives in Y holds during Z, then there exists W such that W is an instance of timeframe, W is a part of Z, and X is located at Y holds during W |
| ! [V__L,V__FL] : ((s__instance(V__L,s__Object) => ((s__instance(V__FL,s__FlashingLight) & s__origin(V__FL,V__L)) => (? [V__I1,V__T2,V__I3] : ((s__instance(V__I1,s__RadiatingLight) & s__instance(V__T2,s__TimeInterval) & s__instance(V__I3,s__RadiatingLight) & s__meetsTemporally(s__WhenFn(V__I1) ,V__T2) & s__meetsTemporally(V__T2,s__WhenFn(V__I3)) & ~((? [V__I2] : ((s__instance(V__I2,s__RadiatingLight) & s__origin(V__I2,V__L) & s__during(s__WhenFn(V__I2) ,V__T2))))) & s__subProcess(V__I1,V__FL) & s__subProcess(V__I3,V__FL)))))) )
|
Mid-level-ontology.kif 626-644 | If X is an instance of flashing light and X originates at Y, then All of the following hold: (1) there exist Z, W (2) V such that Z is an instance of radiating light (3) W is an instance of timeframe (4) V is an instance of radiating light (5) the time of existence of Z meets W (6) W meets the time of existence of V (7) there doesn't exist U such that U is an instance of radiating light (8) U originates at Y (9) the time of existence of U takes place during W (10) Z is a subprocess of X (11) V is a subprocess of X |
| ! [V__D : $i] : ((s__instance(V__D, s__Disappearing) => ( ? [V__OBJ:$i, V__AGENT:$i, V__SEARCH:$i, V__TIME:$i] : ((s__instance(V__SEARCH, s__Searching) & s__earlier(s__WhenFn(V__D), s__WhenFn(V__SEARCH)) & s__agent(V__SEARCH, V__AGENT) & s__instance(V__OBJ, s__Object) & s__patient(V__D, V__OBJ) & s__patient(V__SEARCH, V__OBJ) & s__instance(V__TIME, s__TimeInterval) & s__temporalPart(V__TIME, s__WhenFn(V__SEARCH)) & s__holdsDuring(V__TIME, ~(s__modalAttribute(( ? [V__DISC:$i] : ((s__instance(V__DISC, s__Discovering) & s__agent(V__DISC, V__AGENT) & s__patient(V__DISC, V__OBJ)))), s__Possibility)))))))) | Mid-level-ontology.kif 19162-19184 | If X is an instance of disappearing, then All of the following hold: (1) there exist Y, Z,, , W (2) V such that W is an instance of searching (3) the time of existence of X happens earlier than the time of existence of W (4) Z is an agent of W (5) Y is an instance of object (6) Y is a patient of X (7) Y is a patient of W (8) V is an instance of timeframe (9) V is a part of the time of existence of W (10) the statement there doesn't exist U such that U is an instance of discovering (11) Z is an agent of U (12) Y is a patient of U doesn't have the modal force of possibility holds during V |
| ! [V__CUT : $i,V__OBJ : $i,V__SAW : $i] : (((s__instance(V__SAW, s__Saw) & s__instance(V__CUT, s__Cutting) & s__instrument(V__CUT, V__SAW) & s__instance(V__OBJ, s__Object) & s__patient(V__CUT, V__OBJ)) => ( ? [V__MOTION:$i, V__DIR1:$i, V__DIR2:$i, V__TIME:$i, V__T1:$i, V__T2:$i, V__PART:$i] : ((s__instance(V__MOTION, s__Motion) & s__subProcess(V__MOTION, V__CUT) & s__instance(V__PART, s__CuttingDevice) & s__part(V__PART, V__SAW) & s__meetsSpatially(V__PART, V__OBJ) & s__patient(V__MOTION, V__PART) & s__instance(V__T2, s__TimeInterval) & s__instance(V__T2, s__TimeInterval) & s__WhenFn(V__MOTION) = V__TIME & s__temporalPart(V__TIME, V__T1) & s__temporalPart(V__TIME, V__T2) & s__instance(V__DIR1, s__DirectionalAttribute) & s__instance(V__DIR2, s__DirectionalAttribute) & (s__holdsDuring(V__T1, s__direction(V__MOTION, V__DIR1)) => s__holdsDuring(V__T2, (s__direction(V__MOTION, V__DIR2) & (V__DIR1 = V__DIR2 | s__oppositeDirection(V__DIR1, V__DIR2)) & ~((V__DIR1 = V__DIR2 & s__oppositeDirection(V__DIR1, V__DIR2))))))))))) | Mid-level-ontology.kif 20084-20118 | If X is an instance of saw, Y is an instance of cutting, X is an instrument for Y, Z is an instance of object, and Z is a patient of Y, then there exist W, V,, , U,, , T,, , S,, , R and Q such that W is an instance of motion and W is a subprocess of Y and Q is an instance of cutting device and Q is a part of X and Q meets Z and Q is a patient of W and R is an instance of timeframe and R is an instance of timeframe and equal the time of existence of W and T and T is a part of S and T is a part of R and V is an instance of directional attribute and U is an instance of directional attribute and entities in the process W are moving V holds during Sentities in the process W are moving U and equal V and U or U is an opposite direction of V and ~{ equal V and U } or ~{ U is an opposite direction of V } holds during R |
| ! [V__C : $i] : ((s__instance(V__C, s__Convoy) => ( ? [V__V1:$i, V__V2:$i, V__TIME:$i] : ((~(V__V1 = V__V2) & s__instance(V__V1, s__Vehicle) & s__instance(V__V2, s__Vehicle) & s__instance(V__TIME, s__TimeInterval) & s__temporalPart(V__TIME, s__WhenFn(V__C)) & s__holdsDuring(V__TIME, (s__member(V__V1, V__C) & s__member(V__V2, V__C)))))))) | Mid-level-ontology.kif 24611-24623 | If X is an instance of convoy, then All of the following hold: (1) there exist Y, Z (2) W such that equal Y (3) Z (4) Y is an instance of vehicle (5) Z is an instance of vehicle (6) W is an instance of timeframe (7) W is a part of the time of existence of X (8) Y is a member of X (9) Z is a member of X holds during W |
| ! [V__IMPRISON,V__AGENT,V__INTERVAL] : (((s__instance(V__IMPRISON,s__Imprisoning) & s__detainee(V__IMPRISON,V__AGENT) & s__instance(V__AGENT,s__Human) & s__time(V__IMPRISON,V__INTERVAL) & s__instance(V__INTERVAL,s__TimeInterval)) => (? [V__ARREST,V__TIME] : ((s__instance(V__TIME,s__TimeInterval) & s__time(V__ARREST,V__TIME) & s__earlier(V__TIME,V__INTERVAL) & s__instance(V__ARREST,s__PlacingUnderArrest) & s__arrested(V__ARREST,V__AGENT))))) )
|
Mid-level-ontology.kif 25831-25844 | If X is an instance of imprisoning, Y is a detainee of X, Y is an instance of human, X exists during Z, and Z is an instance of timeframe, then there exist W, V such that V is an instance of timeframe, W exists during V, V happens earlier than Z, W is an instance of placing under arrest, and Y is placed under arrest during W |
| ! [V__Option,V__Date] : (((s__instance(V__Option,s__Agreement) & s__instance(V__Date,s__TimePoint)) => ((s__property(V__Option,s__EuropeanStyleOption) & s__agreementExpirationDate(V__Option,V__Date)) => (? [V__Period,V__Time,V__Exercise] : ((s__instance(V__Time,s__TimeInterval) & (s__instance(V__Period,s__TimeInterval) & (s__EndFn(V__Period) = V__Date) & ((s__instance(V__Exercise,s__ExerciseAnOption) & (s__WhenFn(V__Exercise) = V__Time)) => s__temporalPart(V__Time,V__Period)))))))) )
|
FinancialOntology.kif 2829-2841 | If X the attribute european style option and X has expiration Y, then All of the following hold: (1) there exist Z, W (2) V such that Z is an instance of timeframe (3) equal the end of Z (4) Y (5) V is an instance of exercise an option (6) equal the time of existence of V (7) WW is a part of Z |
| ! [V__PERSON : $i,V__PLACE : $i,V__RESIDENCE : $i,V__T1 : $i] : (((s__holdsDuring(V__T1, (s__attribute(V__PERSON, s__DislocatedCivilian) & s__inhabits(V__PERSON, V__RESIDENCE) & s__located(V__RESIDENCE, V__PLACE))) & s__instance(V__PLACE, s__GeographicArea) & s__instance(V__T1, s__TimeInterval)) => ( ? [V__T0:$i, V__PRIOR_PLACE:$i, V__PRIOR_RES:$i] : ((s__instance(V__T0, s__TimeInterval) & s__earlier(V__T0, V__T1) & s__instance(V__PRIOR_RES, s__Object) & s__instance(V__PRIOR_PLACE, s__GeopoliticalArea) & s__located(V__PRIOR_RES, V__PRIOR_PLACE) & ~(V__PLACE = V__PRIOR_PLACE) & ~(V__RESIDENCE = V__PRIOR_RES) & ~(s__geographicSubregion(V__PLACE, V__PRIOR_PLACE)) & ~(s__geographicSubregion(V__PRIOR_PLACE, V__PLACE)) & s__holdsDuring(V__T0, s__inhabits(V__PERSON, V__PRIOR_RES))))))) | MilitaryPersons.kif 26-47 | If dislocated civilian is an attribute of X, X lives in Y, and Y is located at Z holds during W, Z is an instance of geographic area, and W is an instance of timeframe, then All of the following hold: (1) there exist V, ?PRIOR_PLACE (2) ?PRIOR_RES such that V is an instance of timeframe (3) V happens earlier than W (4) ?PRIOR_RES is an instance of object (5) ?PRIOR_PLACE is an instance of geopolitical area (6) ?PRIOR_RES is located at ?PRIOR_PLACE (7) equal Z (8) ?PRIOR_PLACE (9) equal Y (10) ?PRIOR_RES (11) Z is not a geographic subregion of ?PRIOR_PLACE (12) ?PRIOR_PLACE is not a geographic subregion of Z (13) X lives in ?PRIOR_RES holds during V |
| ! [V__LIST : $i] : ((s__instance(V__LIST, s__ListOnSite) => ( ? [V__SITE:$i, V__ADVERT:$i, V__EARLIER:$i, V__AFTER:$i, V__OWNER:$i] : ((s__instance(V__SITE, s__WebSite) & s__instance(V__ADVERT, s__WebListing) & s__instance(V__EARLIER, s__TimeInterval) & s__instance(V__AFTER, s__TimeInterval) & s__patient(V__LIST, V__ADVERT) & s__EndFn(V__EARLIER) = s__EndFn(V__LIST) & s__earlier(V__LIST, V__AFTER) & s__meetsTemporally(V__LIST, V__AFTER) & s__holdsDuring(V__EARLIER, ~(s__hostedOn(V__ADVERT, V__SITE))) & s__holdsDuring(V__AFTER, s__hostedOn(V__ADVERT, V__SITE)) & s__agent(V__LIST, V__OWNER) & s__possesses(V__OWNER, V__SITE)))))) | UXExperimentalTerms.kif 266-286 | If X is an instance of list on site, then All of the following hold: (1) there exist Y, Z,, , W,, , V (2) U such that Y is an instance of web site (3) Z is an instance of web listing (4) W is an instance of timeframe (5) V is an instance of timeframe (6) Z is a patient of X (7) equal the end of W (8) the end of X (9) X happens earlier than V (10) X meets V (11) Z is hosted on Y holds during W (12) Z is hosted on Y holds during V (13) U is an agent of X (14) U possesses Y |
| ! [V__ATC : $i,V__OBJ : $i,V__USER : $i] : (((s__instance(V__ATC, s__AddToCart) & s__instance(V__OBJ, s__Object) & s__patient(V__ATC, V__OBJ) & s__agent(V__ATC, V__USER)) => ( ? [V__COLL:$i, V__SITE:$i, V__AFTER:$i, V__INTERVAL:$i] : ((s__instance(V__COLL, s__Collection) & s__instance(V__SITE, s__WebSite) & s__instance(V__INTERVAL, s__TimeInterval) & s__webcart(V__USER, V__COLL, V__SITE) & s__BeginFn(V__INTERVAL) = s__EndFn(V__ATC) & s__holdsDuring(V__AFTER, s__member(V__OBJ, V__COLL))))))) | UXExperimentalTerms.kif 1326-1342 | If X is an instance of add to cart, Y is an instance of object, Y is a patient of X, and Z is an agent of X, then All of the following hold: (1) there exist W, V,, , U (2) T such that W is an instance of collection (3) V is an instance of web site (4) T is an instance of timeframe (5) user Z at V has cart W (6) equal the beginning of T (7) the end of X (8) Y is a member of W holds during U |
| ! [V__OBJ : $i,V__USER : $i,V__WATCH : $i] : (((s__instance(V__WATCH, s__WatchItem) & s__instance(V__OBJ, s__Object) & s__patient(V__WATCH, V__OBJ) & s__agent(V__WATCH, V__USER)) => ( ? [V__COLL:$i, V__SITE:$i, V__AFTER:$i, V__INTERVAL:$i] : ((s__instance(V__COLL, s__Collection) & s__instance(V__SITE, s__WebSite) & s__instance(V__INTERVAL, s__TimeInterval) & s__watchingListings(V__USER, V__COLL, V__SITE) & s__BeginFn(V__INTERVAL) = s__EndFn(V__WATCH) & s__holdsDuring(V__AFTER, s__member(V__OBJ, V__COLL))))))) | UXExperimentalTerms.kif 1605-1621 | If X is an instance of watch item, Y is an instance of object, Y is a patient of X, and Z is an agent of X, then All of the following hold: (1) there exist W, V,, , U (2) T such that W is an instance of collection (3) V is an instance of web site (4) T is an instance of timeframe (5) user Z on V is watching W (6) equal the beginning of T (7) the end of X (8) Y is a member of W holds during U |
| ! [V__INTERVAL : $i,V__SITE : $i] : (((s__instance(V__INTERVAL, s__TimeInterval) & s__instance(V__SITE, s__WebSite)) => ( ? [V__NEWBUYERS:$i] : ((s__instance(V__NEWBUYERS, s__Collection) & ( ! [V__AGENT:$i] : ((s__member(V__AGENT, V__NEWBUYERS) => (( ? [V__BUYING:$i] : ((s__instance(V__AGENT, s__AutonomousAgent) & s__instance(V__BUYING, s__Buying) & s__agent(V__BUYING, V__AGENT) & s__instrument(V__BUYING, V__SITE) & s__during(V__BUYING, V__INTERVAL)))) & ~(( ? [V__INTERVAL_BEFORE:$i] : ((s__instance(V__INTERVAL_BEFORE, s__TimeInterval) & s__earlier(V__INTERVAL_BEFORE, V__INTERVAL) & s__holdsDuring(V__INTERVAL_BEFORE, ( ? [V__BUYING_BEFORE:$i] : ((s__instance(V__BUYING_BEFORE, s__Buying) & s__agent(V__BUYING_BEFORE, V__AGENT) & s__instrument(V__BUYING_BEFORE, V__SITE) & s__during(V__BUYING_BEFORE, V__INTERVAL))))))))))))) & s__SiteWideNewBuyersFn(V__INTERVAL, V__SITE) = V__NEWBUYERS))))) | UXExperimentalTerms.kif 3375-3407 | If X is an instance of timeframe and Y is an instance of web site, then All of the following hold: (1) there exists Z such that Z is an instance of collection (2) W W is a member of Zthere exists V such that W is an instance of agent (3) V is an instance of buying (4) W is an agent of V (5) Y is an instrument for V (6) V takes place during X (7) there doesn't exist ?INTERVAL_BEFORE such that ?INTERVAL_BEFORE is an instance of timeframe (8) ?INTERVAL_BEFORE happens earlier than X (9) there exists ?BUYING_BEFORE such that ?BUYING_BEFORE is an instance of buying (10) W is an agent of ?BUYING_BEFORE (11) Y is an instrument for ?BUYING_BEFORE (12) ?BUYING_BEFORE takes place during X holds during ?INTERVAL_BEFORE (13) equal new buyers at Y during X (14) Z |
| ! [V__INTERVAL : $i,V__SITE : $i] : (((s__instance(V__INTERVAL, s__TimeInterval) & s__instance(V__SITE, s__WebSite)) => ( ? [V__NEWREGISTRATIONS:$i] : ((s__instance(V__NEWREGISTRATIONS, s__Collection) & ( ! [V__USER:$i] : (((s__instance(V__USER, s__Human) & ~(( ? [V__INTERVAL_BEFORE:$i] : ((s__instance(V__INTERVAL_BEFORE, s__TimeInterval) & s__earlier(V__INTERVAL_BEFORE, V__INTERVAL) & s__holdsDuring(V__INTERVAL_BEFORE, s__registeredUser(V__USER, V__SITE)))))) & ( ? [V__INTERVAL_DURING:$i] : ((s__instance(V__INTERVAL_DURING, s__TimeInterval) & s__during(V__INTERVAL_DURING, V__INTERVAL) & s__holdsDuring(V__INTERVAL, s__registeredUser(V__USER, V__SITE)))))) => s__member(V__USER, V__NEWREGISTRATIONS)))) & V__NEWREGISTRATIONS = s__SiteWideNewRegistrationsFn(V__INTERVAL, V__SITE)))))) | UXExperimentalTerms.kif 3427-3454 | If X is an instance of timeframe and Y is an instance of web site, then All of the following hold: (1) there exists Z such that Z is an instance of collection (2) W W is an instance of human (3) there doesn't exist ?INTERVAL_BEFORE such that ?INTERVAL_BEFORE is an instance of timeframe (4) ?INTERVAL_BEFORE happens earlier than X (5) W is a registered user of Y holds during ?INTERVAL_BEFORE (6) there exists ?INTERVAL_DURING such that ?INTERVAL_DURING is an instance of timeframe (7) ?INTERVAL_DURING takes place during X (8) W is a registered user of Y holds during XW is a member of Z (9) equal Z (10) new registrations at Y during X |
| ! [V__INTERVAL : $i,V__SITE : $i] : (((s__instance(V__INTERVAL, s__TimeInterval) & s__instance(V__SITE, s__WebSite)) => ( ? [V__NEWSELLERS:$i] : ((s__instance(V__NEWSELLERS, s__Collection) & ( ! [V__AGENT:$i] : ((s__member(V__AGENT, V__NEWSELLERS) => (( ? [V__SELLING:$i] : ((s__instance(V__AGENT, s__AutonomousAgent) & s__instance(V__SELLING, s__Selling) & s__agent(V__SELLING, V__AGENT) & s__instrument(V__SELLING, V__SITE) & s__during(V__SELLING, V__INTERVAL)))) & ~(( ? [V__INTERVAL_BEFORE:$i] : ((s__instance(V__INTERVAL_BEFORE, s__TimeInterval) & s__earlier(V__INTERVAL_BEFORE, V__INTERVAL) & s__holdsDuring(V__INTERVAL_BEFORE, ( ? [V__SELLING_BEFORE:$i] : ((s__instance(V__SELLING_BEFORE, s__Selling) & s__agent(V__SELLING_BEFORE, V__AGENT) & s__instrument(V__SELLING_BEFORE, V__SITE) & s__during(V__SELLING_BEFORE, V__INTERVAL))))))))))))) & s__SiteWideNewSellersFn(V__INTERVAL, V__SITE) = V__NEWSELLERS))))) | UXExperimentalTerms.kif 3474-3506 | If X is an instance of timeframe and Y is an instance of web site, then All of the following hold: (1) there exists Z such that Z is an instance of collection (2) W W is a member of Zthere exists V such that W is an instance of agent (3) V is an instance of selling (4) W is an agent of V (5) Y is an instrument for V (6) V takes place during X (7) there doesn't exist ?INTERVAL_BEFORE such that ?INTERVAL_BEFORE is an instance of timeframe (8) ?INTERVAL_BEFORE happens earlier than X (9) there exists ?SELLING_BEFORE such that ?SELLING_BEFORE is an instance of selling (10) W is an agent of ?SELLING_BEFORE (11) Y is an instrument for ?SELLING_BEFORE (12) ?SELLING_BEFORE takes place during X holds during ?INTERVAL_BEFORE (13) equal new sellers at Y during X (14) Z |
| ! [V__COLL : $i,V__INT : $i,V__MEMBER : $i,V__SITE : $i] : (((s__newRegisteredUsers(V__INT, V__SITE, V__COLL) & s__member(V__MEMBER, V__COLL)) => ( ? [V__DURING:$i] : ((s__instance(V__DURING, s__TimeInterval) & s__during(V__DURING, V__INT) & s__holdsDuring(V__DURING, s__registeredUser(V__MEMBER, V__SITE))))))) | UXExperimentalTerms.kif 3628-3637 | If members of X have registered for Y during Z and W is a member of X, then there exists V such that V is an instance of timeframe, V takes place during Z, and W is a registered user of Y holds during V |
| ! [V__COLL : $i,V__INT1 : $i,V__MEMBER : $i,V__SITE : $i] : (((s__newRegisteredUsers(V__INT1, V__SITE, V__COLL) & s__member(V__MEMBER, V__COLL)) => ~(( ? [V__INT2:$i] : ((s__instance(V__INT2, s__TimeInterval) & s__earlier(V__INT2, V__INT1) & s__holdsDuring(V__INT2, s__registeredUser(V__MEMBER, V__SITE)))))))) | UXExperimentalTerms.kif 3639-3649 | If members of X have registered for Y during Z and W is a member of X, then there doesn't exist V such that V is an instance of timeframe, V happens earlier than Z, and W is a registered user of Y holds during V |
| ! [V__LIST,V__TIME,V__Time] : (((s__instance(V__LIST,s__ConsecutiveTimeIntervalList) & s__inList(V__TIME,V__LIST)) => s__instance(V__Time,s__TimeInterval)) )
|
Weather.kif 3196-3200 | If X is an instance of consecutive time interval list and Y is a member of X, then Z is an instance of timeframe |
| ! [V__ORG : $i] : (((s__instance(V__ORG, s__Organization) & s__attribute(V__ORG, s__WarehousingAndStorage)) => ( ? [V__EV:$i, V__MEM:$i] : ((s__member(V__MEM, V__ORG) & s__agent(V__MEM, V__EV) & ( ? [V__P:$i, V__OBJ:$i] : ((s__instance(V__EV, s__Selling) & s__instance(V__OBJ, s__Object) & s__instance(V__P, s__Human) & s__patient(V__EV, V__P) & s__confersRight(V__MEM, V__P, ( ? [V__B:$i, V__T:$i] : ((s__instance(V__T, s__TimeInterval) & s__instance(V__B, s__Building) & s__possesses(V__P, V__OBJ) & s__holdsDuring(V__T, s__located(V__B, V__OBJ)))))))))))))) | naics.kif 8773-8794 | If X is an instance of organization and warehousing and storage is an attribute of X, then All of the following hold: (1) there exist Y (2) Z such that Z is a member of X (3) Y is an agent of Z (4) there exist W (5) V such that Y is an instance of selling (6) V is an instance of object (7) W is an instance of human (8) W is a patient of Y (9) W allows there exist U (10) T such that T is an instance of timeframe (11) U is an instance of building (12) W possesses V (13) U is located at V holds during T to perform task of the type Z |
| statement |
|
|
| ( ? [V__TIME:$i] : ((s__instance(V__TIME, s__TimeInterval) & s__finishes(V__TIME, s__WhenFn(s__JesusOfNazareth)) & s__starts(V__TIME, s__WhenFn(s__TwelveApostles)) & ( ! [V__MEM:$i] : ((s__holdsDuring(V__TIME, s__member(V__MEM, s__TwelveApostles)) => s__holdsDuring(V__TIME, s__friend(V__MEM, s__JesusOfNazareth)))))))) | Media.kif 1917-1925 | There exists X such that X is an instance of timeframe, X finishes the time of existence of Jesus of Nazareth, X starts the time of existence of Twelve apostles, and Y Y is a member of Twelve apostles holds during XJesus of Nazareth is a friend of Y holds during X |
|