(=>
(instance ?PHYS Physical)
(exists (?LOC ?TIME)
(and
(located ?PHYS ?LOC)
(time ?PHYS ?TIME)))) |
Merge.kif 831-836 |
If X is an instance of physical, then there exist Y, Z such that X is located at Y, and X exists during Z |
(=>
(and
(holdsDuring ?INTERVAL
(?REL ?INST1 ?INST2))
(instance ?INST1 Physical)
(instance ?INST2 Physical))
(and
(time ?INST1 ?INTERVAL)
(time ?INST2 ?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 |
(=>
(temporalPart ?POS
(WhenFn ?THING))
(time ?THING ?POS)) |
Merge.kif 8143-8146 |
If X is a part of the time of existence of Y, then Y exists during X |
(=>
(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 |
(=>
(result ?PROC ?OBJ)
(forall (?TIME)
(=>
(before ?TIME
(BeginFn
(WhenFn ?PROC)))
(not
(time ?OBJ ?TIME))))) |
Merge.kif 8326-8332 |
If X is a result of Y, then For all TimePoint Z: if Z happens before the beginning of the time of existence of Y, then X doesn't exist during Z |
(=>
(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 |
(=>
(instance ?PROCESS Destruction)
(exists (?PATIENT)
(and
(patient ?PROCESS ?PATIENT)
(time ?PATIENT
(BeginFn
(WhenFn ?PROCESS)))
(not
(time ?PATIENT
(EndFn
(WhenFn ?PROCESS))))))) |
Merge.kif 12568-12575 |
If X is an instance of destruction, then there exists Y such that Y is a patient of X, Y exists during the beginning of the time of existence of X, and Y doesn't exist during the end of the time of existence of X |
(=>
(instance ?PROCESS Creation)
(exists (?PATIENT)
(and
(patient ?PROCESS ?PATIENT)
(time ?PATIENT
(EndFn
(WhenFn ?PROCESS)))
(not
(time ?PATIENT
(BeginFn
(WhenFn ?PROCESS))))))) |
Merge.kif 13085-13092 |
If X is an instance of creation, then there exists Y such that Y is a patient of X, Y exists during the end of the time of existence of X, and Y doesn't exist during the beginning of the time of existence of X |
(=>
(and
(instance ?O OccupationalRole)
(typicalAction ?PCLASS
(AttrFn CognitiveAgent ?O)))
(exists (?X ?T ?P ?PT)
(and
(instance ?X CognitiveAgent)
(holdsDuring ?T
(attribute ?X ?O))
(instance ?P ?PCLASS)
(agent ?X ?P)
(time ?P ?PT)
(temporalPart ?PT ?T)))) |
Mid-level-ontology.kif 24538-24551 |
If X is an instance of occupational role and Y is a typical action of a the attr of cognitive agent and X, then All of the following hold: (1) there exist Z, W,, , V (2) U such that Z is an instance of cognitive agent (3) X is an attribute of Z holds during W (4) V is an instance of Y (5) V is an agent of Z (6) V exists during U (7) U is a part of W |
(=>
(playsRoleInEventOfType ?OBJ ?ROLE ?TYPE ?TIME ?PLACE)
(exists (?EVENT)
(and
(instance ?EVENT ?TYPE)
(time ?EVENT ?TIME)
(eventLocated ?EVENT ?PLACE)
(playsRoleInEvent ?OBJ ?ROLE ?EVENT)))) |
Mid-level-ontology.kif 25598-25605 |
If X plays role in event of type Y for Z with W and V, then there exists U such that U is an instance of Z, U exists during W, U is located at V, and X plays role in event Y for U |
(=>
(and
(instance ?IMPRISON Imprisoning)
(detainee ?IMPRISON ?AGENT)
(instance ?AGENT Human)
(time ?IMPRISON ?INTERVAL)
(instance ?INTERVAL TimeInterval))
(exists (?ARREST ?TIME)
(and
(instance ?TIME TimeInterval)
(time ?ARREST ?TIME)
(earlier ?TIME ?INTERVAL)
(instance ?ARREST PlacingUnderArrest)
(arrested ?ARREST ?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 |
(=>
(instance ?OPEN OpeningNewGraphicalWindow)
(exists (?WINDOW)
(and
(patient ?OPEN ?WINDOW)
(instance ?WINDOW InterfaceWindow)
(time ?WINDOW
(EndFn
(WhenFn ?OPEN)))
(not
(time ?WINDOW
(BeginFn
(WhenFn ?OPEN))))))) |
ComputerInput.kif 2389-2396 |
If X is an instance of opening new graphical window, then there exists Y such that Y is a patient of X, Y is an instance of interface window, Y exists during the end of the time of existence of X, and Y doesn't exist during the beginning of the time of existence of X |
(=>
(and
(instance ?CLOSE ClosingGraphicalWindow)
(patient ?CLOSE ?WINDOW))
(and
(instance ?WINDOW InterfaceWindow)
(time ?WINDOW
(BeginFn
(WhenFn ?OPEN)))
(not
(time ?WINDOW
(EndFn
(WhenFn ?OPEN)))))) |
ComputerInput.kif 2454-2461 |
If X is an instance of closing graphical window and Y is a patient of X, then Y is an instance of interface window, Y exists during the beginning of the time of existence of Z, and Y doesn't exist during the end of the time of existence of Z |
(=>
(and
(instance ?Check Check)
(instance ?Processing ProcessingACheck)
(patient ?Processing ?Check))
(exists (?Depositing)
(and
(instance ?Depositing DepositingACheck)
(patient ?Depositing ?Check)
(time ?Depositing
(ImmediatePastFn
(WhenFn ?Processing)))))) |
FinancialOntology.kif 139-148 |
If X is an instance of check, Y is an instance of processing a check, and X is a patient of Y, then there exists Z such that Z is an instance of depositing a check, X is a patient of Z, and Z exists during immediately before the time of existence of Y |
(=>
(and
(instance ?Loan CallableLoan)
(lender ?Loan ?Lender)
(borrower ?Loan ?Borrower)
(totalBalance ?Loan ?Amount)
(instance ?Call Call)
(agent ?Call ?Lender)
(patient ?Call ?Loan))
(holdsObligation ?Borrower
(exists (?Payment)
(and
(destination ?Payment ?Lender)
(time ?Payment
(ImmediateFutureFn
(WhenFn ?Call)))
(transactionAmount ?Payment ?Amount))))) |
FinancialOntology.kif 1469-1485 |
If All of the following hold: (1) X is an instance of callable loan (2) Y lends X (3) X is the borrower of Z (4) W is a total balance of X (5) V is an instance of call (6) Y is an agent of V (7) X is a patient of V, then Z is obliged to perform tasks of type there exists U such that U ends up at Y, U exists during immediately after the time of existence of V, and W is a transaction amount of U |
(=>
(and
(instance ?Refinancing Refinancing)
(time ?Refinancing ?Time)
(instance ?Loan Loan)
(securedBy ?Loan ?Collateral)
(borrower ?Loan ?Borrower)
(currentAccountBalance ?Loan ?Time ?Amount)
(patient ?Refinancing ?Loan))
(exists (?NewLoan ?Payment)
(and
(instance ?NewLoan Loan)
(borrower ?NewLoan ?Borrower)
(securedBy ?Loan ?Collateral)
(destination ?Payment
(CurrencyFn ?Loan))
(time ?Payment ?Time)
(origin ?Payment
(CurrencyFn ?NewLoan))
(transactionAmount ?Payment ?Amount)))) |
FinancialOntology.kif 1491-1508 |
If All of the following hold: (1) X is an instance of refinancing (2) X exists during Y (3) Z is an instance of loan (4) W is a secured by of Z (5) Z is the borrower of V (6) Z current account balance Y for U (7) Z is a patient of X, then All of the following hold: (1) there exist T (2) S such that T is an instance of loan (3) T is the borrower of V (4) W is a secured by of Z (5) S ends up at the currency of Z (6) S exists during Y (7) S originates at the currency of T (8) U is a transaction amount of S |
(=>
(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 |
(=>
(and
(instance ?Option PutOption)
(optionHolder ?Option ?Agent)
(strikePrice ?Option ?Price)
(agreementExpirationDate ?Option ?ExpDate)
(price ?Stocks ?Price ?Time)
(instance ?Time TimeInterval)
(before
(EndFn ?Time)
(BeginFn ?ExpDate))
(underlier ?Option ?Stocks))
(holdsRight ?Agent
(exists (?Sell)
(and
(instance ?Sell Selling)
(patient ?Sell ?Stocks)
(time ?Sell ?Time)
(measure ?Stocks
(MeasureFn 100 ShareUnit))
(agent ?Sell ?Agent))))) |
FinancialOntology.kif 2697-2714 |
If All of the following hold: (1) X is an instance of put option (2) Y holds X (3) Z is a strike price of X (4) X has expiration W (5) V is price Z for U (6) U is an instance of timeframe (7) the end of U happens before the beginning of W (8) V is an underlier of X, then Y has the right to perform %3 |
(=>
(and
(instance ?Option PutOption)
(optionSeller ?Option ?Agent)
(strikePrice ?Option ?Price)
(agreementExpirationDate ?Option ?ExpDate)
(price ?Stocks ?Price ?Time)
(instance ?Time TimeInterval)
(before
(EndFn ?Time)
(BeginFn ?ExpDate))
(underlier ?Option ?Stocks))
(holdsObligation ?Agent
(exists (?Buy)
(and
(instance ?Buy Buying)
(patient ?Buy ?Stocks)
(time ?Buy ?Time)
(measure ?Stocks
(MeasureFn 100 ShareUnit))
(agent ?Buy ?Agent))))) |
FinancialOntology.kif 2716-2734 |
If All of the following hold: (1) X is an instance of put option (2) Y sells X (3) Z is a strike price of X (4) X has expiration W (5) V is price Z for U (6) U is an instance of timeframe (7) the end of U happens before the beginning of W (8) V is an underlier of X, then Y is obliged to perform tasks of type there exists T such that T is an instance of buying and V is a patient of T and T exists during U and the measure of V is 100 share unit(s) and Y is an agent of T |
(=>
(and
(instance ?Exercise ExerciseAnOption)
(patient ?Exercise ?Option)
(property ?Option CallOption)
(time ?Exercise ?Time)
(underlier ?Option ?Stocks))
(exists (?Buy)
(and
(instance ?Buy Buying)
(patient ?Buy ?Stocks)
(time ?Buy ?Time)
(measure ?Stocks
(MeasureFn 100 ShareUnit))))) |
FinancialOntology.kif 2779-2791 |
If X is an instance of exercise an option, Y is a patient of X, Y the attribute call option, X exists during Z, and W is an underlier of Y, then there exists V such that V is an instance of buying and W is a patient of V and V exists during Z and the measure of W is 100 share unit(s) |
(=>
(and
(instance ?Exercise ExerciseAnOption)
(patient ?Exercise ?Option)
(property ?Option PutOption)
(time ?Exercise ?Time)
(underlier ?Option ?Stocks))
(exists (?Sell)
(and
(instance ?Sell Selling)
(patient ?Sell ?Stocks)
(time ?Sell ?Time)
(measure ?Stocks
(MeasureFn 100 ShareUnit))))) |
FinancialOntology.kif 2793-2805 |
If X is an instance of exercise an option, Y is a patient of X, Y the attribute put option, X exists during Z, and W is an underlier of Y, then there exists V such that V is an instance of selling and W is a patient of V and V exists during Z and the measure of W is 100 share unit(s) |
(=>
(instance ?Spread SpreadOption)
(exists (?Option1 ?Option2 ?Buy ?Sell ?Time)
(and
(instance ?Option1 Option)
(instance ?Option2 Option)
(instance ?Buy Buying)
(instance ?Sell Selling)
(subProcess ?Buy ?Spread)
(subProcess ?Sell ?Spread)
(patient ?Buy ?Option1)
(patient ?Sell ?Option2)
(time ?Buy ?Time)
(time ?Sell ?Time)))) |
FinancialOntology.kif 3154-3167 |
If X is an instance of spread option, then All of the following hold: (1) there exist Y, Z,, , W,, , V (2) U such that Y is an instance of option (3) Z is an instance of option (4) W is an instance of buying (5) V is an instance of selling (6) W is a subprocess of X (7) V is a subprocess of X (8) Y is a patient of W (9) Z is a patient of V (10) W exists during U (11) V exists during U |
(=>
(and
(taxDeferredIncome ?Agent ?Income ?Activity)
(time ?Activity ?Time))
(not
(exists (?Tax)
(and
(instance ?Tax Tax)
(causes ?Activity ?Tax)
(time ?Tax ?Time))))) |
FinancialOntology.kif 3369-3378 |
If tax deferred income for X resulting from Y is Z and Y exists during W, then there doesn't exist V such that V is an instance of tax, Y causes V, and V exists during W |
(=>
(agreementAdoptionDate ?AGR ?DATE)
(exists (?PROCESS ?DAY)
(and
(instance ?PROCESS Committing)
(instance ?DAY ?DATE)
(patient ?PROCESS ?AGR)
(time ?PROCESS ?DAY)))) |
Government.kif 669-676 |
If X is an agreement adoption date of Y, then there exist Z, W such that Z is an instance of committing, W is an instance of X, Y is a patient of Z, and Z exists during W |
|
| Display limited to 25 items. Show next 25 |
|
| Display limited to 25 items. Show next 25 |
time