( ! [V__AMOUNT,V__PERIOD] :
((s__instance(V__AMOUNT,s__CurrencyMeasure) &
s__subclass(V__PERIOD,s__TimeInterval))
=>
(s__currencyExchangePerUSDollar(V__AMOUNT,V__PERIOD)
=>
s__currencyExchangeRateInPeriod(s__UnitedStatesDollar,V__AMOUNT,V__PERIOD))
&
(s__currencyExchangeRateInPeriod(s__UnitedStatesDollar,V__AMOUNT,V__PERIOD)
=>
s__currencyExchangePerUSDollar(V__AMOUNT,V__PERIOD))
)
)
|
Economy.kif 3651-3653 |
A kind of time interval is a currency exchange per US dollar of a currency measure if and only if united states dollar currency exchange rate in period the currency measure for a kind of time interval |
| No TPTP formula. May not be expressible in strict first order. |
Economy.kif 3664-3669 |
A kind of time interval is a currency exchange per US dollar of a currency measure if and only if there exists a time position such that the time position is an instance of a kind of time interval and the currency measure is a currency exchange rate of united states dollar holds during the time position |
( ! [V__Date,V__Balance,V__Account,V__Overdraft] :
((s__instance(V__Date,s__Day) &
s__instance(V__Balance,s__RealNumber) &
s__instance(V__Account,s__FinancialAccount) &
s__instance(V__Overdraft,s__RealNumber))
=>
(s__currentAccountBalance(V__Account,V__Date,s__MeasureFn(V__Balance,s__UnitedStatesDollar))
&
s__lessThan(V__Balance,n__0)
&
(V__Overdraft = s__SubtractionFn(n__0,V__Balance)))
=>
s__overdraft(V__Account,s__MeasureFn(V__Overdraft,s__UnitedStatesDollar),V__Date)
)
)
|
FinancialOntology.kif 732-737 |
|
( ! [V__AGENT,V__R,V__CUST,V__X,V__RM,V__FR,V__PHYS] :
((s__instance(V__AGENT,s__CognitiveAgent) &
s__instance(V__CUST,s__CognitiveAgent) &
s__subclass(V__FR,s__HotelFunctionRoom) &
s__instance(V__FR,s__SetOrClass) &
s__instance(V__PHYS,s__SetOrClass))
=>
(s__freeFunctionRoomAmenity(V__FR,V__PHYS)
&
s__instance(V__RM,V__FR)
&
s__element(V__RM,s__PropertyFn(V__AGENT))
&
s__instance(V__R,s__Renting) &
s__patient(V__R,V__RM)
&
s__destination(V__R,V__CUST)
&
s__instance(V__X,V__PHYS)
&
s__possesses(V__AGENT,V__X)
&
s__customer(V__CUST,V__AGENT)
&
((s__instance(V__X,s__Process) &
(s__agent(V__X,V__CUST)
|
s__experiencer(V__X,V__CUST)))
|
(s__possesses(V__AGENT,V__X)
&
s__instance(V__X,s__Object) &
s__uses(V__CUST,V__X))))
=>
s__price(V__X,s__MeasureFn(n__0,s__UnitedStatesDollar),V__AGENT)
)
)
|
Hotel.kif 814-835 |
|
( ! [V__AGENT,V__CUST,V__X,V__PHYS] :
((s__instance(V__AGENT,s__CognitiveAgent) &
s__instance(V__CUST,s__CognitiveAgent) &
s__instance(V__PHYS,s__SetOrClass))
=>
(s__freePropertyAmenity(V__AGENT,V__PHYS)
&
s__instance(V__X,V__PHYS)
&
s__customer(V__CUST,V__AGENT)
&
((s__instance(V__X,s__Process) &
(s__agent(V__X,V__CUST)
|
s__experiencer(V__X,V__CUST)))
|
(s__possesses(V__AGENT,V__X)
&
s__instance(V__X,s__Object) &
s__uses(V__CUST,V__X))))
=>
s__price(V__X,s__MeasureFn(n__0,s__UnitedStatesDollar),V__AGENT)
)
)
|
Hotel.kif 522-537 |
|
( ! [V__O,V__P,V__R,V__ROOM,V__OBJ,V__GUEST,V__HOTEL] :
((s__instance(V__O,s__Object) &
s__instance(V__R,s__TemporaryResidence) &
s__instance(V__ROOM,s__SetOrClass) &
s__subclass(V__ROOM,s__HotelUnit) &
s__instance(V__OBJ,s__SetOrClass) &
s__instance(V__GUEST,s__Human) &
s__instance(V__HOTEL,s__Agent))
=>
(s__freeRoomAmenity(V__ROOM,V__OBJ)
&
s__subclass(V__OBJ,s__Object) &
s__instance(V__R,V__ROOM)
&
s__stays(V__GUEST,V__R)
&
s__element(V__R,s__PropertyFn(V__HOTEL))
&
s__instance(V__O,V__OBJ)
&
s__located(V__O,V__R)
&
s__instance(V__P,s__Process) &
s__agent(V__P,V__GUEST)
&
(s__patient(V__P,V__O)
|
s__instrument(V__P,V__O)
|
s__resource(V__P,V__O)))
=>
s__price(V__P,s__MeasureFn(n__0,s__UnitedStatesDollar),V__HOTEL)
)
)
|
Hotel.kif 334-349 |
|
( ! [V__P,V__R,V__ROOM,V__S,V__PROC,V__GUEST,V__HOTEL] :
((s__instance(V__P,s__Process) &
s__instance(V__R,s__TemporaryResidence) &
s__instance(V__ROOM,s__SetOrClass) &
s__subclass(V__ROOM,s__HotelUnit) &
s__instance(V__S,s__Process) &
s__instance(V__PROC,s__SetOrClass) &
s__instance(V__GUEST,s__Human) &
s__instance(V__HOTEL,s__Agent))
=>
(s__freeRoomAmenity(V__ROOM,V__PROC)
&
s__subclass(V__PROC,s__Process) &
s__instance(V__R,V__ROOM)
&
s__stays(V__GUEST,V__R)
&
s__element(V__R,s__PropertyFn(V__HOTEL))
&
s__patient(V__P,V__GUEST)
&
(s__instance(V__P,V__PROC)
|
(s__instance(V__S,V__PROC)
&
s__subProcess(V__P,V__S)))
&
s__located(V__P,V__R))
=>
s__price(V__P,s__MeasureFn(n__0,s__UnitedStatesDollar),V__HOTEL)
)
)
|
Hotel.kif 351-365 |
|
| No TPTP formula. May not be expressible in strict first order. |
Economy.kif 440-446 |
|
| No TPTP formula. May not be expressible in strict first order. |
Economy.kif 455-461 |
|
| No TPTP formula. May not be expressible in strict first order. |
Economy.kif 463-469 |
|
| No TPTP formula. May not be expressible in strict first order. |
Economy.kif 478-484 |
|
| No TPTP formula. May not be expressible in strict first order. |
Economy.kif 486-492 |
|
( ! [V__AGENT,V__R,V__CUST,V__PRICE,V__X,V__RM,V__FR,V__PHYS] :
((s__instance(V__AGENT,s__CognitiveAgent) &
s__instance(V__CUST,s__CognitiveAgent) &
s__instance(V__PRICE,s__CurrencyMeasure) &
s__subclass(V__FR,s__HotelFunctionRoom) &
s__instance(V__FR,s__SetOrClass) &
s__instance(V__PHYS,s__SetOrClass))
=>
(s__paidFunctionRoomAmenity(V__FR,V__PHYS)
&
s__instance(V__RM,V__FR)
&
s__element(V__RM,s__PropertyFn(V__AGENT))
&
s__instance(V__R,s__Renting) &
s__patient(V__R,V__RM)
&
s__destination(V__R,V__CUST)
&
s__instance(V__X,V__PHYS)
&
s__possesses(V__AGENT,V__X)
&
s__customer(V__CUST,V__AGENT)
&
((s__instance(V__X,s__Process) &
(s__agent(V__X,V__CUST)
|
s__experiencer(V__X,V__CUST)))
|
(s__possesses(V__AGENT,V__X)
&
s__instance(V__X,s__Object) &
s__uses(V__CUST,V__X))))
=>
(s__price(V__X,V__PRICE,V__AGENT)
&
s__greaterThan(V__PRICE,s__MeasureFn(n__0,s__UnitedStatesDollar)))
)
)
|
Hotel.kif 844-867 |
|
( ! [V__AGENT,V__CUST,V__PRICE,V__X,V__PHYS] :
((s__instance(V__AGENT,s__CognitiveAgent) &
s__instance(V__CUST,s__CognitiveAgent) &
s__instance(V__PRICE,s__CurrencyMeasure) &
s__instance(V__PHYS,s__SetOrClass))
=>
(s__paidPropertyAmenity(V__AGENT,V__PHYS)
&
s__instance(V__X,V__PHYS)
&
s__customer(V__CUST,V__AGENT)
&
((s__instance(V__X,s__Process) &
(s__agent(V__X,V__CUST)
|
s__experiencer(V__X,V__CUST)))
|
(s__possesses(V__AGENT,V__X)
&
s__instance(V__X,s__Object) &
s__uses(V__CUST,V__X))))
=>
(s__price(V__X,V__PRICE,V__AGENT)
&
s__greaterThan(V__PRICE,s__MeasureFn(n__0,s__UnitedStatesDollar)))
)
)
|
Hotel.kif 545-562 |
|
( ! [V__O,V__P,V__R,V__ROOM,V__OBJ,V__PRICE,V__GUEST,V__HOTEL] :
((s__instance(V__O,s__Object) &
s__instance(V__P,s__Process) &
s__instance(V__R,s__TemporaryResidence) &
s__instance(V__ROOM,s__SetOrClass) &
s__subclass(V__ROOM,s__HotelUnit) &
s__instance(V__OBJ,s__SetOrClass) &
s__instance(V__PRICE,s__CurrencyMeasure) &
s__instance(V__GUEST,s__Human) &
s__instance(V__HOTEL,s__Agent))
=>
(s__paidRoomAmenity(V__ROOM,V__OBJ)
&
s__subclass(V__OBJ,s__Object))
=>
(s__instance(V__R,V__ROOM)
&
s__stays(V__GUEST,V__R)
&
s__element(V__R,s__PropertyFn(V__HOTEL))
&
s__instance(V__O,V__OBJ)
&
s__located(V__O,V__R)
&
s__instance(V__P,s__Process) &
s__agent(V__P,V__GUEST)
&
(s__located(V__P,V__O)
|
s__patient(V__P,V__O)
|
s__instrument(V__P,V__O)
|
s__resource(V__P,V__O)))
=>
(s__price(V__P,V__PRICE,V__HOTEL)
&
s__greaterThan(V__PRICE,s__MeasureFn(n__0,s__UnitedStatesDollar)))
)
)
|
Hotel.kif 374-394 |
|
( ! [V__P,V__R,V__ROOM,V__S,V__PRICE,V__PROC,V__GUEST,V__HOTEL] :
((s__instance(V__P,s__Process) &
s__instance(V__R,s__TemporaryResidence) &
s__instance(V__ROOM,s__SetOrClass) &
s__subclass(V__ROOM,s__HotelUnit) &
s__instance(V__S,s__Process) &
s__instance(V__PRICE,s__CurrencyMeasure) &
s__instance(V__PROC,s__SetOrClass) &
s__instance(V__GUEST,s__Human) &
s__instance(V__HOTEL,s__Agent))
=>
(s__paidRoomAmenity(V__ROOM,V__PROC)
&
s__subclass(V__PROC,s__Process))
=>
(s__instance(V__R,V__ROOM)
&
s__stays(V__GUEST,V__R)
&
s__element(V__R,s__PropertyFn(V__HOTEL))
&
s__patient(V__P,V__GUEST)
&
(s__instance(V__P,V__PROC)
|
(s__instance(V__S,V__PROC)
&
s__subProcess(V__P,V__S)))
&
s__located(V__P,V__R))
=>
(s__price(V__P,V__PRICE,V__HOTEL)
&
s__greaterThan(V__PRICE,s__MeasureFn(n__0,s__UnitedStatesDollar)))
)
)
|
Hotel.kif 396-414 |
|
( ! [V__N1,V__Time,V__N2,V__N3,V__TimeOfSplit,V__NewNumber,V__Stocks,V__TimeAfterSplit,V__Number] :
((s__instance(V__N1,s__Integer) &
s__instance(V__Time,s__Agent) &
s__instance(V__Time,s__TimeInterval) &
s__instance(V__N2,s__Integer) &
s__instance(V__N3,s__Quantity) &
s__instance(V__TimeOfSplit,s__TimeInterval) &
s__instance(V__NewNumber,s__RealNumber) &
s__instance(V__Stocks,s__Physical) &
s__instance(V__TimeAfterSplit,s__Agent) &
s__instance(V__TimeAfterSplit,s__TimeInterval) &
s__instance(V__Number,s__RealNumber))
=>
(s__price(V__Stocks,s__MeasureFn(V__Number,s__UnitedStatesDollar),V__Time)
&
( ? [V__Event] :
((s__instance(V__Event,s__StockSplit) &
(s__splitFor(V__Event,V__N1,V__N2)
&
(s__WhenFn(V__Event)
= V__TimeOfSplit))))))
=>
((V__N3 = s__MultiplicationFn(V__Number,V__N1))
&
(V__NewNumber = s__DivisionFn(V__N3,V__N2))
&
s__price(V__Stocks,s__MeasureFn(V__NewNumber,s__UnitedStatesDollar),V__TimeAfterSplit)
&
s__meetsTemporally(V__Time,V__TimeOfSplit)
&
s__meetsTemporally(V__TimeOfSplit,V__TimeAfterSplit))
)
)
|
FinancialOntology.kif 2172-2184 |
|
