(=>
(confersRight ?AGENT1 ?AGENT2 ?FORMULA)
(holdsRight ?AGENT2 ?FORMULA)) |
Merge.kif 17790-17792 |
If X allows Y to perform task of the type Z, then X has the right to perform %3 |
(=>
(agreementClause ?PROP Prohibition ?AGREEMENT ?AGENT)
(not
(holdsRight ?AGENT
(exists (?PROC)
(and
(realization ?PROC ?PROP)
(agent ?PROC ?AGENT)))))) |
Mid-level-ontology.kif 15692-15699 |
If X has the responsibility to make Y prohibition in Z, then X doesn't have the right to perform %3 |
(=>
(agreementClause ?PROP Permission ?AGREEMENT ?AGENT)
(holdsRight ?AGENT
(exists (?PROC)
(and
(realization ?PROC ?PROP)
(agent ?PROC ?AGENT))))) |
Mid-level-ontology.kif 15701-15707 |
If X has the responsibility to make Y permission in Z, then X has the right to perform %3 |
(=>
(instance ?JURY Jury)
(holdsRight ?JURY
(exists (?DECISION)
(and
(instance ?DECISION LegalDecision)
(agent ?DECISION ?JURY))))) |
Mid-level-ontology.kif 17696-17702 |
If X is an instance of jury, then X has the right to perform %3 |
(=>
(instance ?ESCAPE Escaping)
(holdsDuring
(ImmediateFutureFn
(WhenFn ?ESCAPE))
(not
(exists (?AGENT)
(holdsRight ?AGENT
(agent ?ESCAPE ?AGENT)))))) |
Mid-level-ontology.kif 19054-19061 |
If X is an instance of escaping, then there doesn't exist Y such that Y has the right to perform holds during immediately after the time of existence of X |
(=>
(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 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 AmericanStyleOption)
(optionHolder ?Option ?Agent)
(agreementExpirationDate ?Option ?Day))
(holdsRight ?Agent
(exists (?Exercise)
(and
(instance ?Exercise ExerciseAnOption)
(patient ?Exercise ?Option)
(before
(EndFn
(WhenFn ?Exercise))
(EndFn ?Day)))))) |
FinancialOntology.kif 2811-2823 |
If X is an instance of american style option, Y holds X, and X has expiration Z, then Y has the right to perform %3 |
(=>
(and
(agreementEffectiveDate ?AGR ?DATE)
(confersRight ?AGR ?AGENT ?FORMULA)
(instance ?TIME ?DATE))
(holdsDuring
(ImmediateFutureFn ?TIME)
(holdsRight ?AGENT ?FORMULA))) |
Government.kif 686-693 |
If X is an agreement effective date of Y, Z allows W to perform task of the type Y, and V is an instance of X, then Z has the right to perform holds during immediately after V |
(=>
(and
(instance ?TA_CTRL TerminalGuidance)
(agent ?TA_CTRL ?AGENT)
(patient ?TA_CTRL ?TARGET))
(not
(holdsRight ?AGENT
(exists (?ATTACK)
(and
(instance ?ATTACK Attack)
(agent ?ATTACK ?AGENT)
(patient ?ATTACK ?TARGET)))))) |
MilitaryProcesses.kif 539-550 |
If ?TA_CTRL is an instance of terminal guidance, Y is an agent of ?TA_CTRL, and Z is a patient of ?TA_CTRL, then Y doesn't have the right to perform %3 |
(=>
(and
(policyEffectiveDate ?POL ?DATE)
(confersRight ?POL ?AGENT ?FORMULA)
(instance ?TIME ?DATE))
(holdsDuring
(ImmediateFutureFn ?TIME)
(holdsRight ?AGENT ?FORMULA))) |
TravelPolicies.kif 197-202 |
If policyEffectiveDate X and Y, Z allows W to perform task of the type X, and V is an instance of Y, then Z has the right to perform holds during immediately after V |
holdsRight