Browsing Interface : Welcome guest : log in
|
Browsing Interface : Welcome guest : log in |
[
Home |
Graph |
LogLearn |
Editor |
]
KB:
Language:
Formal Language:
|
| holdsDuring |
| appearance as argument number 1 |
|
| s__instance(s__holdsDuring,s__BinaryPredicate)
|
Merge.kif 3982-3982 | holds during is an instance of binary predicate |
| s__domain(s__holdsDuring,n__1,s__TimePosition)
|
Merge.kif 3983-3983 | The number 1 argument of holds during is an instance of time position |
| s__domain(s__holdsDuring,n__2,s__Formula)
|
Merge.kif 3984-3984 | The number 2 argument of holds during is an instance of formula |
| s__documentation(s__holdsDuring, s__EnglishLanguage, "(holdsDuring ?TIME ?FORMULA) means that the proposition denoted by ?FORMULA is true in the time frame ?TIME_ Note that this implies that ?FORMULA is true at every TimePoint which is a temporalPart of ?TIME_") | Merge.kif 3986-3989 | The number 2 argument of holds during is an instance of formula |
| appearance as argument number 2 |
|
|
| s__relatedInternalConcept(s__time,s__holdsDuring)
|
Merge.kif 3972-3972 | time is internally related to holds during |
| s__termFormat(s__EnglishLanguage, s__holdsDuring, "holds during") | domainEnglishFormat.kif 28355-28355 | time is internally related to holds during |
| s__termFormat(s__ChineseTraditionalLanguage, s__holdsDuring, "持有期間") | domainEnglishFormat.kif 28356-28356 | time is internally related to holds during |
| s__termFormat(s__ChineseLanguage, s__holdsDuring, "持有期间") | domainEnglishFormat.kif 28357-28357 | time is internally related to holds during |
| s__format(s__EnglishLanguage, s__holdsDuring, "%2 %n{doesnt} hold%p{s} during %1") | english_format.kif 122-122 | time is internally related to holds during |
| antecedent |
|
|
| ! [V__AGENT : $i,V__TIME : $i] : (((s__holdsDuring(V__TIME, s__attribute(V__AGENT, s__LegalPersonhood)) => s__holdsDuring(V__TIME, (s__capability(s__LegalAction, s__agent, V__AGENT) | s__capability(s__LegalAction, s__patient, V__AGENT)))) & (s__holdsDuring(V__TIME, (s__capability(s__LegalAction, s__agent, V__AGENT) | s__capability(s__LegalAction, s__patient, V__AGENT))) => s__holdsDuring(V__TIME, s__attribute(V__AGENT, s__LegalPersonhood))))) | Merge.kif 1695-1701 | Legal personhood is an attribute of X holds during Y if and only if X is capable of doing legal action as a agent or X is capable of doing legal action as a patient holds during Y |
| ! [V__TIME : $i,V__X : $i,V__Y : $i] : ((s__holdsDuring(V__TIME, s__leader(V__X, V__Y)) => s__holdsDuring(V__TIME, s__attribute(V__Y, s__Living)))) | Merge.kif 1711-1713 | If X is a leader of Y holds during Z, then living is an attribute of X holds during Z |
| ! [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__SITUATION1 : $i,V__SITUATION2 : $i,V__TIME : $i] : (((s__holdsDuring(V__TIME, V__SITUATION1) & s__entails(V__SITUATION1, V__SITUATION2)) => s__holdsDuring(V__TIME, V__SITUATION2))) | Merge.kif 3991-3995 | If X holds during Y and X entails Z, then Z holds during Y |
| ! [V__SITUATION : $i,V__TIME : $i] : ((s__holdsDuring(V__TIME, ~(V__SITUATION)) => ~(s__holdsDuring(V__TIME, V__SITUATION)))) | Merge.kif 3997-4001 | If X holds during Y, then X doesn't hold during Y |
| ! [V__ENTITY : $i,V__FORMULA : $i,V__NORM : $i,V__TIME : $i] : ((s__holdsDuring(V__TIME, s__confersNorm(V__ENTITY, V__NORM, V__FORMULA)) => (s__holdsDuring(s__ImmediatePastFn(V__TIME), ~(s__modalAttribute(V__FORMULA, V__NORM))) & s__holdsDuring(s__ImmediateFutureFn(V__TIME), s__modalAttribute(V__FORMULA, V__NORM))))) | Merge.kif 4103-4113 | If X confers norm Y for Z holds during W, then the statement Z doesn't have the modal force of Y holds during immediately before W and the statement Z has the modal force of Y holds during immediately after W |
| ! [V__ENTITY : $i,V__FORMULA : $i,V__NORM : $i,V__TIME : $i] : ((s__holdsDuring(V__TIME, s__deprivesNorm(V__ENTITY, V__NORM, V__FORMULA)) => (s__holdsDuring(s__ImmediatePastFn(V__TIME), s__modalAttribute(V__FORMULA, V__NORM)) & s__holdsDuring(s__ImmediateFutureFn(V__TIME), ~(s__modalAttribute(V__FORMULA, V__NORM)))))) | Merge.kif 4125-4134 | If X deprives norm Y for Z holds during W, then the statement Z has the modal force of Y holds during immediately before W and the statement Z doesn't have the modal force of Y holds during immediately after W |
| ! [V__REGION : $i,V__THING : $i,V__TIME : $i] : ((s__holdsDuring(V__TIME, s__exactlyLocated(V__THING, V__REGION)) => s__WhereFn(V__THING, V__TIME) = V__REGION)) | Merge.kif 4352-4356 | If X is exactly located in Y holds during Z, then equal the place where X was at Z and Y |
| ! [V__OBJ : $i,V__P : $i,V__PERSON : $i,V__T : $i] : (((s__holdsDuring(V__T, s__possesses(V__PERSON, V__OBJ)) & s__part(V__P, V__OBJ)) => s__holdsDuring(V__T, s__possesses(V__PERSON, V__P)))) | Merge.kif 4371-4377 | If X possesses Y holds during Z and W is a part of Y, then X possesses W holds during Z |
| ! [V__AGENT1 : $i,V__AGENT2 : $i,V__OBJ : $i,V__TIME : $i] : (((s__instance(V__TIME, s__TimePosition) & s__holdsDuring(V__TIME, s__possesses(V__AGENT1, V__OBJ)) & s__holdsDuring(V__TIME, s__possesses(V__AGENT2, V__OBJ))) => V__AGENT1 = V__AGENT2)) | Merge.kif 4379-4384 | If X is an instance of time position, Y possesses Z holds during X, and W possesses Z holds during X, then equal Y and W |
| ! [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__SITUATION : $i,V__TIME1 : $i,V__TIME2 : $i] : (((s__holdsDuring(V__TIME1, V__SITUATION) & s__temporalPart(V__TIME2, V__TIME1)) => s__holdsDuring(V__TIME2, V__SITUATION))) | Merge.kif 8128-8132 | If X holds during Y and Z is a part of Y, then X holds during Z |
| ! [V__INST1 : $i,V__INST2 : $i,V__INTERVAL : $i] : (((s__holdsDuring(V__INTERVAL, s__?REL(V__INST1, V__INST2)) & s__instance(V__INST1, s__Physical) & s__instance(V__INST2, s__Physical)) => (s__time(V__INST1, V__INTERVAL) & s__time(V__INST2, V__INTERVAL)))) | Merge.kif 8134-8141 | If X Y and Z holds during W, Y is an instance of physical, and Z is an instance of physical, then Y exists during W and Z exists during W |
| ! [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__HOLE : $i,V__OBJ : $i,V__TIME : $i] : ((s__holdsDuring(V__TIME, s__fills(V__OBJ, V__HOLE)) => s__attribute(V__HOLE, s__Fillable))) | Merge.kif 10182-10185 | If X fills Y holds during Z, then fillable is an attribute of Y |
| ! [V__AGENT : $i,V__LENGTH1 : $i,V__LENGTH2 : $i,V__RUN : $i,V__TIME : $i,V__WALK : $i] : (((s__instance(V__WALK, s__Walking) & s__instance(V__RUN, s__Running) & s__agent(V__WALK, V__AGENT) & s__agent(V__RUN, V__AGENT) & s__holdsDuring(s__WhenFn(V__WALK), s__measure(V__AGENT, s__SpeedFn(V__LENGTH1, V__TIME))) & s__holdsDuring(s__WhenFn(V__RUN), s__measure(V__AGENT, s__SpeedFn(V__LENGTH2, V__TIME)))) => ($greater(V__LENGTH2,V__LENGTH1)))) | Merge.kif 11410-11418 | If All of the following hold: (1) X is an instance of walking (2) Y is an instance of running (3) Z is an agent of X (4) Z is an agent of Y (5) the measure of Z is W per V holds during the time of existence of X (6) the measure of Z is U per V holds during the time of existence of Y, then U is greater than W |
| ! [V__L : $i,V__N : $real,V__T : $i,V__W : $i] : (((s__attribute(V__W, s__Windy) & s__located(V__W, V__L) & V__T = s__WhenFn(V__W) & s__holdsDuring(V__T, s__surfaceWindSpeed(V__L, s__MeasureFn(V__N, s__MilesPerHour)))) => ($greater(V__N,20.0)))) | Merge.kif 11545-11553 | If windy is an attribute of X, X is located at Y, equal Z and the time of existence of X, and W miles per hour(s) is a surface wind speed of Y holds during Z, then W is greater than 20.0 |
| ! [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__DISCOVER : $i,V__DISCOVERING : $i,V__OBJ : $i,V__PLACE : $i] : (((s__instance(V__DISCOVER, s__Discovering) & s__agent(V__DISCOVER, V__A) & s__patient(V__DISCOVER, V__OBJ) & s__holdsDuring(s__WhenFn(V__DISCOVER), s__located(V__OBJ, V__PLACE))) => s__holdsDuring(s__ImmediateFutureFn(s__WhenFn(V__DISCOVERING)), s__knows(V__A, s__located(V__OBJ, V__PLACE))))) | Merge.kif 12256-12268 | If X is an instance of discovering, Y is an agent of X, Z is a patient of X, and Z is located at W holds during the time of existence of X, then Y knows Z is located at W holds during immediately after the time of existence of V |
| ! [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__BOILING : $i,V__MEASURE : $i,V__SUBSTANCE : $i,V__TEMP1 : $real,V__TEMP2 : $real,V__TYPE : $i] : (((s__instance(V__BOILING, s__Boiling) & s__boilingPoint(V__TYPE, s__MeasureFn(V__TEMP1, V__MEASURE)) & s__instance(V__SUBSTANCE, V__TYPE) & s__patient(V__BOILING, V__SUBSTANCE) & s__holdsDuring(s__WhenFn(V__BOILING), s__measure(V__SUBSTANCE, s__MeasureFn(V__TEMP2, V__MEASURE))) & s__instance(V__MEASURE, s__UnitOfTemperature)) => ($greatereq(V__TEMP2,V__TEMP1)))) | Merge.kif 14140-14148 | If All of the following hold: (1) X is an instance of boiling (2) Y Z(s) is a boiling point of W (3) V is an instance of W (4) V is a patient of X (5) the measure of V is U Z(s) holds during the time of existence of X (6) Z is an instance of unit of temperature, then U is greater than or equal to Y |
| ! [V__MEASURE : $i,V__SUBSTANCE : $i,V__TEMP1 : $real,V__TEMP2 : $real,V__TIME : $i,V__TYPE : $i] : (((s__boilingPoint(V__TYPE, s__MeasureFn(V__TEMP1, V__MEASURE)) & s__instance(V__SUBSTANCE, V__TYPE) & s__holdsDuring(V__TIME, s__measure(V__SUBSTANCE, s__MeasureFn(V__TEMP2, V__MEASURE))) & s__instance(V__MEASURE, s__UnitOfTemperature) & ($greatereq(V__TEMP2,V__TEMP1))) => (s__holdsDuring(V__TIME, s__attribute(V__SUBSTANCE, s__Gas)) | ( ? [V__BOIL:$i] : ((s__overlapsTemporally(s__WhenFn(V__BOIL), V__TIME) & s__instance(V__BOIL, s__Boiling) & s__patient(V__BOIL, V__SUBSTANCE))))))) | Merge.kif 14150-14163 | If X Y(s) is a boiling point of Z, W is an instance of Z, the measure of W is V Y(s) holds during U, Y is an instance of unit of temperature, and V is greater than or equal to X, then gas is an attribute of W holds during U or there exists T such that U overlaps the time of existence of T, T is an instance of boiling, and W is a patient of T |
| ! [V__MEASURE : $i,V__SUBSTANCE : $i,V__TEMP1 : $real,V__TEMP2 : $real,V__TEMP3 : $real,V__TIME : $i,V__TYPE : $i] : (((s__instance(V__SUBSTANCE, V__TYPE) & s__boilingPoint(V__TYPE, s__MeasureFn(V__TEMP1, V__MEASURE)) & s__meltingPoint(V__TYPE, s__MeasureFn(V__TEMP2, V__MEASURE)) & s__instance(V__MEASURE, s__UnitOfTemperature) & s__holdsDuring(V__TIME, s__measure(V__SUBSTANCE, s__MeasureFn(V__TEMP3, V__MEASURE))) & ($greater(V__TEMP3,V__TEMP2)) & ($less(V__TEMP3,V__TEMP1))) => (s__holdsDuring(V__TIME, s__attribute(V__SUBSTANCE, s__Liquid)) | ( ? [V__MELT:$i] : ((s__overlapsTemporally(s__WhenFn(V__MELT), V__TIME) & s__instance(V__MELT, s__Melting) & s__patient(V__MELT, V__SUBSTANCE))))))) | Merge.kif 14172-14187 | If All of the following hold: (1) X is an instance of Y (2) Z W(s) is a boiling point of Y (3) V W(s) is a melting point of Y (4) W is an instance of unit of temperature (5) the measure of X is U W(s) holds during T (6) U is greater than V (7) U is less than Z, then liquid is an attribute of X holds during T or there exists S such that T overlaps the time of existence of S, S is an instance of melting, and X is a patient of S |
| ! [V__MEASURE : $i,V__SUBSTANCE : $i,V__TEMP1 : $real,V__TEMP2 : $real,V__TIME : $i,V__TYPE : $i] : (((s__instance(V__SUBSTANCE, V__TYPE) & s__meltingPoint(V__TYPE, s__MeasureFn(V__TEMP1, V__MEASURE)) & s__holdsDuring(V__TIME, s__measure(V__SUBSTANCE, s__MeasureFn(V__TEMP2, V__MEASURE))) & s__instance(V__MEASURE, s__UnitOfTemperature) & ($less(V__TEMP2,V__TEMP1))) => (s__holdsDuring(V__TIME, s__attribute(V__SUBSTANCE, s__Solid)) | ( ? [V__FREEZE:$i] : ((s__overlapsTemporally(s__WhenFn(V__FREEZE), V__TIME) & s__instance(V__FREEZE, s__Freezing) & s__patient(V__FREEZE, V__SUBSTANCE))))))) | Merge.kif 14189-14202 | If X is an instance of Y, Z W(s) is a melting point of Y, the measure of X is V W(s) holds during U, W is an instance of unit of temperature, and V is less than Z, then solid is an attribute of X holds during U or there exists T such that U overlaps the time of existence of T, T is an instance of freezing, and X is a patient of T |
| Display limited to 25 items. Show next 25 | ||
| Display limited to 25 items. Show next 25 |
| consequent |
|
|
| ! [V__AGENT : $i,V__TIME : $i] : (((s__holdsDuring(V__TIME, s__attribute(V__AGENT, s__LegalPersonhood)) => s__holdsDuring(V__TIME, (s__capability(s__LegalAction, s__agent, V__AGENT) | s__capability(s__LegalAction, s__patient, V__AGENT)))) & (s__holdsDuring(V__TIME, (s__capability(s__LegalAction, s__agent, V__AGENT) | s__capability(s__LegalAction, s__patient, V__AGENT))) => s__holdsDuring(V__TIME, s__attribute(V__AGENT, s__LegalPersonhood))))) | Merge.kif 1695-1701 | Legal personhood is an attribute of X holds during Y if and only if X is capable of doing legal action as a agent or X is capable of doing legal action as a patient holds during Y |
| ! [V__TIME : $i,V__X : $i,V__Y : $i] : ((s__holdsDuring(V__TIME, s__leader(V__X, V__Y)) => s__holdsDuring(V__TIME, s__attribute(V__Y, s__Living)))) | Merge.kif 1711-1713 | If X is a leader of Y holds during Z, then living is an attribute of X holds during Z |
| ! [V__C : $i,V__P : $i,V__R : $i] : (((s__resourceExhausted(V__P, V__R) & s__instance(V__R, V__C)) => s__holdsDuring(s__ImmediateFutureFn(s__WhenFn(V__P)), ~(( ? [V__OBJ1:$i] : ((s__part(V__OBJ1, V__R) & s__instance(V__OBJ1, V__C)))))))) | Merge.kif 2644-2655 | If X exhausts Y and Y is an instance of Z, then there doesn't exist W such that W is a part of Y and W is an instance of Z holds during immediately after the time of existence of X |
| ! [V__AGENT : $i,V__FORMULA : $i] : ((s__believes(V__AGENT, V__FORMULA) => ( ? [V__TIME:$i] : (s__holdsDuring(V__TIME, s__considers(V__AGENT, V__FORMULA)))))) | Merge.kif 2926-2930 | If X believes Y, then there exists Z such that X considers Y holds during Z |
| ! [V__SITUATION1 : $i,V__SITUATION2 : $i,V__TIME : $i] : (((s__holdsDuring(V__TIME, V__SITUATION1) & s__entails(V__SITUATION1, V__SITUATION2)) => s__holdsDuring(V__TIME, V__SITUATION2))) | Merge.kif 3991-3995 | If X holds during Y and X entails Z, then Z holds during Y |
| ! [V__SITUATION : $i,V__TIME : $i] : ((s__holdsDuring(V__TIME, ~(V__SITUATION)) => ~(s__holdsDuring(V__TIME, V__SITUATION)))) | Merge.kif 3997-4001 | If X holds during Y, then X doesn't hold during Y |
| ! [V__ENTITY : $i,V__FORMULA : $i,V__NORM : $i,V__TIME : $i] : ((s__holdsDuring(V__TIME, s__confersNorm(V__ENTITY, V__NORM, V__FORMULA)) => (s__holdsDuring(s__ImmediatePastFn(V__TIME), ~(s__modalAttribute(V__FORMULA, V__NORM))) & s__holdsDuring(s__ImmediateFutureFn(V__TIME), s__modalAttribute(V__FORMULA, V__NORM))))) | Merge.kif 4103-4113 | If X confers norm Y for Z holds during W, then the statement Z doesn't have the modal force of Y holds during immediately before W and the statement Z has the modal force of Y holds during immediately after W |
| ! [V__ENTITY : $i,V__FORMULA : $i,V__NORM : $i,V__TIME : $i] : ((s__holdsDuring(V__TIME, s__deprivesNorm(V__ENTITY, V__NORM, V__FORMULA)) => (s__holdsDuring(s__ImmediatePastFn(V__TIME), s__modalAttribute(V__FORMULA, V__NORM)) & s__holdsDuring(s__ImmediateFutureFn(V__TIME), ~(s__modalAttribute(V__FORMULA, V__NORM)))))) | Merge.kif 4125-4134 | If X deprives norm Y for Z holds during W, then the statement Z has the modal force of Y holds during immediately before W and the statement Z doesn't have the modal force of Y holds during immediately after W |
| ! [V__REGION : $i,V__THING : $i,V__TIME : $i] : ((s__WhereFn(V__THING, V__TIME) = V__REGION => s__holdsDuring(V__TIME, s__exactlyLocated(V__THING, V__REGION)))) | Merge.kif 4346-4350 | If equal the place where X was at Y and Z, then X is exactly located in Z holds during Y |
| ! [V__OBJ : $i,V__P : $i,V__PERSON : $i,V__T : $i] : (((s__holdsDuring(V__T, s__possesses(V__PERSON, V__OBJ)) & s__part(V__P, V__OBJ)) => s__holdsDuring(V__T, s__possesses(V__PERSON, V__P)))) | Merge.kif 4371-4377 | If X possesses Y holds during Z and W is a part of Y, then X possesses W holds during Z |
| ! [V__PROC1 : $i,V__PROC2 : $i] : ((s__hindersSubclass(V__PROC1, V__PROC2) => ( ! [V__TIME:$i, V__PLACE:$i] : (s__decreasesLikelihood(s__holdsDuring(V__TIME, ( ? [V__INST1:$i] : ((s__instance(V__INST1, V__PROC1) & s__eventLocated(V__INST1, V__PLACE))))), s__holdsDuring(V__TIME, ( ? [V__INST2:$i] : ((s__instance(V__INST2, V__PROC2) & s__eventLocated(V__INST2, V__PLACE)))))))))) | Merge.kif 4433-4446 | If instances of X hinder instances of Y, then For all Entities Z and W: there exists V such that V is an instance of X, V is located at W holds during Z decreases likelihood of there exists U such that U is an instance of Y, and U is located at W holds during Z |
| ! [V__PROC1 : $i,V__PROC2 : $i] : ((s__preventsSubclass(V__PROC1, V__PROC2) => ( ! [V__TIME:$i, V__PLACE:$i] : ((s__holdsDuring(V__TIME, ( ? [V__INST1:$i] : ((s__instance(V__INST1, V__PROC1) & s__eventLocated(V__INST1, V__PLACE))))) => ~(s__holdsDuring(V__TIME, ( ? [V__INST2:$i] : ((s__instance(V__INST2, V__PROC2) & s__eventLocated(V__INST2, V__PLACE))))))))))) | Merge.kif 4462-4476 | If instances of X prevent instances of Y, then For all TimePosition Z and Entity W: if there exists V such that V is an instance of X and V is located at W holds during Z, then there doesn't exist U such that U is an instance of Y and U is located at W doesn't hold during Z |
| ! [V__L : $i,V__P : $i,V__T : $i,V__X : $i] : (((s__prevents(V__X, V__P) & s__WhenFn(V__X) = V__T & s__eventLocated(V__X, V__L)) => ~(s__holdsDuring(V__T, ( ? [V__Y:$i] : ((s__instance(V__Y, V__P) & s__eventLocated(V__Y, V__L)))))))) | Merge.kif 4489-4499 | If X prevents the occurrence of Y, equal the time of existence of X and Z, and X is located at W, then there doesn't exist V such that V is an instance of Y and V is located at W doesn't hold during Z |
| ! [V__PROC : $i,V__X : $i] : ((s__hinders(V__X, V__PROC) => ( ? [V__L:$i, V__T:$i] : (s__decreasesLikelihood((s__WhenFn(V__X) = V__T & s__eventLocated(V__X, V__L)), s__holdsDuring(V__T, ( ? [V__Y:$i] : ((s__instance(V__Y, V__PROC) & s__eventLocated(V__Y, V__L)))))))))) | Merge.kif 4511-4522 | If X hinders Y, then there exist Z, W such that equal the time of existence of X, W, X is located at Z decreases likelihood of there exists V such that V is an instance of Y, and V is located at Z holds during W |
| ! [V__PROC : $i,V__TIME1 : $i] : ((s__frequency(V__PROC, V__TIME1) => ( ! [V__TIME2:$i] : ((s__duration(V__TIME2, V__TIME1) => ( ? [V__POSITION:$i] : ((s__temporalPart(V__POSITION, V__TIME2) & s__holdsDuring(V__POSITION, ( ? [V__INST:$i] : (s__instance(V__INST, V__PROC)))))))))))) | Merge.kif 8091-8101 | If X occurs every Y, then For all TimeInterval Z: if duration of Z is Y, then there exists W such that W is a part of Z and there exists V such that V is an instance of X holds during W |
| ! [V__SITUATION : $i,V__TIME1 : $i,V__TIME2 : $i] : (((s__holdsDuring(V__TIME1, V__SITUATION) & s__temporalPart(V__TIME2, V__TIME1)) => s__holdsDuring(V__TIME2, V__SITUATION))) | Merge.kif 8128-8132 | If X holds during Y and Z is a part of Y, then X holds during Z |
| ! [V__DEATH : $i,V__ORG : $i] : (((s__instance(V__DEATH, s__Death) & s__instance(V__ORG, s__Organism) & s__experiencer(V__DEATH, V__ORG)) => ( ? [V__REM:$i, V__OBJ:$i] : ((s__result(V__DEATH, V__REM) & s__instance(V__REM, s__OrganicObject) & s__holdsDuring(s__FutureFn(s__WhenFn(V__DEATH)), s__attribute(V__REM, s__Dead)) & (s__holdsDuring(s__ImmediateFutureFn(s__WhenFn(V__DEATH)), s__part(V__OBJ, V__REM)) => s__holdsDuring(s__ImmediatePastFn(s__WhenFn(V__DEATH)), s__part(V__OBJ, V__ORG)))))))) | Merge.kif 10450-10469 | If X is an instance of death, Y is an instance of organism, and Y experiences X, then there exist Z and W such that Z is a result of X and Z is an instance of organic object and dead is an attribute of Z holds during after the time of existence of X and W is a part of Z holds during immediately after the time of existence of XW is a part of Y holds during immediately before the time of existence of X |
| ! [V__HUMAN : $i,V__PROC : $i] : (((s__instance(V__PROC, s__IntentionalProcess) & s__agent(V__PROC, V__HUMAN) & s__instance(V__HUMAN, s__Animal)) => s__holdsDuring(s__WhenFn(V__PROC), s__attribute(V__HUMAN, s__Awake)))) | Merge.kif 10750-10755 | If X is an instance of intentional process, Y is an agent of X, and Y is an instance of animal, then awake is an attribute of Y holds during the time of existence of X |
| ! [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__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__ImmediateFutureFn(s__WhenFn(V__JOIN)), s__employs(V__ORG, V__PERSON)))) | Merge.kif 10867-10876 | 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 employs Z holds during immediately after 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__PERSON : $i] : (((s__instance(V__LEAVE, s__Quitting) & s__instance(V__ORG, s__Organization) & s__agent(V__LEAVE, V__PERSON) & s__patient(V__LEAVE, V__ORG)) => s__desires(V__PERSON, s__holdsDuring(s__EndFn(s__WhenFn(V__LEAVE)), ~(s__member(V__PERSON, V__ORG)))))) | Merge.kif 10912-10922 | If X is an instance of quitting, Y is an instance of organization, Z is an agent of X, and Y is a patient of X, then Z desires 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 |
| Display limited to 25 items. Show next 25 | ||
| Display limited to 25 items. Show next 25 |
| statement |
|
|
| ( ? [V__T:$i] : ((s__instance(V__T, s__YearFn(2002)) & s__holdsDuring(V__T, s__coworker(s__SteveJobsOfApple, s__TimCookOfApple))))) | ComputingBrands.kif 2441-2445 | There exists X such that X is an instance of the year 2002 and Tim Cook is a coworker of Steve Jobs holds during X |
| ( ? [V__T:$i] : ((s__instance(V__T, s__YearFn(1976)) & s__holdsDuring(V__T, s__coworker(s__SteveJobsOfApple, s__SteveWozniakOfApple))))) | ComputingBrands.kif 2453-2457 | There exists X such that X is an instance of the year 1976 and Steve Wozniak is a coworker of Steve Jobs holds during X |
| ( ? [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 |
| ! [V__AGE : $i,V__AGEMINUSONE : $i,V__AREA : $i,V__MILITARYAGE : $i,V__PERSON : $i,V__YEAR : $i] : (s__ReachingMilitaryAgeAnnuallyMaleFn(V__AREA, V__YEAR) = s__CardinalityFn(s__KappaFn(V__PERSON, (s__instance(V__PERSON, s__Human) & s__attribute(V__PERSON, s__Male) & s__militaryAge(V__AREA, V__MILITARYAGE) & V__AGEMINUSONE = $difference(V__AGE ,1) & s__holdsDuring(V__YEAR, (s__age(V__PERSON, V__AGEMINUSONE) | s__age(V__PERSON, V__AGE))) & V__AGE = V__MILITARYAGE & s__inhabits(V__PERSON, V__AREA))))) | Military.kif 1197-1210 | equal the reaching military age annually male of X, Y, and the number of instances in the class described by Z |
| ! [V__AREA : $i,V__BIRTH : $i,V__INFANT : $i,V__WOMAN : $i,V__Y : $int,V__YEAR : $i] : ((s__instance(V__YEAR, s__YearFn(V__Y)) & s__ChildrenBornPerWomanFn(V__AREA, V__YEAR) = s__CardinalityFn(s__KappaFn(V__INFANT, (s__instance(V__BIRTH, s__Birth) & s__experiencer(V__BIRTH, V__INFANT) & s__agent(V__BIRTH, V__WOMAN) & s__instance(V__WOMAN, s__Human) & s__attribute(V__WOMAN, s__Female) & s__holdsDuring(V__YEAR, s__inhabits(V__WOMAN, V__AREA))))))) | People.kif 490-503 | X is an instance of the year Y and equal the children born per woman of Z, X, and the number of instances in the class described by W |
| appearance as argument number 0 |
|
|
|