Browsing Interface : Welcome guest : log in
|
Browsing Interface : Welcome guest : log in |
[
Home |
Graph |
LogLearn |
Editor |
]
KB:
Language:
Formal Language:
|
| EndFn |
| appearance as argument number 1 |
|
| s__instance(s__EndFn,s__TemporalRelation)
|
Merge.kif 8181-8181 | End is an instance of temporal relation |
| s__instance(s__EndFn,s__UnaryFunction)
|
Merge.kif 8182-8182 | End is an instance of unary function |
| s__instance(s__EndFn,s__TotalValuedRelation)
|
Merge.kif 8183-8183 | End is an instance of total valued relation |
| s__domain(s__EndFn,n__1,s__TimeInterval)
|
Merge.kif 8184-8184 | The number 1 argument of end is an instance of timeframe |
| s__range(s__EndFn,s__TimePoint)
|
Merge.kif 8185-8185 | The range of end is an instance of time point |
| s__documentation(s__EndFn, s__EnglishLanguage, "A UnaryFunction that maps a TimeInterval to the TimePoint at which the interval ends_") | Merge.kif 8187-8188 | The range of end 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__EndFn(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__OTHERPOINT,V__POINT))))))) )
|
Merge.kif 8190-8197 | If equal the end of X and Y, then For all TimePoint Z: if Z is a part of X and equal Z and Y, then Z happens before Y |
| ! [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__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__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__PROCESSSTART,V__PROCESS,V__AGENTEND,V__AGENT] : (((s__instance(V__PROCESSSTART,s__TimePoint) & s__instance(V__PROCESS,s__Process) & s__instance(V__AGENTEND,s__TimePoint) & s__instance(V__AGENT,s__AutonomousAgent)) => (((V__PROCESSSTART = s__BeginFn(s__WhenFn(V__PROCESS))) & (V__AGENTEND = s__EndFn(s__WhenFn(V__AGENT))) & s__benefits(V__PROCESS,V__AGENT)) => s__before(V__PROCESSSTART,V__AGENTEND))) )
|
Mid-level-ontology.kif 25238-25243 | If equal X and the beginning of the time of existence of Y, equal Z and the end of the time of existence of W, and W is a beneficiary of Y, then X happens before Z |
| ! [V__PROCESSSTART,V__PROCESS,V__AGENTEND,V__AGENT] : (((s__instance(V__PROCESSSTART,s__TimePoint) & s__instance(V__PROCESS,s__Process) & s__instance(V__AGENTEND,s__TimePoint) & s__instance(V__AGENT,s__AutonomousAgent)) => (((V__PROCESSSTART = s__BeginFn(s__WhenFn(V__PROCESS))) & (V__AGENTEND = s__EndFn(s__WhenFn(V__AGENT))) & s__suffers(V__PROCESS,V__AGENT)) => s__before(V__PROCESSSTART,V__AGENTEND))) )
|
Mid-level-ontology.kif 32202-32211 | If equal X and the beginning of the time of existence of Y, equal Z and the end of the time of existence of W, and W suffers from Y, then X happens before Z |
| ! [V__N : $real,V__O : $i,V__START : $i] : (((s__instance(V__START, s__Starting) & s__objectTransferred(V__START, V__O) & s__holdsDuring(s__EndFn(V__START), s__measure(V__O, s__MeasureFn(V__N, s__MilesPerHour)))) => ($greater(V__N,0.0)))) | Mid-level-ontology.kif 34762-34768 | If X is an instance of starting, the object transferred in X is Y, and the measure of Y is Z miles per hour(s) holds during the end of X, then Z is greater than 0.0 |
| ! [V__AREA1 : $i,V__AREA2 : $i,V__EXPORT : $i,V__ITEM : $i] : (((s__instance(V__EXPORT, s__Exporting) & s__patient(V__EXPORT, V__ITEM) & s__instance(V__AREA1, s__GeopoliticalArea) & s__instance(V__AREA2, s__GeopoliticalArea) & s__holdsDuring(s__BeginFn(s__WhenFn(V__EXPORT)), s__located(V__ITEM, V__AREA1)) & s__holdsDuring(s__EndFn(s__WhenFn(V__EXPORT)), s__located(V__ITEM, V__AREA2))) => ~(s__located(V__AREA2, V__AREA1)))) | Economy.kif 2691-2701 | If All of the following hold: (1) X is an instance of exporting (2) Y is a patient of X (3) Z is an instance of geopolitical area (4) W is an instance of geopolitical area (5) Y is located at Z holds during the beginning of the time of existence of X (6) Y is located at W holds during the end of the time of existence of X, then W is not located at Z |
| ! [V__AREA1 : $i,V__AREA2 : $i,V__IMPORT : $i,V__ITEM : $i] : (((s__instance(V__IMPORT, s__Importing) & s__patient(V__IMPORT, V__ITEM) & s__instance(V__AREA1, s__GeopoliticalArea) & s__instance(V__AREA2, s__GeopoliticalArea) & s__holdsDuring(s__BeginFn(s__WhenFn(V__IMPORT)), s__located(V__ITEM, V__AREA1)) & s__holdsDuring(s__EndFn(s__WhenFn(V__IMPORT)), s__located(V__ITEM, V__AREA2))) => ~(s__located(V__AREA2, V__AREA1)))) | Economy.kif 2857-2872 | If All of the following hold: (1) X is an instance of importing (2) Y is a patient of X (3) Z is an instance of geopolitical area (4) W is an instance of geopolitical area (5) Y is located at Z holds during the beginning of the time of existence of X (6) Y is located at W holds during the end of the time of existence of X, then W is not located at Z |
| ! [V__Payment,V__Amount,V__Date,V__DueDate,V__Account] : (((s__instance(V__Payment,s__FinancialTransaction) & s__instance(V__Amount,s__CurrencyMeasure) & s__instance(V__Date,s__Day) & s__instance(V__DueDate,s__TimeInterval)) => ((s__transactionAmount(V__Payment,V__Amount) & s__date(V__Payment,V__Date) & s__instance(V__Account,s__FinancialAccount) & s__destination(V__Payment,s__CurrencyFn(V__Account)) & s__amountDue(V__Account,V__Amount,V__DueDate) & s__before(s__EndFn(V__Date) ,s__BeginFn(V__DueDate))) => s__instance(V__Payment,s__Prepayment))) )
|
FinancialOntology.kif 856-864 | If All of the following hold: (1) X is a transaction amount of Y (2) date of Y is Z (3) W is an instance of financial account (4) Y ends up at the currency of W (5) W amount due X for V (6) the end of Z happens before the beginning of V, then Y is an instance of prepayment |
| ! [V__MaturityDate,V__DateOfWithdrawal,V__CD,V__Withdrawal] : (((s__instance(V__MaturityDate,s__Day) & s__instance(V__DateOfWithdrawal,s__Day)) => ((s__instance(V__CD,s__CertificateOfDeposit) & s__maturityDate(V__CD,V__MaturityDate) & s__instance(V__Withdrawal,s__Withdrawal) & s__origin(V__Withdrawal,s__CurrencyFn(V__CD)) & s__date(V__Withdrawal,V__DateOfWithdrawal) & s__before(s__EndFn(V__DateOfWithdrawal) ,s__BeginFn(V__MaturityDate))) => (? [V__Penalty] : ((s__instance(V__Penalty,s__Penalty) & s__destination(V__Penalty,s__CurrencyFn(V__CD)) & s__causes(V__Withdrawal,V__Penalty)))))) )
|
FinancialOntology.kif 1112-1124 | If All of the following hold: (1) X is an instance of certificate of deposit (2) Y is a maturity date of X (3) Z is an instance of withdrawing from an account (4) Z originates at the currency of X (5) date of Z is W (6) the end of W happens before the beginning of Y, then there exists V such that V is an instance of penalizing, V ends up at the currency of X, and Z causes V |
| ! [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 |
| ! [V__Agent : $i,V__ExpDate : $i,V__Option : $i,V__Price : $i,V__Seller : $i,V__Stocks : $i,V__Time : $i] : (((s__instance(V__Option, s__CallOption) & s__optionSeller(V__Option, V__Seller) & 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__holdsObligation(V__Seller, ( ? [V__Sell:$i] : ((s__instance(V__Sell, s__Selling) & s__patient(V__Sell, V__Stocks) & s__time(V__Sell, V__Time) & s__measure(V__Stocks, s__MeasureFn(100, s__ShareUnit)) & s__agent(V__Sell, V__Agent))))))) | FinancialOntology.kif 2672-2689 | If All of the following hold: (1) X is an instance of call option (2) Y sells 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 is obliged to perform tasks of type there exists T such that T is an instance of selling and V is a patient of T and T exists during U and the measure of V is 100 share unit(s) and S is an agent of T |
| Display limited to 25 items. Show next 25 | ||
| Display limited to 25 items. Show next 25 |
| consequent |
|
|
| ! [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__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__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__M] : ((s__instance(V__M,s__Midnight) => (? [V__D] : ((s__instance(V__D,s__Day) & (V__M = s__EndFn(V__D)))))) )
|
Merge.kif 8983-8988 | If X is an instance of midnight, then there exists Y such that Y is an instance of day, equal X, and the end of Y |
| ! [V__EVE] : ((s__instance(V__EVE,s__Evening) => (? [V__MID] : ((s__instance(V__MID,s__Midnight) & (s__EndFn(V__EVE) = V__MID))))) )
|
Merge.kif 9117-9122 | If X is an instance of evening, then there exists Y such that Y is an instance of midnight, equal the end 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__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 |
| ! [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__AGENT : $i,V__CONTENT : $i,V__INTERPRET : $i] : (((s__instance(V__INTERPRET, s__Interpreting) & s__agent(V__INTERPRET, V__AGENT) & s__patient(V__INTERPRET, V__CONTENT) & s__instance(V__CONTENT, s__ContentBearingObject)) => ( ? [V__PROP:$i] : (s__holdsDuring(s__EndFn(s__WhenFn(V__INTERPRET)), s__believes(V__AGENT, s__containsInformation(V__CONTENT, V__PROP))))))) | Merge.kif 11110-11122 | If X is an instance of interpreting, Y is an agent of X, Z is a patient of X, and Z is an instance of content bearing object, then there exists W such that Y believes Z contains information W 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__destination(V__MOTION, V__PLACE)) => s__holdsDuring(s__EndFn(s__WhenFn(V__MOTION)), s__located(V__OBJ, V__PLACE)))) | Merge.kif 11304-11309 | If X is an instance of motion, Y moves during X, and X ends up at Z, then Y is located at Z holds during the end of the time of existence of X |
| ! [V__PROC : $i] : ((s__instance(V__PROC, s__DirectionChange) => ( ? [V__ATTR:$i] : ((s__instance(V__ATTR, s__DirectionalAttribute) & ((s__holdsDuring(s__BeginFn(s__WhenFn(V__PROC)), s__manner(V__PROC, V__ATTR)) & s__holdsDuring(s__EndFn(s__WhenFn(V__PROC)), ~(s__manner(V__PROC, V__ATTR)))) | (s__holdsDuring(s__EndFn(s__WhenFn(V__PROC)), s__manner(V__PROC, V__ATTR)) & s__holdsDuring(s__BeginFn(s__WhenFn(V__PROC)), ~(s__manner(V__PROC, V__ATTR)))))))))) | Merge.kif 11560-11571 | If X is an instance of direction change, then there exists Y such that Y is an instance of directional attribute and X is performed in the manner Y holds during the beginning of the time of existence of X and X is not performed in the manner Y holds during the end of the time of existence of X or X is performed in the manner Y holds during the end of the time of existence of X and X is not performed in the manner Y 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 |
|