(=>
(equal
(EndFn ?INTERVAL) ?POINT)
(forall (?OTHERPOINT)
(=>
(and
(temporalPart ?OTHERPOINT ?INTERVAL)
(not
(equal ?OTHERPOINT ?POINT)))
(before ?OTHERPOINT ?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 |
(=>
(and
(resource ?PROC ?OBJ)
(holdsDuring
(BeginFn
(WhenFn ?PROC))
(measure ?OBJ ?QUANT1))
(holdsDuring
(EndFn
(WhenFn ?PROC))
(measure ?OBJ ?QUANT2)))
(greaterThan ?QUANT1 ?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 |
(=>
(and
(equal
(BeginFn ?INTERVAL1)
(BeginFn ?INTERVAL2))
(before
(EndFn ?INTERVAL1)
(EndFn ?INTERVAL2)))
(starts ?INTERVAL1 ?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 |
(=>
(and
(before
(BeginFn ?INTERVAL2)
(BeginFn ?INTERVAL1))
(equal
(EndFn ?INTERVAL2)
(EndFn ?INTERVAL1)))
(finishes ?INTERVAL1 ?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 |
(=>
(temporallyBetweenOrEqual
(BeginFn
(WhenFn ?PHYS)) ?TIME
(EndFn
(WhenFn ?PHYS)))
(and
(time ?PHYS ?TIME)
(instance ?TIME 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 |
(=>
(and
(instance ?TI TimeInterval)
(equal ?S
(BeginFn ?TI))
(equal ?E
(EndFn ?TI)))
(before ?S ?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 |
(=>
(and
(instance ?TI1 TimeInterval)
(instance ?TI2 TimeInterval)
(beforeOrEqual
(BeginFn ?TI2)
(BeginFn ?TI1))
(before
(BeginFn ?TI1)
(EndFn ?TI2)))
(overlapsTemporally ?TI2 ?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 |
(=>
(equal
(EndFn ?INTERVAL1)
(BeginFn ?INTERVAL2))
(meetsTemporally ?INTERVAL1 ?INTERVAL2)) |
Merge.kif 8541-8545 |
If equal the end of X and the beginning of Y, then X meets Y |
(=>
(and
(instance ?INTERVAL1 TimeInterval)
(instance ?INTERVAL2 TimeInterval)
(equal
(BeginFn ?INTERVAL1)
(BeginFn ?INTERVAL2))
(equal
(EndFn ?INTERVAL1)
(EndFn ?INTERVAL2)))
(equal ?INTERVAL1 ?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 |
(=>
(before
(EndFn ?INTERVAL1)
(BeginFn ?INTERVAL2))
(earlier ?INTERVAL1 ?INTERVAL2)) |
Merge.kif 8584-8586 |
If the end of X happens before the beginning of Y, then X happens earlier than Y |
(=>
(and
(instance ?CHANGE ChangeOfPossession)
(patient ?CHANGE ?OBJ)
(holdsDuring
(BeginFn
(WhenFn ?CHANGE))
(possesses ?AGENT1 ?OBJ))
(holdsDuring
(EndFn
(WhenFn ?CHANGE))
(possesses ?AGENT2 ?OBJ)))
(not
(equal ?AGENT1 ?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 |
(=>
(and
(instance ?A Attaching)
(patient ?A ?O1)
(patient ?A ?O2)
(holdsDuring
(BeginFn
(WhenFn ?A))
(not
(connected ?O1 ?O2)))
(holdsDuring
(EndFn
(WhenFn ?A))
(connected ?O1 ?O2)))
(and
(objectAttached ?A ?O1)
(objectAttached ?A ?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 |
(=>
(and
(instance ?D Detaching)
(patient ?D ?O1)
(patient ?D ?O2)
(holdsDuring
(BeginFn
(WhenFn ?D))
(connected ?O1 ?O2))
(holdsDuring
(EndFn
(WhenFn ?A))
(not
(connected ?O1 ?O2))))
(and
(objectDetached ?A ?O1)
(objectDetached ?A ?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 |
(=>
(and
(patient ?PROCESS ?PATIENT)
(time ?PATIENT
(EndFn
(WhenFn ?PROCESS)))
(not
(time ?PATIENT
(BeginFn
(WhenFn ?PROCESS)))))
(instance ?PROCESS 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 |
(=>
(and
(resourceConsumption ?PROC ?QUANT)
(instance ?QUANT ConstantQuantity)
(resource ?PROC ?RES)
(holdsDuring
(BeginFn
(WhenFn ?PROC))
(measure ?RES
(MeasureFn ?X ?U)))
(holdsDuring
(EndFn
(WhenFn ?PROC))
(measure ?RES
(MeasureFn ?Y ?U))))
(equal ?QUANT
(MeasureFn
(SubtractionFn ?X ?Y) ?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) |
(=>
(and
(resourceConsumption ?PROC ?QUANT)
(instance ?QUANT FunctionQuantity)
(resource ?PROC ?RES)
(equal ?QUANT
(PerFn
(MeasureFn ?Q ?U)
(MeasureFn ?DC ?DU)))
(duration
(WhenFn ?PROC)
(MeasureFn ?T ?DU))
(holdsDuring
(BeginFn
(WhenFn ?PROC))
(measure ?RES
(MeasureFn ?X ?U)))
(holdsDuring
(EndFn
(WhenFn ?PROC))
(measure ?RES
(MeasureFn ?Y ?U))))
(equal ?Y
(MeasureFn
(SubtractionFn ?X
(MultiplicationFn ?T
(DivisionFn ?Q ?DC))) ?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) |
(=>
(and
(equal ?PROCESSSTART
(BeginFn
(WhenFn ?PROCESS)))
(equal ?AGENTEND
(EndFn
(WhenFn ?AGENT)))
(benefits ?PROCESS ?AGENT))
(before ?PROCESSSTART ?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 |
(=>
(and
(equal ?PROCESSSTART
(BeginFn
(WhenFn ?PROCESS)))
(equal ?AGENTEND
(EndFn
(WhenFn ?AGENT)))
(suffers ?PROCESS ?AGENT))
(before ?PROCESSSTART ?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 |
(=>
(and
(instance ?START Starting)
(objectTransferred ?START ?O)
(holdsDuring
(EndFn ?START)
(measure ?O
(MeasureFn ?N MilesPerHour))))
(greaterThan ?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 |
(=>
(and
(instance ?EXPORT Exporting)
(patient ?EXPORT ?ITEM)
(instance ?AREA1 GeopoliticalArea)
(instance ?AREA2 GeopoliticalArea)
(holdsDuring
(BeginFn
(WhenFn ?EXPORT))
(located ?ITEM ?AREA1))
(holdsDuring
(EndFn
(WhenFn ?EXPORT))
(located ?ITEM ?AREA2)))
(not
(located ?AREA2 ?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 |
(=>
(and
(instance ?IMPORT Importing)
(patient ?IMPORT ?ITEM)
(instance ?AREA1 GeopoliticalArea)
(instance ?AREA2 GeopoliticalArea)
(holdsDuring
(BeginFn
(WhenFn ?IMPORT))
(located ?ITEM ?AREA1))
(holdsDuring
(EndFn
(WhenFn ?IMPORT))
(located ?ITEM ?AREA2)))
(not
(located ?AREA2 ?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 |
(=>
(and
(transactionAmount ?Payment ?Amount)
(date ?Payment ?Date)
(instance ?Account FinancialAccount)
(destination ?Payment
(CurrencyFn ?Account))
(amountDue ?Account ?Amount ?DueDate)
(before
(EndFn ?Date)
(BeginFn ?DueDate)))
(instance ?Payment 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 |
(=>
(and
(instance ?CD CertificateOfDeposit)
(maturityDate ?CD ?MaturityDate)
(instance ?Withdrawal Withdrawal)
(origin ?Withdrawal
(CurrencyFn ?CD))
(date ?Withdrawal ?DateOfWithdrawal)
(before
(EndFn ?DateOfWithdrawal)
(BeginFn ?MaturityDate)))
(exists (?Penalty)
(and
(instance ?Penalty Penalty)
(destination ?Penalty
(CurrencyFn ?CD))
(causes ?Withdrawal ?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 |
(=>
(and
(instance ?Option CallOption)
(optionHolder ?Option ?Agent)
(strikePrice ?Option ?Price)
(agreementExpirationDate ?Option ?ExpDate)
(underlier ?Option ?Stocks)
(price ?Stocks ?Price ?Time)
(instance ?Time TimeInterval)
(before
(EndFn ?Time)
(BeginFn ?ExpDate)))
(holdsRight ?Agent
(exists (?Buy)
(and
(instance ?Buy Buying)
(patient ?Buy ?Stocks)
(time ?Buy ?Time)
(measure ?Stocks
(MeasureFn 100 ShareUnit))
(agent ?Buy ?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 |
(=>
(and
(instance ?Option CallOption)
(optionSeller ?Option ?Seller)
(strikePrice ?Option ?Price)
(agreementExpirationDate ?Option ?ExpDate)
(underlier ?Option ?Stocks)
(price ?Stocks ?Price ?Time)
(instance ?Time TimeInterval)
(before
(EndFn ?Time)
(BeginFn ?ExpDate)))
(holdsObligation ?Seller
(exists (?Sell)
(and
(instance ?Sell Selling)
(patient ?Sell ?Stocks)
(time ?Sell ?Time)
(measure ?Stocks
(MeasureFn 100 ShareUnit))
(agent ?Sell ?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 |
Monkey