( ! [V__Agent,V__Account] :
((s__instance(V__Account,s__FinancialAccount) =>
((((s__accountHolder(V__Account,V__Agent)
&
s__instance(V__Agent,s__Corporation))
=>
s__instance(V__Account,s__CorporateAccount))
&
(s__instance(V__Account,s__CorporateAccount) =>
(s__accountHolder(V__Account,V__Agent)
&
s__instance(V__Agent,s__Corporation))))))
)
)
|
FinancialOntology.kif 972-976 |
A cognitive agent holds account a financial account and the cognitive agent is an instance of corporation if and only if the financial account is an instance of corporate account |
( ! [V__Agent,V__Account] :
((s__instance(V__Account,s__FinancialAccount) =>
((((s__accountHolder(V__Account,V__Agent)
&
s__instance(V__Agent,s__Human))
=>
s__instance(V__Account,s__PersonalAccount))
&
(s__instance(V__Account,s__PersonalAccount) =>
(s__accountHolder(V__Account,V__Agent)
&
s__instance(V__Agent,s__Human))))))
)
)
|
FinancialOntology.kif 950-954 |
A cognitive agent holds account a financial account and the cognitive agent is an instance of human if and only if the financial account is an instance of personal account |
( ! [V__OBJ2,V__AIRCRAFT,V__QUANTITY] :
(((s__instance(V__OBJ2,s__SelfConnectedObject) &
s__instance(V__QUANTITY,s__AltitudeMeasure))
=>
((((s__altitude(V__AIRCRAFT,V__OBJ2,V__QUANTITY)
&
s__surface(V__OBJ2,s__PlanetEarth) &
s__instance(V__AIRCRAFT,s__Aircraft))
=>
s__absoluteHeight(V__AIRCRAFT,V__QUANTITY))
&
(s__absoluteHeight(V__AIRCRAFT,V__QUANTITY)
=>
(s__altitude(V__AIRCRAFT,V__OBJ2,V__QUANTITY)
&
s__surface(V__OBJ2,s__PlanetEarth) &
s__instance(V__AIRCRAFT,s__Aircraft))))))
)
)
|
MilitaryDevices.kif 1462-1467 |
The altitude of an aircraft is a self connected object and the self connected object is a surface of planet earth and the aircraft is an instance of aircraft if and only if an altitude measure is the absolute height of the aircraft |
( ! [V__NUMBER1,V__NUMBER2] :
(((((s__AbsoluteValueFn(V__NUMBER1)
= V__NUMBER2)
&
s__instance(V__NUMBER1,s__RealNumber) &
s__instance(V__NUMBER2,s__RealNumber))
=>
((s__instance(V__NUMBER1,s__NonnegativeRealNumber) &
(V__NUMBER1 = V__NUMBER2))
|
(s__instance(V__NUMBER1,s__NegativeRealNumber) &
(V__NUMBER2 = s__SubtractionFn(n__0,V__NUMBER1)))))
&
(((s__instance(V__NUMBER1,s__NonnegativeRealNumber) &
(V__NUMBER1 = V__NUMBER2))
|
(s__instance(V__NUMBER1,s__NegativeRealNumber) &
(V__NUMBER2 = s__SubtractionFn(n__0,V__NUMBER1))))
=>
((s__AbsoluteValueFn(V__NUMBER1)
= V__NUMBER2)
&
s__instance(V__NUMBER1,s__RealNumber) &
s__instance(V__NUMBER2,s__RealNumber))))
)
)
|
Merge.kif 4595-4606 |
The absolute value of a real number is equal to a nonnegative real number and the real number is an instance of real number and the nonnegative real number is an instance of real number if and only if the real number is an instance of nonnegative real number and the real number is equal to the nonnegative real number or the real number is an instance of negative real number and the nonnegative real number is equal to (0 and the real number) |
( ! [V__AGENT] :
((((s__instance(V__AGENT,s__SentientAgent) &
s__attribute(V__AGENT,s__Living))
=>
( ? [V__ATTR] :
((s__instance(V__ATTR,s__ConsciousnessAttribute) &
s__attribute(V__AGENT,V__ATTR)))))
&
(( ? [V__ATTR] :
((s__instance(V__ATTR,s__ConsciousnessAttribute) &
s__attribute(V__AGENT,V__ATTR))))
=>
(s__instance(V__AGENT,s__SentientAgent) &
s__attribute(V__AGENT,s__Living))))
)
)
|
Merge.kif 17453-17460 |
An object is an instance of sentient agent and living is an attribute of the object if and only if there exists an attribute such that the attribute is an instance of consciousness attribute and the attribute is an attribute of the object |
( ! [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 |
| No TPTP formula. May not be expressible in strict first order. |
FinancialOntology.kif 961-965 |
An entity is an instance of personal account and the number of instances in the class described by a symbolic string is greater than 1 if and only if the entity is an instance of joint account |
| No TPTP formula. May not be expressible in strict first order. |
Mid-level-ontology.kif 28317-28327 |
An entity is an instance of body part and Bare is an attribute of the entity holds during a time position if and only if there doesn't exist another entity such that the other entity is an instance of clothing and the other entity covers the entity holds during the time position |
| No TPTP formula. May not be expressible in strict first order. |
Merge.kif 11844-11851 |
A process is an instance of combining and an object is a resource for the process and an entity is a result of the process if and only if the object is not a part of the entity holds during the beginning of the time of existence of the process and the object is a part of the entity holds during the end of the time of existence of the process |
( ! [V__S,V__LD] :
((s__instance(V__S,s__RealNumber) =>
((((s__instance(V__LD,s__LiquidDrop) &
s__approximateDiameter(V__LD,s__MeasureFn(V__S,s__Micrometer))
&
s__lessThan(n__500,V__S))
=>
s__instance(V__LD,s__Droplet))
&
(s__instance(V__LD,s__Droplet) =>
(s__instance(V__LD,s__LiquidDrop) &
s__approximateDiameter(V__LD,s__MeasureFn(V__S,s__Micrometer))
&
s__lessThan(n__500,V__S))))))
)
)
|
Geography.kif 7082-7088 |
A self connected object is an instance of liquid drop and the approximate diameter of the self connected object is a real number micrometer(s) and 500 is less than the real number if and only if the self connected object is an instance of droplet |
( ! [V__PERSON] :
((((s__instance(V__PERSON,s__Human) &
( ! [V__ORG] :
((s__instance(V__ORG,s__Agent) =>
(~(s__employs(V__ORG,V__PERSON)))))))
=>
s__attribute(V__PERSON,s__Unemployed))
&
(s__attribute(V__PERSON,s__Unemployed) =>
(s__instance(V__PERSON,s__Human) &
( ! [V__ORG] :
((s__instance(V__ORG,s__Agent) =>
(~(s__employs(V__ORG,V__PERSON)))))))))
)
)
|
Merge.kif 16447-16453 |
A cognitive agent is an instance of human and for all an agent the agent doesn't employ the cognitive agent if and only if unemployed is an attribute of the cognitive agent |
( ! [V__P,V__S,V__PM] :
(((s__instance(V__P,s__SelfConnectedObject) &
s__instance(V__S,s__RealNumber))
=>
((((s__instance(V__PM,s__ParticulateMatter) &
s__part(V__P,V__PM)
&
s__approximateDiameter(V__P,s__MeasureFn(V__S,s__Micrometer))
&
s__greaterThan(n__10,V__S)
&
s__greaterThan(V__S,n__2_5))
=>
( ? [V__PM10] :
((s__instance(V__PM10,s__CoarseParticulateMatter) &
s__part(V__PM10,V__PM)))))
&
(( ? [V__PM10] :
((s__instance(V__PM10,s__CoarseParticulateMatter) &
s__part(V__PM10,V__PM))))
=>
(s__instance(V__PM,s__ParticulateMatter) &
s__part(V__P,V__PM)
&
s__approximateDiameter(V__P,s__MeasureFn(V__S,s__Micrometer))
&
s__greaterThan(n__10,V__S)
&
s__greaterThan(V__S,n__2_5))))))
)
)
|
Geography.kif 6998-7009 |
An object is an instance of PM and a self connected object is a part of the object and the approximate diameter of the self connected object is a real number micrometer(s) and 10 is greater than the real number and the real number is greater than 2.5 if and only if there exists the object10 such that the object10 is an instance of PM10 and the object10 is a part of the object |
( ! [V__P,V__S,V__PM] :
(((s__instance(V__P,s__SelfConnectedObject) &
s__instance(V__S,s__RealNumber))
=>
((((s__instance(V__PM,s__ParticulateMatter) &
s__part(V__P,V__PM)
&
s__approximateDiameter(V__P,s__MeasureFn(V__S,s__Micrometer))
&
s__greaterThanOrEqualTo(V__S,n__2_5))
=>
( ? [V__PM25] :
((s__instance(V__PM25,s__FineParticulateMatter) &
s__part(V__PM25,V__PM)))))
&
(( ? [V__PM25] :
((s__instance(V__PM25,s__FineParticulateMatter) &
s__part(V__PM25,V__PM))))
=>
(s__instance(V__PM,s__ParticulateMatter) &
s__part(V__P,V__PM)
&
s__approximateDiameter(V__P,s__MeasureFn(V__S,s__Micrometer))
&
s__greaterThanOrEqualTo(V__S,n__2_5))))))
)
)
|
Geography.kif 7027-7037 |
An object is an instance of PM and a self connected object is a part of the object and the approximate diameter of the self connected object is a real number micrometer(s) and the real number is greater than or equal to 2.5 if and only if there exists the object25 such that the object25 is an instance of PM2.5 and the object25 is a part of the object |
( ! [V__SCROLL] :
((((s__instance(V__SCROLL,s__WindowScrolling) &
s__instance(V__SCROLL,s__UserSignifiedGraphicalAction))
=>
s__instance(V__SCROLL,s__WindowScrollingByUser))
&
(s__instance(V__SCROLL,s__WindowScrollingByUser) =>
(s__instance(V__SCROLL,s__WindowScrolling) &
s__instance(V__SCROLL,s__UserSignifiedGraphicalAction))))
)
)
|
ComputerInput.kif 1804-1808 |
An entity is an instance of WindowScrolling and the entity is an instance of UserSignifiedGraphicalAction if and only if the entity is an instance of WindowScrollingByUser |
( ! [V__AMOUNT,V__UNIT] :
(((s__instance(V__AMOUNT,s__Number) &
s__instance(V__AMOUNT,s__PhysicalQuantity))
=>
((((s__instance(V__UNIT,s__UnitOfMeasure) &
(V__AMOUNT = s__MeasureFn(n__1,s__SquareUnitFn(V__UNIT))))
=>
(V__AMOUNT = s__MultiplicationFn(s__MeasureFn(n__1,V__UNIT)
,s__MeasureFn(n__1,V__UNIT))))
&
((V__AMOUNT = s__MultiplicationFn(s__MeasureFn(n__1,V__UNIT)
,s__MeasureFn(n__1,V__UNIT)))
=>
(s__instance(V__UNIT,s__UnitOfMeasure) &
(V__AMOUNT = s__MeasureFn(n__1,s__SquareUnitFn(V__UNIT))))))))
)
)
|
Geography.kif 3804-3808 |
An unit of measure is an instance of unit of measure and a number is equal to 1 the square unit of the unit of measure(s) if and only if the number is equal to 1 the unit of measure(s) and 1 the unit of measure(s) |
( ! [V__Account,V__Withdrawal] :
((((s__instance(V__Withdrawal,s__Withdrawal) &
s__instance(V__Account,s__FinancialAccount) &
s__origin(V__Withdrawal,s__CurrencyFn(V__Account))
&
~(( ? [V__Penalty] :
((s__instance(V__Penalty,s__Penalty) &
s__destination(V__Penalty,s__CurrencyFn(V__Account))
&
s__causes(V__Withdrawal,V__Penalty))))))
=>
s__liquidity(V__Account,s__HighLiquidity))
&
(s__liquidity(V__Account,s__HighLiquidity) =>
(s__instance(V__Withdrawal,s__Withdrawal) &
s__instance(V__Account,s__FinancialAccount) &
s__origin(V__Withdrawal,s__CurrencyFn(V__Account))
&
~(( ? [V__Penalty] :
((s__instance(V__Penalty,s__Penalty) &
s__destination(V__Penalty,s__CurrencyFn(V__Account))
&
s__causes(V__Withdrawal,V__Penalty))))))))
)
)
|
FinancialOntology.kif 1767-1777 |
A process is an instance of withdrawal and a financial account is an instance of financial account and the process originates at the currency of the financial account and there doesn't exist another process such that the other process is an instance of penalty and the other process ends up at the currency of the financial account and the process causes the other process if and only if the liqudity of the financial account is high liquidity |
| No TPTP formula. May not be expressible in strict first order. |
Weather.kif 2673-2683 |
An entity is an instance of region and the entity the attribute standard ambient temperature and pressure holds during a time position if and only if 298.15 kelvin degree(s) is an air temperature of the entity and 29.530 inch mercury(s) is a barometric pressure of the entity holds during the time position |
( ! [V__PLACE,V__AREA] :
((((s__located(V__PLACE,V__AREA)
&
s__instance(V__PLACE,s__PostalPlace) &
s__instance(V__AREA,s__PostcodeArea))
=>
s__postPostcodeArea(V__PLACE,V__AREA))
&
(s__postPostcodeArea(V__PLACE,V__AREA)
=>
(s__located(V__PLACE,V__AREA)
&
s__instance(V__PLACE,s__PostalPlace) &
s__instance(V__AREA,s__PostcodeArea))))
)
)
|
Mid-level-ontology.kif 22914-22919 |
A PostalPlace is located at a PostcodeArea and the PostalPlace is an instance of PostalPlace and the PostcodeArea is an instance of PostcodeArea if and only if the PostalPlace is in post code the PostcodeArea |
( ! [V__PLACE,V__GEO] :
((((s__located(V__PLACE,V__GEO)
&
s__instance(V__PLACE,s__PostalPlace) &
s__instance(V__GEO,s__City))
=>
s__postCity(V__PLACE,V__GEO))
&
(s__postCity(V__PLACE,V__GEO)
=>
(s__located(V__PLACE,V__GEO)
&
s__instance(V__PLACE,s__PostalPlace) &
s__instance(V__GEO,s__City))))
)
)
|
Mid-level-ontology.kif 22887-22892 |
A PostalPlace is located at a city and the PostalPlace is an instance of PostalPlace and the city is an instance of city if and only if the PostalPlace is in the city |
( ! [V__PLACE,V__GEO] :
((((s__located(V__PLACE,V__GEO)
&
s__instance(V__PLACE,s__PostalPlace) &
s__instance(V__GEO,s__Neighborhood))
=>
s__postNeighborhood(V__PLACE,V__GEO))
&
(s__postNeighborhood(V__PLACE,V__GEO)
=>
(s__located(V__PLACE,V__GEO)
&
s__instance(V__PLACE,s__PostalPlace) &
s__instance(V__GEO,s__Neighborhood))))
)
)
|
Mid-level-ontology.kif 22800-22805 |
A PostalPlace is located at a neighborhood and the PostalPlace is an instance of PostalPlace and the neighborhood is an instance of neighborhood if and only if the PostalPlace is in the neighborhood |
( ! [V__PLACE,V__GEO] :
((((s__located(V__PLACE,V__GEO)
&
s__instance(V__PLACE,s__PostalPlace) &
s__instance(V__GEO,s__StateOrProvince))
=>
s__postDistrict(V__PLACE,V__GEO))
&
(s__postDistrict(V__PLACE,V__GEO)
=>
(s__located(V__PLACE,V__GEO)
&
s__instance(V__PLACE,s__PostalPlace) &
s__instance(V__GEO,s__StateOrProvince))))
)
)
|
Mid-level-ontology.kif 22871-22876 |
A PostalPlace is located at a state or province and the PostalPlace is an instance of PostalPlace and the state or province is an instance of state or province if and only if the PostalPlace is in the state or province |
( ! [V__PLACE,V__GEO] :
((((s__located(V__PLACE,V__GEO)
&
s__instance(V__PLACE,s__PostalPlace) &
(s__instance(V__GEO,s__Nation) |
s__instance(V__GEO,s__DependencyOrSpecialSovereigntyArea)))
=>
s__postCountry(V__PLACE,V__GEO))
&
(s__postCountry(V__PLACE,V__GEO)
=>
(s__located(V__PLACE,V__GEO)
&
s__instance(V__PLACE,s__PostalPlace) &
(s__instance(V__GEO,s__Nation) |
s__instance(V__GEO,s__DependencyOrSpecialSovereigntyArea)))))
)
)
|
Mid-level-ontology.kif 22837-22844 |
A PostalPlace is located at a geopolitical area and the PostalPlace is an instance of PostalPlace and the geopolitical area is an instance of nation or the geopolitical area is an instance of dependency or special sovereignty area if and only if the PostalPlace is in the geopolitical area |
( ! [V__TIME,V__PHYS] :
((s__instance(V__PHYS,s__Physical) =>
((((s__time(V__PHYS,V__TIME)
&
s__instance(V__TIME,s__TimePoint))
=>
s__temporallyBetweenOrEqual(s__BeginFn(s__WhenFn(V__PHYS))
,V__TIME,s__EndFn(s__WhenFn(V__PHYS))))
&
(s__temporallyBetweenOrEqual(s__BeginFn(s__WhenFn(V__PHYS))
,V__TIME,s__EndFn(s__WhenFn(V__PHYS)))
=>
(s__time(V__PHYS,V__TIME)
&
s__instance(V__TIME,s__TimePoint))))))
)
)
|
Merge.kif 7901-7905 |
A physical exists during a time point and the time point is an instance of time point if and only if the time point is between or at the beginning of the time of existence of the physical and the end of the time of existence of the physical |
( ! [V__AGENT2,V__OBJECT,V__AGENT1] :
(((s__instance(V__AGENT2,s__Agent) &
s__instance(V__AGENT1,s__Agent))
=>
(((( ? [V__BORROW] :
((s__instance(V__BORROW,s__Borrowing) &
s__agent(V__BORROW,V__AGENT1)
&
s__origin(V__BORROW,V__AGENT2)
&
s__patient(V__BORROW,V__OBJECT))))
=>
( ? [V__LEND] :
((s__instance(V__LEND,s__Lending) &
s__agent(V__LEND,V__AGENT2)
&
s__destination(V__LEND,V__AGENT1)
&
s__patient(V__LEND,V__OBJECT)))))
&
(( ? [V__LEND] :
((s__instance(V__LEND,s__Lending) &
s__agent(V__LEND,V__AGENT2)
&
s__destination(V__LEND,V__AGENT1)
&
s__patient(V__LEND,V__OBJECT))))
=>
( ? [V__BORROW] :
((s__instance(V__BORROW,s__Borrowing) &
s__agent(V__BORROW,V__AGENT1)
&
s__origin(V__BORROW,V__AGENT2)
&
s__patient(V__BORROW,V__OBJECT))))))))
)
)
|
Merge.kif 11204-11216 |
There exists a process such that the process is an instance of borrowing and an agent is an agent of the process and the process originates at another agent and an entity is a patient of the process if and only if there exists another process such that the other process is an instance of lending and the other agent is an agent of the other process and the other process ends up at the agent and the entity is a patient of the other process |
( ! [V__ARTIFACT] :
(((( ? [V__BUILD] :
((s__instance(V__BUILD,s__Constructing) &
s__result(V__BUILD,V__ARTIFACT))))
=>
s__instance(V__ARTIFACT,s__StationaryArtifact))
&
(s__instance(V__ARTIFACT,s__StationaryArtifact) =>
( ? [V__BUILD] :
((s__instance(V__BUILD,s__Constructing) &
s__result(V__BUILD,V__ARTIFACT))))))
)
)
|
Merge.kif 12186-12191 |
There exists a process such that the process is an instance of constructing and an entity is a result of the process if and only if the entity is an instance of stationary artifact |
|
| Display limited to 25 items. Show next 25 |
|
| Display limited to 25 items. Show next 25 |
