(=>
(bidPrice ?Obj ?Money ?Agent)
(exists (?Offering)
(and
(instance ?Offering Offering)
(containsFormula ?Offering
(exists (?Buying)
(and
(instance ?Buying Buying)
(agent ?Buying ?Agent)
(patient ?Buying ?Obj)
(transactionAmount ?Buying ?Money))))))) |
FinancialOntology.kif 1958-1969 |
If X bids Y for Z, then there exists W such that W is an instance of offering, W contains the formula there exists V such that V is an instance of buying, X is an agent of V, Z is a patient of V, and Y is a transaction amount of V |
(=>
(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 ?AUCTIONING Auctioning)
(instance ?BIDDER1 AutonomousAgent)
(instance ?BIDDER2 AutonomousAgent)
(instance ?ITEM Object)
(instance ?U UnitOfCurrency)
(patient ?AUCTIONING ?ITEM)
(bidPrice ?ITEM
(MeasureFn ?OFFER1 ?U) ?BIDDER1)
(bidPrice ?ITEM
(MeasureFn ?OFFER2 ?U) ?BIDDER2)
(greaterThan ?OFFER1 ?OFFER2))
(destination ?AUCTIONING ?BIDDER1)) |
UXExperimentalTerms.kif 354-365 |
If All of the following hold: (1) X is an instance of auctioning (2) Y is an instance of agent (3) Z is an instance of agent (4) W is an instance of object (5) V is an instance of unit of currency (6) W is a patient of X (7) Y bids U V(s) for W (8) Z bids T V(s) for W (9) U is greater than T, then X ends up at Y |
(=>
(bidPrice ?OBJECT ?AMOUNT ?AGENT)
(exists (?BIDDING)
(and
(instance ?BIDDING Bidding)
(objectOfBid ?BIDDING ?OBJECT)
(amountOfBid ?BIDDING ?AMOUNT)
(agent ?BIDDING ?AGENT)))) |
UXExperimentalTerms.kif 1407-1414 |
If X bids Y for Z, then there exists W such that W is an instance of bidding, W is a bid for Z, Y is the bid of W, and X is an agent of W |