(=>
(confersObligation ?AGENT1 ?AGENT2 ?FORMULA)
(holdsObligation ?AGENT2 ?FORMULA)) |
Merge.kif 17812-17814 |
If X obligates Y to perform task of the type Z, then X is obliged to perform tasks of type Y |
(=>
(and
(instance ?UNIT SecurityUnit)
(subOrganization ?UNIT ?ORG))
(holdsObligation ?UNIT
(exists (?MAINTAIN)
(and
(instance ?MAINTAIN Maintaining)
(agent ?MAINTAIN ?UNIT)
(patient ?MAINTAIN ?ORG))))) |
Mid-level-ontology.kif 9886-9895 |
If X is an instance of security unit and X is a part of the organization Y, then X is obliged to perform tasks of type there exists Z such that Z is an instance of maintaining, X is an agent of Z, and Y is a patient 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 |
(=>
(and
(instance ?Account CreditAccount)
(accountHolder ?Account ?Agent)
(principalAmount ?Account ?Principal)
(agreementPeriod ?Account ?Period)
(interestEarned ?Account ?Interest ?Period)
(equal ?Total
(AdditionFn ?Principal ?Interest)))
(holdsObligation ?Agent
(exists (?Payment)
(transactionAmount ?Payment ?Total)))) |
FinancialOntology.kif 1261-1271 |
If All of the following hold: (1) X is an instance of credit account (2) Y holds account X (3) Z is a principal amount of X (4) W is an agreement period of X (5) X is interest earned V for W (6) equal U and (Z and V), then Y is obliged to perform tasks of type there exists T such that U is a transaction amount of T |
(=>
(and
(instance ?Account Loan)
(borrower ?Account ?Agent)
(principalAmount ?Account ?Principal)
(agreementPeriod ?Account ?Period)
(interestEarned ?Account ?Interest ?Period)
(equal ?Total
(AdditionFn ?Principal ?Interest)))
(holdsObligation ?Agent
(exists (?Payment)
(transactionAmount ?Payment ?Total)))) |
FinancialOntology.kif 1311-1321 |
If All of the following hold: (1) X is an instance of loan (2) X is the borrower of Y (3) Z is a principal amount of X (4) W is an agreement period of X (5) X is interest earned V for W (6) equal U and (Z and V), then Y is obliged to perform tasks of type there exists T such that U is a transaction amount of T |
(=>
(and
(instance ?Loan BalloonLoan)
(maturityDate ?Loan ?Date)
(totalBalance ?Loan ?Amount)
(borrower ?Loan ?Agent))
(holdsObligation ?Agent
(exists (?Payment)
(and
(date ?Payment ?Date)
(transactionAmount ?Payment ?Amount)
(destination ?Payment
(CurrencyFn ?Loan)))))) |
FinancialOntology.kif 1451-1462 |
If X is an instance of balloon loan, Y is a maturity date of X, Z is a total balance of X, and X is the borrower of W, then W is obliged to perform tasks of type there exists V such that date of V is Y, Z is a transaction amount of V, and V ends up at the currency of X |
(=>
(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 ?Order MarketOrder)
(attribute ?Broker Broker)
(partyToAgreement ?Order ?Broker)
(orderFor ?Order ?TransactionType ?Shares))
(holdsObligation ?Broker
(exists (?Transaction)
(and
(instance ?Transaction ?TransactionType)
(patient ?Transaction ?Shares))))) |
FinancialOntology.kif 2029-2039 |
If X is an instance of market order, broker is an attribute of Y, Y is a party to agreement of X, and X is order for Z for W, then Y is obliged to perform tasks of type there exists V such that V is an instance of Z and W is a patient of V |
(=>
(and
(instance ?Order LimitOrder)
(partyToAgreement ?Order ?Broker)
(attribute ?Broker Broker)
(orderFor ?Order Buying ?Object)
(measure ?Object ?Quantity)
(limitPrice ?Order
(MeasureFn ?LimitPrice ?U))
(instance ?U UnitOfCurrency)
(askPrice ?Object
(MeasureFn ?Price ?U) ?Time)
(lessThanOrEqualTo ?Price ?LimitPrice))
(holdsObligation ?Broker
(exists (?Buy)
(and
(instance ?Buy Buying)
(patient ?Buy ?Object)
(measure ?Object ?Quantity)
(equal
(WhenFn ?Buy) ?BuyingTime)
(overlapsTemporally ?Time ?BuyingTime))))) |
FinancialOntology.kif 2057-2077 |
If All of the following hold: (1) X is an instance of limit order (2) Y is a party to agreement of X (3) broker is an attribute of Y (4) X is order for buying for Z (5) the measure of Z is W (6) V U(s) is a limit price of X (7) U is an instance of unit of currency (8) T asks for S U(s) for Z (9) S is less than or equal to V, then Y is obliged to perform tasks of type there exists R such that R is an instance of buying, Z is a patient of R, the measure of Z is W, equal the time of existence of R, Q, and Q overlaps T |
(=>
(and
(attribute ?Order LimitOrder)
(partyToAgreement ?Order ?Broker)
(attribute ?Broker Broker)
(orderFor ?Order Selling ?Object)
(measure ?Object ?Quantity)
(limitPrice ?Order
(MeasureFn ?LimitPrice ?U))
(bidPrice ?Object
(MeasureFn ?Price ?U) ?Time)
(instance ?U UnitOfCurrency)
(greaterThanOrEqualTo ?Price ?LimitPrice))
(holdsObligation ?Broker
(exists (?Sell)
(and
(instance ?Sell Selling)
(patient ?Sell ?Object)
(measure ?Object ?Quantity)
(equal
(WhenFn ?Sell) ?SellingTime)
(overlapsTemporally ?SellingTime ?Time))))) |
FinancialOntology.kif 2079-2099 |
If All of the following hold: (1) limit order is an attribute of X (2) Y is a party to agreement of X (3) broker is an attribute of Y (4) X is order for selling for Z (5) the measure of Z is W (6) V U(s) is a limit price of X (7) T bids S U(s) for Z (8) U is an instance of unit of currency (9) S is greater than or equal to V, then Y is obliged to perform tasks of type there exists R such that R is an instance of selling, Z is a patient of R, the measure of Z is W, equal the time of existence of R, Q, and T overlaps Q |
(=>
(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)
(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
(agreementEffectiveDate ?AGR ?DATE)
(confersObligation ?AGR ?AGENT ?FORMULA)
(instance ?TIME ?DATE))
(holdsDuring
(ImmediateFutureFn ?TIME)
(holdsObligation ?AGENT ?FORMULA))) |
Government.kif 677-684 |
If X is an agreement effective date of Y, Z obligates W to perform task of the type Y, and V is an instance of X, then Z is obliged to perform tasks of type W holds during immediately after V |
(=>
(and
(instance ?CONST
(ConstitutionFn ?COUNTRY))
(instance ?COUNTRY Nation)
(equal ?GOV
(GovernmentFn ?COUNTRY))
(instance
(WhenFn ?GOV) ?CLASS)
(agreementEffectiveDuring ?CONST ?CLASS)
(subProposition ?PART ?CONST)
(containsFormula ?PART ?FORMULA))
(holdsObligation ?GOV ?FORMULA)) |
Government.kif 745-754 |
If All of the following hold: (1) X is an instance of the constitution of Y (2) Y is an instance of nation (3) equal Z and the government of Y (4) the time of existence of Z is an instance of W (5) W is an agreement effective during of X (6) V is a sub-proposition of X (7) V contains the formula U, then Z is obliged to perform tasks of type U |
(=>
(and
(instance ?B Bleeding)
(instance ?D Death)
(instance ?H Human)
(instance ?P Human)
(experiencer ?B ?P)
(orientation ?H ?P Near)
(modalAttribute
(causes ?B ?D) Likely))
(holdsObligation ?H
(exists (?A)
(and
(instance ?A ApplyingTourniquet)
(agent ?A ?H)
(destination ?A ?P))))) |
Medicine.kif 45-60 |
If All of the following hold: (1) X is an instance of bleeding (2) Y is an instance of death (3) Z is an instance of human (4) W is an instance of human (5) W experiences X (6) Z is near to W (7) the statement X causes Y has the modal force of likely, then Z is obliged to perform tasks of type there exists V such that V is an instance of applying a tourniquet, Z is an agent of V, and V ends up at W |
(=>
(and
(policyEffectiveDate ?POL ?DATE)
(confersObligation ?POL ?AGENT ?FORMULA)
(instance ?TIME ?DATE))
(holdsDuring
(ImmediateFutureFn ?TIME)
(holdsObligation ?AGENT ?FORMULA))) |
TravelPolicies.kif 190-195 |
If policyEffectiveDate X and Y, Z obligates W to perform task of the type X, and V is an instance of Y, then Z is obliged to perform tasks of type W holds during immediately after V |
holdsObligation