( ! [V__Agent,V__Account,V__Asset] :
(((s__instance(V__Agent,s__CognitiveAgent) &
s__instance(V__Asset,s__FinancialAsset) &
s__instance(V__Asset,s__Object))
=>
((((s__instance(V__Account,s__FinancialAccount) &
s__possesses(V__Agent,V__Asset)
&
(V__Account = s__AccountFn(V__Asset)))
=>
s__accountHolder(V__Account,V__Agent))
&
(s__accountHolder(V__Account,V__Agent)
=>
(s__instance(V__Account,s__FinancialAccount) &
s__possesses(V__Agent,V__Asset)
&
(V__Account = s__AccountFn(V__Asset)))))))
)
)
|
FinancialOntology.kif 2270-2275 |
A financial account is an instance of financial account and a cognitive agent possesses a financial asset and the financial account is equal to the account of the financial asset if and only if the cognitive agent holds account the financial account |
( ! [V__AGENT,V__CUST,V__X,V__LUGGAGE] :
(((s__instance(V__AGENT,s__CognitiveAgent) &
s__instance(V__CUST,s__CognitiveAgent) &
s__instance(V__X,s__CognitiveAgent))
=>
(((s__customer(V__CUST,V__AGENT)
&
s__employs(V__AGENT,V__X)
&
s__attribute(V__AGENT,s__TravelerAccommodation) &
s__attribute(V__X,s__Porter) &
s__possesses(V__CUST,V__LUGGAGE)
&
s__instance(V__LUGGAGE,s__TravelContainer))
=>
(( ? [V__ROOM, V__CARRY] :
((s__instance(V__ROOM,s__HotelUnit) &
s__instance(V__CARRY,s__Carrying) &
s__agent(V__CARRY,V__X)
&
(s__destination(V__CARRY,V__ROOM)
|
s__origin(V__CARRY,V__ROOM)))))))))
)
)
|
Hotel.kif 2352-2367 |
|
( ! [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__Class) &
s__instance(V__PHYS,s__Class))
=>
(((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 820-841 |
|
( ! [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__Class))
=>
(((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 526-541 |
|
| No TPTP formula. May not be expressible in strict first order. |
ComputingBrands.kif 4398-4415 |
|
| No TPTP formula. May not be expressible in strict first order. |
Merge.kif 4112-4118 |
|
| No TPTP formula. May not be expressible in strict first order. |
Transportation.kif 3195-3205 |
|
( ! [V__BondHolder,V__Bond,V__Interest] :
(((s__instance(V__BondHolder,s__Agent) &
s__instance(V__Interest,s__Interest))
=>
(((s__instance(V__Bond,s__Bond) &
s__couponInterest(V__Bond,V__Interest)
&
s__possesses(V__BondHolder,V__Bond))
=>
(( ? [V__Period, V__Payment] :
((s__instance(V__Period,s__TimeDuration) &
s__instance(V__Payment,s__Process) &
(s__periodicPayment(s__AccountFn(V__Bond)
,V__Interest,V__Period)
&
s__destination(V__Payment,V__BondHolder)))))))))
)
)
|
FinancialOntology.kif 2219-2227 |
|
| No TPTP formula. May not be expressible in strict first order. |
FinancialOntology.kif 2338-2347 |
|
( ! [V__Period,V__Total,V__BondHolder,V__Date,V__Bond,V__Interest,V__Principal] :
(((s__instance(V__Period,s__TimeInterval) &
s__instance(V__Total,s__Number) &
s__instance(V__Total,s__CurrencyMeasure) &
s__instance(V__BondHolder,s__Agent) &
s__instance(V__Date,s__Day) &
s__instance(V__Interest,s__Interest) &
s__instance(V__Interest,s__Number) &
s__instance(V__Principal,s__Number) &
s__instance(V__Principal,s__CurrencyMeasure))
=>
(((s__instance(V__Bond,s__ZeroCouponBond) &
s__maturityDate(s__AccountFn(V__Bond)
,V__Date)
&
s__possesses(V__BondHolder,V__Bond)
&
s__principalAmount(s__AccountFn(V__Bond)
,V__Principal)
&
s__agreementPeriod(s__AccountFn(V__Bond)
,V__Period)
&
s__interestEarned(s__AccountFn(V__Bond)
,V__Interest,V__Period)
&
(V__Total = s__AdditionFn(V__Principal,V__Interest)))
=>
(( ? [V__Payment] :
((s__instance(V__Payment,s__Payment) &
s__destination(V__Payment,V__BondHolder)
&
s__origin(V__Payment,s__AccountFn(V__Bond))
&
s__transactionAmount(V__Payment,V__Total))))))))
)
)
|
FinancialOntology.kif 2282-2296 |
|
( ! [V__P1,V__P2,V__C] :
(((s__instance(V__P1,s__Organism) &
s__instance(V__P2,s__Organism))
=>
(((s__instance(V__C,s__FamilyBusiness) &
s__possesses(V__P1,V__C)
&
s__possesses(V__P2,V__C))
=>
(s__familyRelation(V__P1,V__P2)))))
)
)
|
Mid-level-ontology.kif 6617-6622 |
|
| No TPTP formula. May not be expressible in strict first order. |
Merge.kif 11120-11127 |
|
( ! [V__Agent,V__Card] :
((s__instance(V__Agent,s__CognitiveAgent) =>
(((s__instance(V__Card,s__CreditCard) &
s__possesses(V__Agent,V__Card))
=>
(( ? [V__Account] :
((s__instance(V__Account,s__CreditCardAccount) &
s__cardAccount(V__Card,V__Account)
&
s__accountHolder(V__Account,V__Agent))))))))
)
)
|
FinancialOntology.kif 218-226 |
|
( ! [V__Agent,V__Card,V__Transaction] :
((s__instance(V__Agent,s__Agent) =>
(((s__instance(V__Card,s__DebitCard) &
s__possesses(V__Agent,V__Card)
&
s__instance(V__Transaction,s__FinancialTransaction) &
s__instrument(V__Transaction,V__Card))
=>
(( ? [V__PIN, V__Enter] :
((s__instance(V__PIN,s__SymbolicString) &
(s__pin(V__PIN,V__Card)
&
s__instance(V__Enter,s__EnteringAPin) &
s__patient(V__Enter,V__PIN)
&
s__agent(V__Enter,V__Agent)))))))))
)
)
|
FinancialOntology.kif 3483-3494 |
|
( ! [V__Agent,V__Card] :
((s__instance(V__Agent,s__CognitiveAgent) =>
(((s__instance(V__Card,s__DebitCard) &
s__possesses(V__Agent,V__Card))
=>
(( ? [V__Account] :
((s__instance(V__Account,s__DepositAccount) &
s__cardAccount(V__Card,V__Account)
&
s__accountHolder(V__Account,V__Agent))))))))
)
)
|
FinancialOntology.kif 203-211 |
|
( ! [V__AGENT,V__DEGREE] :
((s__instance(V__AGENT,s__Agent) =>
(((s__instance(V__DEGREE,s__AcademicDegree) &
s__possesses(V__AGENT,V__DEGREE))
=>
(( ? [V__PROGRAM, V__STUDY] :
((s__instance(V__STUDY,s__Process) &
(s__instance(V__PROGRAM,s__EducationalProgram) &
s__realization(V__STUDY,V__PROGRAM)
&
s__experiencer(V__STUDY,V__AGENT)))))))))
)
)
|
Mid-level-ontology.kif 14760-14768 |
|
| No TPTP formula. May not be expressible in strict first order. |
Mid-level-ontology.kif 23265-23272 |
|
| No TPTP formula. May not be expressible in strict first order. |
Mid-level-ontology.kif 23130-23137 |
|
( ! [V__AGENT,V__FLEET,V__NUM] :
(((s__instance(V__AGENT,s__Agent) &
s__instance(V__NUM,s__Integer))
=>
(((s__instance(V__FLEET,s__Fleet) &
s__fleetSize(V__AGENT,V__NUM)
&
s__possesses(V__AGENT,V__FLEET))
=>
(s__memberCount(V__FLEET,V__NUM)))))
)
)
|
Mid-level-ontology.kif 3461-3466 |
|
( ! [V__INTERNAL,V__AREA] :
((s__instance(V__AREA,s__Agent) =>
(((s__instance(V__INTERNAL,s__InternalShipRegister) &
s__possesses(V__AREA,V__INTERNAL))
=>
(s__instance(V__AREA,s__Nation)))))
)
)
|
Transportation.kif 1176-1180 |
|
( ! [V__OWNER,V__ITEM,V__LISTING] :
(((s__instance(V__ITEM,s__Object) &
s__instance(V__LISTING,s__WebListing) &
s__instance(V__OWNER,s__Agent) &
s__attribute(V__LISTING,s__ForSaleByOwner) &
s__possesses(V__OWNER,V__ITEM))
=>
(s__instance(V__OWNER,s__Human)))
)
)
|
UXExperimentalTerms.kif 472-479 |
|
| No TPTP formula. May not be expressible in strict first order. |
Mid-level-ontology.kif 15088-15099 |
|
( ! [V__NATIONAL,V__AREA] :
((s__instance(V__AREA,s__Agent) =>
(((s__instance(V__NATIONAL,s__NationalShipRegister) &
s__possesses(V__AREA,V__NATIONAL))
=>
(s__instance(V__AREA,s__Nation)))))
)
)
|
Transportation.kif 1126-1130 |
|
( ! [V__OFFSHORE,V__AREA] :
((s__instance(V__AREA,s__Agent) =>
(((s__instance(V__OFFSHORE,s__OffshoreShipRegister) &
s__possesses(V__AREA,V__OFFSHORE))
=>
(s__instance(V__AREA,s__Nation)))))
)
)
|
Transportation.kif 1192-1196 |
|
| No TPTP formula. May not be expressible in strict first order. |
Mid-level-ontology.kif 14828-14835 |
|
|
| Display limited to 25 items. Show next 25 |
|
| Display limited to 25 items. Show next 25 |
