(=>
(and
(holdsDuring ?T2 ?SIT2)
(holdsDuring ?T1 ?SIT1)
(instance ?T1 TimeInterval)
(instance ?T2 TimeInterval)
(causesProposition ?SIT1 ?SIT2))
(beforeOrEqual
(BeginFn ?T1)
(BeginFn ?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 |
(=>
(instance ?OBJ Object)
(exists (?TIME1 ?TIME2)
(and
(instance ?TIME1 TimePoint)
(instance ?TIME2 TimePoint)
(before ?TIME1 ?TIME2)
(forall (?TIME)
(=>
(and
(beforeOrEqual ?TIME1 ?TIME)
(beforeOrEqual ?TIME ?TIME2))
(time ?OBJ ?TIME)))))) |
Merge.kif 8312-8324 |
If X is an instance of object, then there exist Y, Z such that Y is an instance of time point, Z is an instance of time point, Y happens before Z, W Y happens before, at W, and W happens before, or at ZX exists during W |
(=>
(or
(before ?POINT1 ?POINT2)
(equal ?POINT1 ?POINT2))
(beforeOrEqual ?POINT1 ?POINT2)) |
Merge.kif 8353-8357 |
If X happens before Y or equal X and Y, then X happens before or at Y |
(=>
(temporallyBetweenOrEqual ?POINT1 ?POINT2 ?POINT3)
(and
(beforeOrEqual ?POINT1 ?POINT2)
(beforeOrEqual ?POINT2 ?POINT3))) |
Merge.kif 8396-8400 |
If X is between or at Y and Z, then Y happens before or at X and X happens before or at Z |
(=>
(and
(firstInstanceCreated ?C ?T)
(instance ?I ?C))
(beforeOrEqual ?T
(BeginFn
(WhenFn ?I)))) |
Mid-level-ontology.kif 33312-33318 |
If X was firstInstanceCreated at Y and Z is an instance of X, then Y happens before or at the beginning of the time of existence of Z |
(=>
(and
(amountDue ?Account ?Amount ?DueDate)
(accountHolder ?Account ?Agent))
(holdsObligation ?Agent
(exists (?Payment)
(and
(instance ?Payment Payment)
(transactionAmount ?Payment ?Amount)
(or
(destination ?Payment
(CurrencyFn ?Account))
(origin ?Payment
(CurrencyFn ?Account)))
(date ?Payment ?Date)
(beforeOrEqual
(EndFn ?Date)
(BeginFn ?DueDate)))))) |
FinancialOntology.kif 676-689 |
If X amount due Y for Z and W holds account X, then W is obliged to perform tasks of type there exists V such that V is an instance of payment, Y is a transaction amount of V, V ends up at the currency of X, V originates at the currency of X, date of V is U, and the end of U happens before, or at the beginning of Z |
