Browsing Interface : Welcome guest : log in
Home |  Graph |  ]  KB:  Language:   

Formal Language: 



KB Term:  Term intersection
English Word: 

  instance

Sigma KEE - instance
instance

appearance as argument number 1
-------------------------


s__documentation(s__instance__m,s__ChineseLanguage,'"如果一个物体属于一个 SetOrClass, 这物体就那个 SetOrClass 的一个instance。 一个个体可以是许多类别的一个 instance, 其中有一些可以是其他类别 的子类别,所以对于 instance 并没有假设任何具体或独特的含义。"')

chinese_format.kif 1359-1361
s__documentation(s__instance__m,s__EnglishLanguage,'"An object is an instance of a Class if it is included in that Class. An individual may be an instance of many classes, some of which may be subclasses of others. Thus, there is no assumption in the meaning of instance about specificity or uniqueness."')

Merge.kif 84-87
s__domain(s__instance__m,n__1,s__Entity)

Merge.kif 81-81 The number 1 argument of instance is an instance of entity
s__domain(s__instance__m,n__2,s__Class)

Merge.kif 82-82 The number 2 argument of instance is an instance of class
s__instance(s__BinaryPredicate,s__SetOrClass)

s__instance(s__instance__m,s__BinaryPredicate)

Merge.kif 80-80 instance is an instance of binary predicate

appearance as argument number 2
-------------------------


s__format(s__ChineseLanguage,s__instance__m,'"%1 %n 是 %2 的 instance"')

chinese_format.kif 305-305
s__format(s__EnglishLanguage,s__instance__m,'"%1 is %n an instance of %2"')

english_format.kif 313-313
s__relatedInternalConcept(s__member__m,s__instance__m)

Merge.kif 1179-1179 member is internally related to instance
s__subrelation(s__element__m,s__instance__m)

Merge.kif 5175-5175 element is a subrelation of instance
s__subrelation(s__immediateInstance__m,s__instance__m)

Merge.kif 89-89 immediate instance is a subrelation of instance
s__termFormat(s__ChineseLanguage,s__instance__m,'"例"')

domainEnglishFormat.kif 30234-30234
s__termFormat(s__ChineseLanguage,s__instance__m,'"实例"')

chinese_format.kif 306-306
s__termFormat(s__ChineseTraditionalLanguage,s__instance__m,'"例"')

domainEnglishFormat.kif 30233-30233
s__termFormat(s__EnglishLanguage,s__instance__m,'"instance"')

domainEnglishFormat.kif 30232-30232

antecedent
-------------------------


( ! [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 2291-2296 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 28876-28886 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 1818-1822 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 1788-1798 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 23460-23465 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 23433-23438 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 23346-23351 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 23417-23422 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 23383-23390 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

consequent
-------------------------


( ! [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__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__LIST3,V__LIST1,V__LIST2] :
   (((s__instance(V__LIST3,s__List) &
         s__instance(V__LIST1,s__List) &
         s__instance(V__LIST2,s__List))
       =>
       (((((V__LIST3 = s__ListConcatenateFn(V__LIST1,V__LIST2))
             &
             ~((V__LIST1 = s__NullList))
               &
               ~((V__LIST2 = s__NullList)))
               =>
               ( ! [V__NUMBER1, V__NUMBER2] :
                 (((s__lessThanOrEqualTo(V__NUMBER1,s__ListLengthFn(V__LIST1))
                   &
                   s__lessThanOrEqualTo(V__NUMBER2,s__ListLengthFn(V__LIST2))
               &
               s__instance(V__NUMBER1,s__PositiveInteger) &
               s__instance(V__NUMBER2,s__PositiveInteger))
             =>
             (((s__ListOrderFn(V__LIST3,V__NUMBER1)
                 = s__ListOrderFn(V__LIST1,V__NUMBER1))
             &
             (s__ListOrderFn(V__LIST3,s__AdditionFn(s__ListLengthFn(V__LIST1)
            ,V__NUMBER2))
         = s__ListOrderFn(V__LIST2,V__NUMBER2))))))))
&
(( ! [V__NUMBER1, V__NUMBER2] :
(((s__lessThanOrEqualTo(V__NUMBER1,s__ListLengthFn(V__LIST1))
&
s__lessThanOrEqualTo(V__NUMBER2,s__ListLengthFn(V__LIST2))
&
s__instance(V__NUMBER1,s__PositiveInteger) &
s__instance(V__NUMBER2,s__PositiveInteger))
=>
(((s__ListOrderFn(V__LIST3,V__NUMBER1)
= s__ListOrderFn(V__LIST1,V__NUMBER1))
&
(s__ListOrderFn(V__LIST3,s__AdditionFn(s__ListLengthFn(V__LIST1)
,V__NUMBER2))
= s__ListOrderFn(V__LIST2,V__NUMBER2)))))))
=>
((V__LIST3 = s__ListConcatenateFn(V__LIST1,V__LIST2))
&
~((V__LIST1 = s__NullList))
&
~((V__LIST2 = s__NullList)))))))
)
)

Merge.kif 2979-2995 A list is equal to the list composed of another list and a third list and the other list is not equal to null list and the third list is not equal to null list if and only if for all a positive integer and another positive integer
( ! [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
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 28876-28886 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
( ! [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__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 1818-1822 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
No TPTP formula. May not be expressible in strict first order. Economy.kif 1523-1528 A geopolitical area annual expenditures of area in period a currency measure for a kind of time interval 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 an annual expenditures of area of the geopolitical area holds during the time position
No TPTP formula. May not be expressible in strict first order. Economy.kif 1494-1499 A geopolitical area annual revenues of area in period a currency measure for a kind of time interval 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 an annual revenues of area of the geopolitical area holds during the time position
( ! [V__HOLE1] :
   ((s__instance(V__HOLE1,s__Object) =>
       (((s__attribute(V__HOLE1,s__Fillable) =>
             ( ? [V__HOLE2] :
               ((s__instance(V__HOLE2,s__Hole) &
                   s__part(V__HOLE1,V__HOLE2)))))
         &
         (( ? [V__HOLE2] :
             ((s__instance(V__HOLE2,s__Hole) &
                 s__part(V__HOLE1,V__HOLE2))))
         =>
         s__attribute(V__HOLE1,s__Fillable)))))
)
)

Merge.kif 9530-9535 Fillable is an attribute of an object if and only if there exists another object such that the other object is an instance of hole and the object is a part of the other object
( ! [V__MUSIC] :
   (((s__instance(V__MUSIC,s__Object) &
         s__instance(V__MUSIC,s__Process))
       =>
       (((s__attribute(V__MUSIC,s__PolyphonicMusic) =>
             ( ? [V__PART1, V__PART2] :
               ((s__instance(V__MUSIC,s__MakingMusic) &
                   s__instance(V__PART1,s__MakingMusic) &
                   s__instance(V__PART2,s__MakingMusic) &
                   s__subProcess(V__PART1,V__MUSIC)
                 &
                 s__subProcess(V__PART2,V__MUSIC)
               &
               ~((V__PART1 = V__PART2))
               &
               s__cooccur(V__PART1,V__MUSIC)
             &
             s__cooccur(V__PART2,V__MUSIC)))))
   &
   (( ? [V__PART1, V__PART2] :
       ((s__instance(V__MUSIC,s__MakingMusic) &
           s__instance(V__PART1,s__MakingMusic) &
           s__instance(V__PART2,s__MakingMusic) &
           s__subProcess(V__PART1,V__MUSIC)
         &
         s__subProcess(V__PART2,V__MUSIC)
       &
       ~((V__PART1 = V__PART2))
       &
       s__cooccur(V__PART1,V__MUSIC)
     &
     s__cooccur(V__PART2,V__MUSIC))))
=>
s__attribute(V__MUSIC,s__PolyphonicMusic)))))
)
)

Mid-level-ontology.kif 695-706 Polyphonic music is an attribute of an object if and only if there exist a process and another process such that the object is an instance of making music and the process is an instance of making music and the other process is an instance of making music and the process is a subprocess of the object and the other process is a subprocess of the object and the process is not equal to the other process and the process occurs at the same time as the object and the other process occurs at the same time as the object
( ! [V__LAND,V__WATER,V__DIST] :
   (((s__instance(V__LAND,s__Physical) &
         s__instance(V__WATER,s__Object) &
         s__instance(V__DIST,s__RealNumber))
       =>
       (((s__attribute(V__WATER,s__OpenSea) =>
             (s__instance(V__WATER,s__SaltWaterArea) &
               ~(s__instance(V__WATER,s__LandlockedWater))
               &
               s__distance(V__LAND,V__WATER,s__MeasureFn(V__DIST,s__NauticalMile))
             &
             s__greaterThan(V__DIST,n__5)))
       &
       ((s__instance(V__WATER,s__SaltWaterArea) &
           ~(s__instance(V__WATER,s__LandlockedWater))
           &
           s__distance(V__LAND,V__WATER,s__MeasureFn(V__DIST,s__NauticalMile))
         &
         s__greaterThan(V__DIST,n__5))
     =>
     s__attribute(V__WATER,s__OpenSea)))))
)
)

Geography.kif 4506-4514 Open sea is an attribute of an object if and only if the object is an instance of salt water area and the object is not an instance of landlocked water and the distance between a physical and the object is a real number nautical mile(s) and the real number is greater than 5
( ! [V__AccountType,V__Bank] :
   (((s__subclass(V__AccountType,s__FinancialAccount) &
         s__instance(V__AccountType,s__Class) &
         s__instance(V__Bank,s__Bank_FinancialOrganization))
       =>
       (((s__bankAccount(V__AccountType,V__Bank)
           =>
           ( ? [V__Account] :
             ((s__instance(V__Account,s__FinancialAccount) &
                 (s__instance(V__Account,V__AccountType)
                 &
                 s__accountAt(V__Account,V__Bank))))))
     &
     (( ? [V__Account] :
         ((s__instance(V__Account,s__FinancialAccount) &
             (s__instance(V__Account,V__AccountType)
             &
             s__accountAt(V__Account,V__Bank)))))
   =>
   s__bankAccount(V__AccountType,V__Bank)))))
)
)

FinancialOntology.kif 3855-3860 A bank- financial organization is a bank account of a kind of financial account if and only if there exists another financial account such that the other financial account is an instance of a kind of financial account and the other financial account is held by the bank- financial organization
No TPTP formula. May not be expressible in strict first order. Economy.kif 1569-1574 A geopolitical area capital expenditures of area in period a currency measure for a kind of time interval 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 capital expenditures of area of the geopolitical area holds during the time position
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
No TPTP formula. May not be expressible in strict first order. Economy.kif 3671-3676 An UnitOfCurrency currency exchange rate in period a currency measure for a kind of time interval 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 the UnitOfCurrency holds during the time position
( ! [V__AGENT2,V__AGENT1] :
   (((s__instance(V__AGENT2,s__CognitiveAgent) &
         s__instance(V__AGENT1,s__CognitiveAgent))
       =>
       (((s__customer(V__AGENT1,V__AGENT2)
           =>
           ( ? [V__SERVICE] :
             ((s__instance(V__SERVICE,s__FinancialTransaction) &
                 s__agent(V__SERVICE,V__AGENT2)
               &
               s__destination(V__SERVICE,V__AGENT1)))))
     &
     (( ? [V__SERVICE] :
         ((s__instance(V__SERVICE,s__FinancialTransaction) &
             s__agent(V__SERVICE,V__AGENT2)
           &
           s__destination(V__SERVICE,V__AGENT1))))
   =>
   s__customer(V__AGENT1,V__AGENT2)))))
)
)

Mid-level-ontology.kif 7284-7290 A cognitive agent is a customer of another cognitive agent if and only if there exists a process such that the process is an instance of financial transaction and the cognitive agent is an agent of the process and the process ends up at the other cognitive agent
( ! [V__Org,V__Person2,V__Person1] :
   (((s__instance(V__Org,s__Organization) &
         s__instance(V__Person2,s__CognitiveAgent) &
         s__instance(V__Person1,s__CognitiveAgent))
       =>
       (((s__customerRepresentative(V__Person1,V__Person2,V__Org)
           =>
           ( ? [V__Service] :
             ((s__instance(V__Service,s__FinancialTransaction) &
                 s__employs(V__Org,V__Person1)
               &
               s__agent(V__Service,V__Person1)
             &
             s__destination(V__Service,V__Person2)))))
   &
   (( ? [V__Service] :
       ((s__instance(V__Service,s__FinancialTransaction) &
           s__employs(V__Org,V__Person1)
         &
         s__agent(V__Service,V__Person1)
       &
       s__destination(V__Service,V__Person2))))
=>
s__customerRepresentative(V__Person1,V__Person2,V__Org)))))
)
)

FinancialOntology.kif 3597-3604 A cognitive agent customer representative another cognitive agent for an organization if and only if there exists a process such that the process is an instance of financial transaction and the organization employs the cognitive agent and the cognitive agent is an agent of the process and the process ends up at the other cognitive agent
No TPTP formula. May not be expressible in strict first order. Economy.kif 2822-2827 A geopolitical area is economic aid donated in period a currency measure for a kind of time interval 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 an economic aid donated of the geopolitical area holds during the time position
No TPTP formula. May not be expressible in strict first order. Economy.kif 2862-2867 A geopolitical area is economic aid received net in period a currency measure for a kind of time interval 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 an economic aid received net of the geopolitical area holds during the time position
No TPTP formula. May not be expressible in strict first order. Economy.kif 2060-2065 A geopolitical area is electricity fraction from source in period a kind of power generation for a real number with a kind of time interval 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 geopolitical area is electricity fraction from source a kind of power generation for the real number holds during the time position

Display limited to 25 items. Show next 25

Display limited to 25 items. Show next 25

statement
-------------------------


No TPTP formula. May not be expressible in strict first order. Government.kif 1227-1234 For all ?AGENT, ?VOTER,, , ?ELECTION and ?VOTING contains information exclusive male suffrage
No TPTP formula. May not be expressible in strict first order. Government.kif 909-917 For all ?COUNTRY, ?ELECTION,, , ?VOTING and ?VOTER contains information voter citizenship requirement
No TPTP formula. May not be expressible in strict first order. Government.kif 1078-1089 For all ?POLITY, ?AGENT,, , ?ELECTION,, , ?VOTINGAGE and ?AGE contains information universal suffrage law
No TPTP formula. May not be expressible in strict first order. Government.kif 1146-1160 For all ?POLITY, ?VOTER,, , ?ELECTION,, , ?VOTINGAGE and ?AGE contains information compulsory suffrage law
No TPTP formula. May not be expressible in strict first order. WMD.kif 912-920 ?SYMPTOM is a biochemical agent syndrome of ?AGENT and ?AGENT biochemical agent antidote ?SUBSTANCE for ?PROCESS and ?SAMPLE is an instance of ?SUBSTANCE and ?THERAPY is an instance of ?PROCESS and ?ORGANISM experiences ?THERAPY and ?SAMPLE is a patient of ?THERAPY decreases likelihood of ?SYMPTOM is an attribute of ?ORGANISM
No TPTP formula. May not be expressible in strict first order. Military.kif 867-876 The available for military service male of a geopolitical area is equal to the number of instances in the class described by a symbolic string
No TPTP formula. May not be expressible in strict first order. People.kif 462-472 The children born per woman of a geopolitical area and the year an integer is equal to the number of instances in the class described by a symbolic string
No TPTP formula. May not be expressible in strict first order. Military.kif 890-901 The fit for military service male of a geopolitical area is equal to the number of instances in the class described by a symbolic string
No TPTP formula. May not be expressible in strict first order. People.kif 49-54 The population of a geopolitical area is equal to the number of instances in the class described by a symbolic string
No TPTP formula. May not be expressible in strict first order. Military.kif 928-941 The reaching military age annually male of a geopolitical area and a year is equal to the number of instances in the class described by a symbolic string
( ? [V__THING] :
   (s__instance(V__THING,s__Entity)))

Merge.kif 791-792 There exists an entity such that the entity is an instance of entity
No TPTP formula. May not be expressible in strict first order. Media.kif 1972-1980 There exists a time interval such that the time interval is an instance of time interval and the time interval finishes the time of existence of JesusOfNazareth and the time interval starts the time of existence of TwelveApostles and for all an entity
No TPTP formula. May not be expressible in strict first order. ComputingBrands.kif 3283-3289 IBookstore has the purpose there exists ?D such that ?D is an instance of downloading and iBookstore is an instrument for ?D and ?T is an instance of text and the object transferred in ?D is ?T
No TPTP formula. May not be expressible in strict first order. Media.kif 2507-2508 Montenegro is an instance of european nation holds during after the day 3
No TPTP formula. May not be expressible in strict first order. Media.kif 2505-2506 Montenegro is an instance of independent state holds during after the day 3
No TPTP formula. May not be expressible in strict first order. Media.kif 2519-2520 Serbia and montenegro is not an instance of independent state holds during after the day 3
No TPTP formula. May not be expressible in strict first order. Media.kif 2492-2493 Serbia is an instance of european nation holds during after the day 5
No TPTP formula. May not be expressible in strict first order. Media.kif 2490-2491 Serbia is an instance of independent state holds during after the day 5
No TPTP formula. May not be expressible in strict first order. WMD.kif 762-768 ?SYMPTOM is a biochemical agent syndrome of ?AGENT and ?PROCESSTYPE is a biochemical agent delivery of ?AGENT and ?PROCESS is an instance of ?PROCESSTYPE and ?ORGANISM experiences ?PROCESS increases likelihood of ?SYMPTOM is an attribute of ?ORGANISM
( ! [V__WINDOW] :
   (~((s__hasGUEState(V__WINDOW,s__GUE_NonVisibleState) &
         s__hasGUEState(V__WINDOW,s__GUE_ActiveState) &
         s__instance(V__WINDOW,s__InterfaceWindow)))
     )
   )

ComputerInput.kif 2040-2044 ~{ A GUIElement has state GUE_NonVisibleState } or ~{ the GUIElement has state GUE_ActiveState } or ~{ the GUIElement is an instance of InterfaceWindow }
( ! [V__CURSOR] :
   (~((s__instance(V__CURSOR,s__Cursor) &
         s__hasGUEState(V__CURSOR,s__GUE_SelectedState)))
     )
   )

ComputerInput.kif 2255-2258 ~{ A GUIElement is an instance of Cursor } or ~{ the GUIElement has state GUE_SelectedState }
( ! [V__CURSOR] :
   (~((s__instance(V__CURSOR,s__MouseCursor) &
         s__hasGUEState(V__CURSOR,s__GUE_ActiveState)))
     )
   )

ComputerInput.kif 1981-1984 ~{ A GUIElement is an instance of MouseCursor } or ~{ the GUIElement has state GUE_ActiveState }
( ! [V__NUMBER1,V__NUMBER2,V__GRAPH] :
   (((s__instance(V__NUMBER1,s__PositiveInteger) &
         s__instance(V__NUMBER2,s__PositiveInteger) &
         s__instance(V__GRAPH,s__Graph))
       =>
       (~(( ? [V__PATH1, V__PATH2] :
             ((s__instance(V__PATH1,s__GraphPath) &
                 s__instance(V__PATH2,s__GraphPath) &
                 (s__instance(V__PATH1,s__CutSetFn(V__GRAPH))
               &
               s__instance(V__PATH2,s__MinimalCutSetFn(V__GRAPH))
           &
           s__pathLength(V__PATH1,V__NUMBER1)
         &
         s__pathLength(V__PATH2,V__NUMBER2)
       &
       s__lessThan(V__NUMBER1,V__NUMBER2))))))))
)
)

Merge.kif 5839-5846 There don't exist a graph path and another graph path such that the graph path is an instance of the set of paths that partition a graph into two separate graphs and the other graph path is an instance of the set of minimal paths that partition the graph into two separate graphs and the length of the graph path is a positive integer and the length of the other graph path is another positive integer and the positive integer is less than the other positive integer

appearance as argument number 0
-------------------------


( ! [V__PARTTYPE,V__VIR] :
   (((s__subclass(V__PARTTYPE,s__CellPart) &
         s__instance(V__PARTTYPE,s__Class) &
         s__instance(V__VIR,s__Cell))
       =>
       (s__instance(s__CellPartFn(V__VIR,V__PARTTYPE)
      ,V__PARTTYPE)))
)
)

VirusProteinAndCellPart.kif 594-594 The cell part of a cell and a kind of cell part is an instance of a kind of cell part
( ! [V__PARTTYPE,V__VIR] :
   (((s__subclass(V__PARTTYPE,s__VirusPart) &
         s__instance(V__PARTTYPE,s__Class) &
         s__instance(V__VIR,s__Virus))
       =>
       (s__instance(s__ViralPartFn(V__VIR,V__PARTTYPE)
      ,V__PARTTYPE)))
)
)

VirusProteinAndCellPart.kif 583-583 The viral part of a virus and a kind of virus part is an instance of a kind of virus part
s__instance(s__FinancialRating,s__SetOrClass)

s__instance(s__AAA_Rating,s__FinancialRating)

FinancialOntology.kif 2482-2482 AAA-rating is an instance of financial rating
s__instance(s__ABPFn__m,s__UnaryFunction)

s__instance(s__UnaryFunction,s__SetOrClass)

UXExperimentalTerms.kif 3430-3430 Average buying price is an instance of unary function
s__instance(s__ABTest,s__ExperimentAttribute)

s__instance(s__ExperimentAttribute,s__SetOrClass)

UXExperimentalTerms.kif 4621-4621 A/B test is an instance of experiment attribute
s__instance(s__APucikwarLanguage,s__CentralGreatAndamaneseLanguage)

s__instance(s__CentralGreatAndamaneseLanguage,s__SetOrClass)

Languages.kif 5379-5379 A pucikwar language is an instance of central great andamanese language
s__instance(s__OrganizationOfNations,s__SetOrClass)

s__instance(s__ASEANRegionalForum,s__OrganizationOfNations)

Government.kif 2845-2845 ASEAN regional forum is an instance of organization of nations
s__instance(s__ASPFn__m,s__UnaryFunction)

s__instance(s__UnaryFunction,s__SetOrClass)

UXExperimentalTerms.kif 3473-3473 Average buying price is an instance of unary function
s__instance(s__ATandTCorp,s__Corporation)

s__instance(s__Corporation,s__SetOrClass)

ComputingBrands.kif 2089-2089 ATandTCorp is an instance of corporation
s__instance(s__Archipelago,s__SetOrClass)

s__instance(s__AalandIslands,s__Archipelago)

Media.kif 2530-2530 AalandIslands is an instance of archipelago
s__instance(s__DependencyOrSpecialSovereigntyArea,s__SetOrClass)

s__instance(s__AalandIslands,s__DependencyOrSpecialSovereigntyArea)

Media.kif 2531-2531 AalandIslands is an instance of dependency or special sovereignty area
s__instance(s__UnclassifiedSpokenLanguage,s__SetOrClass)

s__instance(s__AariyaLanguage,s__UnclassifiedSpokenLanguage)

Languages.kif 3771-3771 Aariya language is an instance of unclassified spoken language
s__instance(s__ReligiousPosition,s__SetOrClass)

s__instance(s__Abbot,s__ReligiousPosition)

People.kif 1212-1212 Abbot is an instance of religious position
s__instance(s__SpokenHumanLanguage,s__SetOrClass)

s__instance(s__AbinomnLanguage,s__SpokenHumanLanguage)

Languages.kif 2923-2923 Abinomn language is an instance of spoken human language
s__instance(s__AbishiraLanguage,s__UnclassifiedSpokenLanguage)

s__instance(s__UnclassifiedSpokenLanguage,s__SetOrClass)

Languages.kif 3777-3777 Abishira language is an instance of unclassified spoken language
s__instance(s__NorthCaucasianLanguage,s__SetOrClass)

s__instance(s__AbkhazLanguage,s__NorthCaucasianLanguage)

Languages.kif 14542-14542 AbkhazLanguage is an instance of north caucasian language
s__instance(s__BinaryFunction,s__SetOrClass)

s__instance(s__AbortedFn__m,s__BinaryFunction)

MilitaryProcesses.kif 2390-2390 Aborted is an instance of binary function
s__instance(s__BinaryFunction,s__SetOrClass)

s__instance(s__AbortedLaunchFn__m,s__BinaryFunction)

MilitaryProcesses.kif 2456-2456 Aborted launch is an instance of binary function
s__instance(s__BinaryFunction,s__SetOrClass)

s__instance(s__AbortedMissionFn__m,s__BinaryFunction)

MilitaryProcesses.kif 2410-2410 Aborted mission is an instance of binary function
s__instance(s__AntiSymmetricPositionalAttribute,s__SetOrClass)

s__instance(s__Above,s__AntiSymmetricPositionalAttribute)

Merge.kif 16285-16285 Above is an instance of AntiSymmetricPositionalAttribute
s__instance(s__Above,s__PositionalAttribute)

s__instance(s__PositionalAttribute,s__SetOrClass)

Merge.kif 16284-16284 Above is an instance of positional attribute
s__instance(s__TotalValuedRelation,s__SetOrClass)

s__instance(s__AbsoluteValueFn__m,s__TotalValuedRelation)

Merge.kif 4588-4588 Absolute value is an instance of total valued relation
s__instance(s__UnaryFunction,s__SetOrClass)

s__instance(s__AbsoluteValueFn__m,s__UnaryFunction)

Merge.kif 4587-4587 Absolute value is an instance of unary function
s__instance(s__NorthBirdsHeadLanguage,s__SetOrClass)

s__instance(s__AbunLanguage,s__NorthBirdsHeadLanguage)

Languages.kif 13705-13705 Abun language is an instance of north birds head language
s__instance(s__MusicGenre,s__SetOrClass)

s__instance(s__Acapella,s__MusicGenre)

Music.kif 515-515 Acapella is an instance of music genre

Display limited to 25 items. Show next 25

Display limited to 25 items. Show next 25


Show simplified definition (without tree view)
Show simplified definition (with tree view)

Show without tree


Sigma web home      Suggested Upper Merged Ontology (SUMO) web home
Sigma version 3.0 is open source software produced by Articulate Software and its partners