Term Intersection : Welcome guest : log in
Home |  Graph |  ]  KB:  Language:   

Formal Language: 



Term 1: Term 2:

( ! [V__AGENT,V__CATALOG,V__TIMEINT,V__CLASS,V__PROCESSINSTANCE,V__PROCESS,V__OBJ] :
   ((s__offersAtTime(V__AGENT,V__CATALOG,V__TIMEINT)
     &
     s__catalogItem(V__CLASS,V__CATALOG)
   &
   s__subclass(V__CLASS,s__Object) &
   s__instance(V__PROCESSINSTANCE,V__PROCESS)
&
s__subclass(V__PROCESS,s__Process) &
s__instance(V__OBJ,V__CLASS)
&
s__patient(V__PROCESSINSTANCE,V__OBJ))
=>
s__capabilityDuring(V__PROCESS,s__agent__m,V__AGENT,V__TIMEINT))
)

Catalog.kif 136-145
No TPTP formula. May not be expressible in strict first order. Hotel.kif 780-801
No TPTP formula. May not be expressible in strict first order. Catalog.kif 64-75
( ! [V__CLASS,V__ROW1] :
   (s__disjointDecomposition_2(V__CLASS,V__ROW1)
   =>
   (! [V__ITEM] :
     (s__inList(V__ITEM,s__ListFn_1(V__ROW1))
   =>
   s__subclass(V__ITEM,V__CLASS))))
)

Merge.kif 3133-3138
( ! [V__DISEASE,V__SUBSTANCE,V__PROCESS,V__SUB] :
   ((s__diseaseTreatment(V__DISEASE,V__SUBSTANCE,V__PROCESS)
     &
     s__subclass(V__SUB,V__PROCESS))
=>
s__diseaseTreatment(V__DISEASE,V__SUBSTANCE,V__SUB))
)

WMD.kif 903-907
( ! [V__VIRUS] :
   (s__subclass(V__VIRUS,s__TickBorneEncephalitisVirus) =>
     (? [V__DISEASE] :
       (s__instance(V__DISEASE,s__TickBorneEncephalitis) &
         s__biochemicalAgentSyndrome(V__VIRUS,V__DISEASE))))
)

WMD.kif 1829-1834
No TPTP formula. May not be expressible in strict first order. Economy.kif 2586-2595
( ! [V__X,V__Y] :
   (s__subclass(V__X,V__Y)
   =>
   (s__instance(V__X,s__SetOrClass) &
     s__instance(V__Y,s__SetOrClass)))
)

Merge.kif 150-154
( ! [V__AGENT,V__CATALOG,V__CLASS] :
   ((s__offers(V__AGENT,V__CATALOG)
     &
     s__catalogItem(V__CLASS,V__CATALOG)
   &
   s__subclass(V__CLASS,s__Process))
=>
s__capability(V__CLASS,s__agent__m,V__AGENT))
)

Catalog.kif 87-92
( ! [V__ROOM,V__PROC,V__R,V__GUEST,V__HOTEL,V__P,V__S,V__PRICE] :
   ((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__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(0,s__UnitedStatesDollar)))))
)

Hotel.kif 394-411
( ! [V__REGION,V__TYPE] :
   ((s__vegetationType(V__REGION,V__TYPE)
     &
     s__subclass(V__TYPE,s__Plant) &
     s__instance(V__REGION,s__GeographicArea))
   =>
   (? [V__PLANT] :
     (s__instance(V__PLANT,V__TYPE)
     &
     s__located(V__PLANT,V__REGION))))
)

Geography.kif 5773-5781
( ! [V__SEAT,V__AUDITORIUM,V__STAGE,V__PERSON,V__SEE] :
   ((s__instance(V__SEAT,s__AuditoriumSeat) &
       s__part(V__SEAT,V__AUDITORIUM)
     &
     s__part(V__STAGE,V__AUDITORIUM)
   &
   s__instance(V__AUDITORIUM,s__Auditorium) &
   s__instance(V__STAGE,s__PerformanceStage) &
   s__located(V__PERSON,V__SEAT)
&
s__instance(V__PERSON,s__Human) &
s__subclass(V__SEE,s__Seeing) &
(! [V__INST] :
   (s__instance(V__INST,V__SEE)
   =>
   s__patient(V__INST,V__STAGE))))
=>
s__capability(V__SEE,s__agent__m,V__PERSON))
)

Mid-level-ontology.kif 7016-7030
( ! [V__DISEASE,V__PROCESS] :
   (s__diseaseTreatment(V__DISEASE,s__OralAntibiotic,V__PROCESS)
   =>
   s__subclass(V__PROCESS,s__Ingesting))
)

WMD.kif 1189-1191
( ! [V__AREA,V__MO,V__TEMP] :
   ((s__instance(V__AREA,s__SubtropicalDesertClimateZone) &
       s__subclass(V__MO,s__Month) &
       s__averageTemperatureForPeriod(V__AREA,V__MO,V__TEMP))
   =>
   s__greaterThan(V__TEMP,s__MeasureFn(18,s__CelsiusDegree)))
)

Geography.kif 1348-1353
No TPTP formula. May not be expressible in strict first order. Economy.kif 2171-2178
( ! [V__TOKEN,V__X] :
   (s__codeMapping(s__ISO_639_1,V__TOKEN,V__X)
   =>
   (s__instance(V__X,s__HumanLanguage) |
     s__subclass(V__X,s__HumanLanguage)))
)

Languages.kif 14683-14687
( ! [V__SEQ,V__CLASS] :
   ((s__instance(V__SEQ,s__SequenceFunction) &
       s__range(V__SEQ,V__CLASS))
   =>
   s__subclass(V__CLASS,s__Integer))
)

Merge.kif 3469-3473
( ! [V__X,V__Y,V__PRES,V__BOIL,V__TEMP] :
   ((s__instance(V__X,V__Y)
     &
     s__subclass(V__Y,s__PureSubstance) &
     s__barometricPressure(V__X,s__MeasureFn(V__PRES,s__InchMercury))
   &
   s__greaterThan(29.92,V__PRES)
&
s__boilingPoint(V__Y,s__MeasureFn(V__BOIL,s__KelvinDegree))
&
s__measure(V__X,s__MeasureFn(V__TEMP,s__KelvinDegree))
&
s__greaterThan(V__TEMP,V__BOIL))
=>
s__attribute(V__X,s__Gas))
)

Merge.kif 13729-13738
( ! [V__CH] :
   (s__instance(V__CH,s__Charcoal) =>
     (? [V__C,V__W] :
       (s__subclass(V__C,s__Combustion) &
         s__instance(V__W,s__Wood) &
         s__result(V__C,V__CH)
       &
       s__resource(V__C,V__W))))
)

Cars.kif 1669-1676
( ! [V__COIN] :
   (s__instance(V__COIN,s__CurrencyCoin) =>
     (? [V__METAL] :
       (s__subclass(V__METAL,s__Metal) &
         s__material(V__METAL,V__COIN))))
)

Mid-level-ontology.kif 4135-4140
No TPTP formula. May not be expressible in strict first order. Economy.kif 2281-2290
No TPTP formula. May not be expressible in strict first order. Economy.kif 2127-2134
( ! [V__REL,V__CLASS] :
   ((s__instance(V__REL,s__EconomicRelation) &
       s__domain(V__REL,1,V__CLASS))
   =>
   s__subclass(V__CLASS,s__GeopoliticalArea))
)

Mid-level-ontology.kif 14460-14464
( ! [V__TYPE,V__EVENT,V__REGION,V__OBJECT,V__PLACE] :
   ((s__subclass(V__TYPE,s__Process) &
       s__instance(V__EVENT,V__TYPE)
     &
     s__eventLocated(V__EVENT,V__REGION)
   &
   s__instance(s__attends__m,s__CaseRole) &
   s__instance(V__OBJECT,s__Object) &
   s__instance(V__REGION,s__GeographicArea) &
   s__attends(V__EVENT,V__OBJECT))
=>
s__capableAtLocation(V__TYPE,s__attends__m,V__OBJECT,V__PLACE))
)

Transportation.kif 2606-2615
( ! [V__ROOM,V__PROC,V__R,V__GUEST,V__HOTEL,V__P,V__S] :
   ((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__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(0,s__UnitedStatesDollar),V__HOTEL))
)

Hotel.kif 350-363
( ! [V__REM,V__DEATH,V__ORG,V__ORGTYPE] :
   ((s__instance(V__REM,s__OrganicObject) &
       s__instance(V__DEATH,s__Death) &
       s__experiencer(V__DEATH,V__ORG)
     &
     s__instance(V__ORG,V__ORGTYPE)
   &
   s__subclass(V__ORG,s__Organism) &
   s__result(V__DEATH,V__REM))
=>
s__instance(V__REM,s__DeadFn(V__ORGTYPE)))
)

Mid-level-ontology.kif 251-259
No TPTP formula. May not be expressible in strict first order. Mid-level-ontology.kif 11141-11152
( ! [V__ROOM,V__OBJ] :
   ((s__roomAmenity(V__ROOM,V__OBJ)
     &
     s__subclass(V__OBJ,s__Object))
   =>
   (! [V__R] :
     (s__instance(V__R,V__ROOM)
     =>
     (? [V__O] :
       (s__instance(V__R,V__ROOM)
       &
       s__instance(V__O,V__OBJ)
     &
     s__located(V__O,V__R))))))
)

Hotel.kif 276-287
No TPTP formula. May not be expressible in strict first order. Hotel.kif 495-510
( ! [V__AREA,V__MO,V__TEMP] :
   ((s__instance(V__AREA,s__DesertClimateZone) &
       s__subclass(V__MO,s__Month) &
       s__averageTemperatureForPeriod(V__AREA,V__MO,V__TEMP)
     &
     s__greaterThan(V__TEMP,s__MeasureFn(18,s__CelsiusDegree)))
=>
s__instance(V__AREA,s__SubtropicalDesertClimateZone))
)

Geography.kif 1340-1346
( ! [V__X,V__Y,V__MELT,V__PRES,V__TEMP] :
   ((s__instance(V__X,V__Y)
     &
     s__subclass(V__Y,s__PureSubstance) &
     s__meltingPoint(V__Y,s__MeasureFn(V__MELT,s__KelvinDegree))
   &
   s__barometricPressure(V__X,s__MeasureFn(V__PRES,s__InchMercury))
&
s__greaterThan(V__PRES,29.92)
&
s__measure(V__X,s__MeasureFn(V__TEMP,s__KelvinDegree))
&
s__lessThan(V__TEMP,V__MELT))
=>
s__attribute(V__X,s__Solid))
)

Merge.kif 13751-13760
No TPTP formula. May not be expressible in strict first order. Merge.kif 15446-15453
No TPTP formula. May not be expressible in strict first order. Media.kif 1902-1906
No TPTP formula. May not be expressible in strict first order. Catalog.kif 339-355
( ! [V__AREA] :
   (s__instance(V__AREA,s__ColdClimateZone) =>
     (? [V__MO,V__AMOUNT] :
       (s__subclass(V__MO,s__Month) &
         s__averageTemperatureForPeriod(V__AREA,V__MO,V__AMOUNT)
       &
       s__lessThan(V__AMOUNT,s__MeasureFn(-3,s__CelsiusDegree)))))
)

Geography.kif 1481-1487
( ! [V__M] :
   (s__instance(V__M,s__Meat) =>
     (? [V__DA,V__AC] :
       (s__instance(V__DA,s__DeadFn(V__AC))
     &
     s__part(V__M,V__DA)
   &
   s__subclass(V__AC,s__Animal))))
)

Food.kif 304-310
( ! [V__PROCESS,V__PROCESS_CLASS,V__ACCESSING,V__AGENT,V__TIMETOFIRST] :
   ((s__instance(V__PROCESS,V__PROCESS_CLASS)
     &
     s__subclass(V__PROCESS_CLASS,s__Process) &
     s__instance(V__ACCESSING,s__AccessingWebPage) &
     s__instance(V__AGENT,s__Agent) &
     s__agent(V__PROCESS,V__AGENT)
   &
   s__agent(V__ACCESSING,V__AGENT)
&
s__during(V__PROCESS,V__ACCESSING)
&
s__instance(V__TIMETOFIRST,s__TimeInterval) &
(~ (? [V__PROCESS2] :
   (s__instance(V__PROCESS2,V__PROCESS_CLASS)
   &
   s__agent(V__PROCESS2,V__AGENT)
&
s__during(V__PROCESS2,V__ACCESSING)
&
s__before(s__BeginFn(s__WhenFn(V__PROCESS2))
,s__BeginFn(s__WhenFn(V__PROCESS))))))
&
(s__BeginFn(s__WhenFn(V__ACCESSING))
= s__BeginFn(s__WhenFn(V__TIMETOFIRST)))
&
(s__BeginFn(s__WhenFn(V__PROCESS))
= s__EndFn(s__WhenFn(V__TIMETOFIRST))))
=>
(s__TTFxFn(V__PROCESS_CLASS,V__ACCESSING)
= V__TIMETOFIRST))
)

UXExperimentalTerms.kif 1703-1725
( ! [V__ROBOT,V__LENGTHLIMIT,V__INSTANCE,V__OBJECT,V__LENGTH,V__WIDTH,V__HEIGHT,V__RADIUS] :
   ((s__lengthLimit(V__ROBOT,V__LENGTHLIMIT)
     &
     s__instance(V__INSTANCE,V__OBJECT)
   &
   s__subclass(V__OBJECT,s__Object) &
   ((s__defaultMaximumLength(V__OBJECT,V__LENGTH)
     &
     s__defaultMaximumWidth(V__OBJECT,V__WIDTH)
   &
   s__defaultMaximumHeight(V__OBJECT,V__HEIGHT))
|
((s__greaterThan(V__LENGTH,V__LENGTHLIMIT)
&
s__greaterThan(V__WIDTH,V__LENGTHLIMIT))
|
(s__greaterThan(V__LENGTH,V__LENGTHLIMIT)
&
s__greaterThan(V__HEIGHT,V__LENGTHLIMIT))
|
(s__greaterThan(V__WIDTH,V__LENGTHLIMIT)
&
s__greaterThan(V__HEIGHT,V__LENGTHLIMIT)))
|
(s__defaultMaximumSphereRadius(V__OBJECT,V__RADIUS)
&
s__greaterThan(s__MultiplicationFn(V__RADIUS,2)
,s__DivisionFn(V__LENGTHLIMIT,2)))))
=>
(~ s__canCarry(V__ROBOT,V__INSTANCE)))
)

Robot.kif 54-78
( ! [V__TYPE,V__EVENT,V__PLACE] :
   ((s__subclass(V__TYPE,s__WaterVehicle) &
       s__instance(V__EVENT,s__TransportationFn(V__TYPE))
   &
   s__eventLocated(V__EVENT,V__PLACE))
=>
s__instance(V__PLACE,s__WaterArea))
)

Transportation.kif 2221-2226
( ! [V__BUSINESS,V__TYPE,V__GENUS] :
   ((s__organizationProductType(V__BUSINESS,V__TYPE)
     &
     s__subclass(V__TYPE,V__GENUS))
=>
s__organizationProductType(V__BUSINESS,V__GENUS))
)

Economy.kif 1631-1635
( ! [V__DISEASE,V__PROCESS] :
   (s__diseaseTreatment(V__DISEASE,s__TopicalAntibiotic,V__PROCESS)
   =>
   s__subclass(V__PROCESS,s__Covering))
)

WMD.kif 1216-1218
( ! [V__MENU,V__MEMB] :
   (s__instance(V__MENU,s__AlcoholMenu) =>
     (! [V__X] :
       (s__catalogItem(V__X,V__MENU)
       =>
       s__subclass(V__MEMB,s__AlcoholicBeverage))))
)

Dining.kif 217-222
( ! [V__RESEARCH] :
   (s__instance(V__RESEARCH,s__ResearchingWeaponOfMassDestruction) =>
     (? [V__WEAPON] :
       (s__subclass(V__WEAPON,s__WeaponOfMassDestruction) &
         s__refers(V__RESEARCH,V__WEAPON))))
)

WMD.kif 718-723
( ! [V__AGENT,V__CLASS] :
   ((s__authors(V__AGENT,V__CLASS)
     &
     s__subclass(V__CLASS,s__MusicalComposition))
   =>
   s__composer(V__AGENT,V__CLASS))
)

Media.kif 1853-1857
( ! [V__PRED1,V__PRED2,V__CLASS] :
   ((s__subrelation(V__PRED1,V__PRED2)
     &
     s__instance(V__PRED2,V__CLASS)
   &
   s__subclass(V__CLASS,s__InheritableRelation))
=>
s__instance(V__PRED1,V__CLASS))
)

Merge.kif 221-226
( ! [V__PLATFORM,V__PARTY] :
   ((s__subclass(V__PLATFORM,s__PartyPlatform) &
       s__authors(V__PARTY,V__PLATFORM)
     &
     s__instance(V__PARTY,s__Organization))
   =>
   s__instance(V__PARTY,s__PoliticalParty))
)

Government.kif 2271-2276
( ! [V__GEO,V__TYPE,V__AREA] :
   ((s__instance(V__GEO,s__GeographicPartTypeFn(V__TYPE,V__AREA))
   &
   s__subclass(V__TYPE,s__GeopoliticalArea) &
   s__instance(V__AREA,s__GeopoliticalArea))
=>
s__geopoliticalSubdivision(V__GEO,V__AREA))
)

Geography.kif 6254-6259
( ! [V__CLASS,V__TYPE,V__AREA] :
   ((V__CLASS = s__GeographicPartTypeFn(V__TYPE,V__AREA))
   =>
   s__subclass(V__CLASS,V__TYPE))
)

Geography.kif 6244-6246
( ! [V__HOLIDAY,V__DAY,V__MONTH,V__YEAR,V__DATE,V__LATER_YEAR] :
   ((s__commemoratesDate(V__HOLIDAY,s__DayFn(V__DAY,s__MonthFn(V__MONTH,s__YearFn(V__YEAR))))
&
s__instance(V__DATE,V__HOLIDAY)
&
s__subclass(V__HOLIDAY,s__FixedHoliday) &
s__lessThanOrEqualTo(V__YEAR,V__LATER_YEAR))
=>
s__instance(V__DATE,s__DayFn(V__DAY,s__MonthFn(V__MONTH,s__YearFn(V__LATER_YEAR)))))
)

Government.kif 613-619
( ! [V__ENTITY,V__CLASS] :
   (s__immediateInstance(V__ENTITY,V__CLASS)
   =>
   (~ (? [V__SUBCLASS] :
       (s__subclass(V__SUBCLASS,V__CLASS)
       &
       (~ (V__SUBCLASS = V__CLASS))
       &
       s__instance(V__ENTITY,V__SUBCLASS)))))
)

Merge.kif 104-110
( ! [V__GRAPH] :
   (s__instance(V__GRAPH,s__Graph) =>
     s__subclass(s__MinimalCutSetFn(V__GRAPH)
  ,s__CutSetFn(V__GRAPH)))
)

Merge.kif 6205-6207
( ! [V__CS1,V__CLASS,V__ECLASS,V__N,V__G,V__E] :
   ((s__instance(V__CS1,V__CLASS)
     &
     s__subclass(V__CLASS,s__CompoundSubstance) &
     (~ (? [V__CS2] :
         (s__instance(V__CS2,V__CLASS)
         &
         s__part(V__CS2,V__CS1))))
&
s__molecularRatio(V__ECLASS,V__N,V__CLASS)
&
s__instance(V__G,s__Group) &
s__member(V__E,V__G)
&
s__part(V__E,V__CS1)
&
s__instance(V__E,V__ECLASS))
=>
s__memberCount(V__G,V__N))
)

Cars.kif 1767-1781
( ! [V__S] :
   (s__instance(V__S,s__Seafood) =>
     (? [V__DA,V__F] :
       (s__instance(V__DA,s__DeadFn(V__F))
     &
     s__part(V__S,V__DA)
   &
   s__subclass(V__F,s__Fish))))
)

Food.kif 864-870
( ! [V__AREA,V__TYPE] :
   ((s__naturalHazardTypeInArea(V__AREA,V__TYPE)
     &
     s__subclass(V__TYPE,s__Process))
   =>
   (? [V__ITEM] :
     (s__instance(V__ITEM,V__TYPE)
     &
     s__located(V__ITEM,V__AREA)
   &
   s__overlapsTemporally(s__WhenFn(V__ITEM)
,s__WhenFn(V__AREA)))))
)

Geography.kif 2215-2223
( ! [V__MENU,V__MEMB] :
   (s__instance(V__MENU,s__BeverageMenu) =>
     (! [V__X] :
       (s__catalogItem(V__X,V__MENU)
       =>
       s__subclass(V__MEMB,s__Beverage))))
)

Dining.kif 205-210
( ! [V__MENU,V__MEMB] :
   (s__instance(V__MENU,s__WineMenu) =>
     (! [V__X] :
       (s__catalogItem(V__X,V__MENU)
       =>
       s__subclass(V__MEMB,s__WineMenu))))
)

Dining.kif 229-234
No TPTP formula. May not be expressible in strict first order. Cars.kif 3452-3478
( ! [V__CATALOG] :
   (s__instance(V__CATALOG,s__Catalog) =>
     (? [V__X] :
       (s__subclass(V__X,s__Agent) &
         s__offers(V__X,V__CATALOG))))
)

Catalog.kif 36-41
( ! [V__AREA,V__MO,V__TEMP] :
   ((s__instance(V__AREA,s__PolarClimateZone) &
       s__subclass(V__MO,s__Month) &
       s__averageTemperatureForPeriod(V__AREA,V__MO,V__TEMP))
   =>
   s__greaterThan(s__MeasureFn(10,s__CelsiusDegree),V__TEMP))
)

Geography.kif 1511-1516
( ! [V__OBJECTTYPE,V__OBJECT,V__PART] :
   ((s__subclass(V__OBJECTTYPE,s__Substance) &
       s__instance(V__OBJECT,V__OBJECTTYPE)
     &
     s__part(V__PART,V__OBJECT))
=>
s__instance(V__PART,V__OBJECTTYPE))
)

Merge.kif 1068-1073
No TPTP formula. May not be expressible in strict first order. Economy.kif 2597-2604
No TPTP formula. May not be expressible in strict first order. Government.kif 2278-2285
No TPTP formula. May not be expressible in strict first order. Economy.kif 2160-2169
( ! [V__ARTIFACT1,V__ARTIFACT2] :
   (s__version(V__ARTIFACT1,V__ARTIFACT2)
   =>
   s__subclass(V__ARTIFACT1,V__ARTIFACT2))
)

Merge.kif 15786-15788
No TPTP formula. May not be expressible in strict first order. Mid-level-ontology.kif 15975-15996
No TPTP formula. May not be expressible in strict first order. Economy.kif 2116-2125
No TPTP formula. May not be expressible in strict first order. Catalog.kif 357-372
( ! [V__REL,V__NUMBER,V__CLASS1,V__CLASS2] :
   ((s__domainSubclass(V__REL,V__NUMBER,V__CLASS1)
     &
     s__domainSubclass(V__REL,V__NUMBER,V__CLASS2))
=>
(s__subclass(V__CLASS1,V__CLASS2)
|
s__subclass(V__CLASS2,V__CLASS1)))
)

Merge.kif 275-281
( ! [V__AREA] :
   (s__instance(V__AREA,s__TemperateClimateZone) =>
     (? [V__MO,V__AMOUNT] :
       (s__subclass(V__MO,s__Month) &
         s__averageTemperatureForPeriod(V__AREA,V__MO,V__AMOUNT)
       &
       s__greaterThan(V__AMOUNT,s__MeasureFn(10,s__CelsiusDegree)))))
)

Geography.kif 1373-1379
( ! [V__CLASS1,V__OBJCLASS1,V__CLASS2,V__OBJCLASS2] :
   (((V__CLASS1 = s__ReceivingAnObjectFn(V__OBJCLASS1))
     &
     (V__CLASS2 = s__ReceivingAnObjectFn(V__OBJCLASS2))
   &
   s__subclass(V__OBJCLASS1,V__OBJCLASS2))
=>
s__subclass(V__CLASS1,V__CLASS2))
)

Media.kif 195-200
No TPTP formula. May not be expressible in strict first order. Economy.kif 2206-2215
( ! [V__REL,V__NUMBER,V__CLASS1,V__CLASS2] :
   ((s__domain(V__REL,V__NUMBER,V__CLASS1)
     &
     s__domain(V__REL,V__NUMBER,V__CLASS2))
=>
(s__subclass(V__CLASS1,V__CLASS2)
|
s__subclass(V__CLASS2,V__CLASS1)))
)

Merge.kif 249-255
( ! [V__X,V__Y,V__Z] :
   ((s__subclass(V__X,V__Y)
     &
     s__instance(V__Z,V__X))
=>
s__instance(V__Z,V__Y))
)

Merge.kif 156-160
( ! [V__CLASS1,V__CLASS2,V__INTERSECT] :
   (s__classIntersection(V__CLASS1,V__CLASS2,V__INTERSECT)
   =>
   (s__subclass(V__INTERSECT,V__CLASS1)
   &
   s__subclass(V__INTERSECT,V__CLASS2)))
)

ComputerInput.kif 73-77
( ! [V__ARG1,V__ARG2,V__PROC] :
   ((s__instance(s__eventPartlyLocated__m,s__CaseRole) &
       s__eventPartlyLocated(V__ARG1,V__ARG2)
     &
     s__instance(V__ARG1,V__PROC)
   &
   s__subclass(V__PROC,s__Process))
=>
s__capability(V__PROC,s__eventPartlyLocated__m,V__ARG2))
)

Merge.kif 4026-4032
No TPTP formula. May not be expressible in strict first order. Media.kif 1896-1900
No TPTP formula. May not be expressible in strict first order. Catalog.kif 278-293
No TPTP formula. May not be expressible in strict first order. Cars.kif 3416-3446
No TPTP formula. May not be expressible in strict first order. Mid-level-ontology.kif 28110-28139
( ! [V__T] :
   (s__instance(V__T,s__Truck) =>
     (? [V__L] :
       (s__subclass(V__L,s__Object) &
         s__cargoType(V__T,V__L))))
)

Transportation.kif 1956-1961
( ! [V__TEAM] :
   (s__instance(V__TEAM,s__SportsTeam) =>
     (? [V__SPORT] :
       (s__subclass(V__SPORT,s__Sport) &
         s__capability(V__SPORT,s__agent__m,V__TEAM))))
)

Mid-level-ontology.kif 7236-7241
( ! [V__OBJ,V__ROLE,V__EVENT,V__CLASS,V__TIME,V__PLACE] :
   ((s__playsRoleInEvent(V__OBJ,V__ROLE,V__EVENT)
     &
     s__instance(V__EVENT,V__CLASS)
   &
   s__subclass(V__CLASS,s__Process) &
   s__time(V__EVENT,V__TIME)
&
s__eventLocated(V__EVENT,V__PLACE))
=>
s__playsRoleInEventOfType(V__OBJ,V__ROLE,V__CLASS,V__TIME,V__PLACE))
)

Mid-level-ontology.kif 21133-21140
( ! [V__X] :
   (s__subclass(V__X,s__UniformClothing) =>
     (? [V__GRP] :
       s__hasUniform(V__GRP,V__X)))
)

Mid-level-ontology.kif 24741-24744
No TPTP formula. May not be expressible in strict first order. Catalog.kif 322-337
( ! [V__X,V__CLASS,V__I,V__ATTR] :
   ((s__subclass(V__X,V__CLASS)
     &
     s__instance(V__I,V__X)
   &
   s__instance(V__ATTR,s__Attribute))
=>
(s__property(V__I,V__ATTR)
=>
(V__X = s__AttrFn(V__CLASS,V__ATTR))))
)

Merge.kif 1834-1842
( ! [V__C] :
   (s__instance(V__C,s__ElectricalConductor) =>
     (? [V__S] :
       (s__subclass(V__S,s__ConductorSubstance) &
         s__material(V__S,V__C))))
)

engineering.kif 820-825
( ! [V__AGENT,V__ORGANISM,V__SUB] :
   ((s__biologicalAgentCarrier(V__AGENT,V__ORGANISM)
     &
     s__subclass(V__SUB,V__ORGANISM))
=>
s__biologicalAgentCarrier(V__AGENT,V__SUB))
)

WMD.kif 922-926
No TPTP formula. May not be expressible in strict first order. Media.kif 1914-1918
No TPTP formula. May not be expressible in strict first order. Hotel.kif 310-324
( ! [V__CLASS] :
   (s__instance(V__CLASS,s__Class) <=>
     s__subclass(V__CLASS,s__Entity))
   )

Merge.kif 854-856
( ! [V__AREA,V__MO,V__TEMP] :
   ((s__instance(V__AREA,s__GeographicArea) &
       s__subclass(V__MO,s__Month) &
       s__averageTemperatureForPeriod(V__AREA,V__MO,V__TEMP)
     &
     s__greaterThan(s__MeasureFn(10,s__CelsiusDegree),V__TEMP))
=>
s__instance(V__AREA,s__PolarClimateZone))
)

Geography.kif 1518-1524
( ! [V__ROBOT,V__INSTANCE,V__OBJECT,V__WIDTHLIMIT,V__LENGTH,V__WIDTH,V__HEIGHT,V__RADIUS] :
   ((s__instance(V__ROBOT,s__CarryBot) &
       s__instance(V__INSTANCE,V__OBJECT)
     &
     s__subclass(V__OBJECT,s__Object) &
     s__widthLimit(V__ROBOT,V__WIDTHLIMIT)
   &
   ((s__defaultMaximumLength(V__OBJECT,V__LENGTH)
     &
     s__defaultMaximumWidth(V__OBJECT,V__WIDTH)
   &
   s__defaultMaximumHeight(V__OBJECT,V__HEIGHT)
&
s__greaterThan(V__LENGTH,V__WIDTHLIMIT)
&
s__greaterThan(V__WIDTH,V__WIDTHLIMIT)
&
s__greaterThan(V__HEIGHT,V__WIDTHLIMIT))
|
(s__defaultMaximumSphereRadius(V__OBJECT,V__RADIUS)
&
s__greaterThan(s__MultiplicationFn(V__RADIUS,2)
,V__WIDTHLIMIT))))
=>
(~ s__canCarry(V__ROBOT,V__INSTANCE)))
)

Robot.kif 27-45
( ! [V__BUSINESS,V__TYPE,V__GENUS] :
   ((s__organizationServiceType(V__BUSINESS,V__TYPE)
     &
     s__subclass(V__TYPE,V__GENUS))
=>
s__organizationServiceType(V__BUSINESS,V__GENUS))
)

Economy.kif 1671-1675
( ! [V__O,V__L] :
   (s__habitatOfOrganism(V__O,V__L)
   =>
   (~ s__subclass(V__O,s__DomesticAnimal)))
)

Mid-level-ontology.kif 28453-28456
( ! [V__CLASS1,V__CLASS2] :
   (s__immediateSubclass(V__CLASS1,V__CLASS2)
   =>
   (~ (? [V__CLASS3] :
       (s__subclass(V__CLASS3,V__CLASS2)
       &
       s__subclass(V__CLASS1,V__CLASS3)
     &
     (~ (V__CLASS2 = V__CLASS3))
     &
     (~ (V__CLASS1 = V__CLASS3))))))
)

Merge.kif 176-183
( ! [V__REL,V__CLASS1,V__CLASS2] :
   ((s__rangeSubclass(V__REL,V__CLASS1)
     &
     s__rangeSubclass(V__REL,V__CLASS2))
=>
(s__subclass(V__CLASS1,V__CLASS2)
|
s__subclass(V__CLASS2,V__CLASS1)))
)

Merge.kif 389-395
No TPTP formula. May not be expressible in strict first order. Media.kif 1890-1894
No TPTP formula. May not be expressible in strict first order. Cars.kif 3499-3521
( ! [V__DOCTOR] :
   (s__attribute(V__DOCTOR,s__MedicalDoctor) =>
     (? [V__PROCESS1,V__PROCESS2] :
       (s__subclass(V__PROCESS1,s__DiagnosticProcess) &
         s__subclass(V__PROCESS2,s__TherapeuticProcess) &
         s__capability(V__PROCESS1,s__agent__m,V__DOCTOR)
       &
       s__capability(V__PROCESS2,s__agent__m,V__DOCTOR))))
)

Mid-level-ontology.kif 18657-18664
( ! [V__REL,V__CLASS1,V__CLASS2] :
   ((s__range(V__REL,V__CLASS1)
     &
     s__range(V__REL,V__CLASS2))
=>
(s__subclass(V__CLASS1,V__CLASS2)
|
s__subclass(V__CLASS2,V__CLASS1)))
)

Merge.kif 360-366
( ! [V__UNIT,V__NUMBER1,V__STATE,V__NUMBER2] :
   ((s__subclass(V__UNIT,s__AreaMeasure) &
       s__measure(s__Alaska,s__MeasureFn(V__NUMBER1,V__UNIT))
   &
   s__measure(V__STATE,s__MeasureFn(V__NUMBER2,V__UNIT))
&
s__instance(V__STATE,s__AmericanState) &
(~ (s__Alaska = V__STATE)))
=>
s__lessThan(V__NUMBER2,V__NUMBER1))
)

CountriesAndRegions.kif 871-878
No TPTP formula. May not be expressible in strict first order. Merge.kif 15480-15489
( ! [V__AREA,V__TYPE] :
   ((s__instance(V__AREA,V__TYPE)
     &
     s__subclass(V__TYPE,s__ClimateZone))
   =>
   s__climateTypeInArea(V__AREA,V__TYPE))
)

Geography.kif 1242-1246
( ! [V__ROOM,V__HOTELUNIT] :
   ((s__attribute(V__ROOM,s__Oversized) &
       s__immediateInstance(V__ROOM,V__HOTELUNIT)
     &
     s__subclass(V__HOTELUNIT,s__HotelUnit))
   =>
   (? [V__NORMAL,V__AREA1,V__AREA2] :
     (s__immediateInstance(V__NORMAL,V__HOTELUNIT)
     &
     s__measure(V__NORMAL,V__AREA1)
   &
   s__measure(V__ROOM,V__AREA2)
&
s__instance(V__AREA1,s__AreaMeasure) &
s__instance(V__AREA2,s__AreaMeasure) &
s__greaterThan(V__AREA2,V__AREA1))))
)

Hotel.kif 1136-1148
( ! [V__DISEASE,V__SUBSTANCE,V__PROCESS,V__SUB] :
   ((s__diseaseTreatment(V__DISEASE,V__SUBSTANCE,V__PROCESS)
     &
     s__subclass(V__SUB,V__SUBSTANCE))
=>
s__diseaseTreatment(V__DISEASE,V__SUB,V__PROCESS))
)

WMD.kif 909-913
( ! [V__AGENT,V__CATALOG,V__CLASS,V__PROCESSINST,V__PROCESS,V__OBJ] :
   ((s__offers(V__AGENT,V__CATALOG)
     &
     s__catalogItem(V__CLASS,V__CATALOG)
   &
   s__subclass(V__CLASS,s__Object) &
   s__instance(V__PROCESSINST,V__PROCESS)
&
s__subclass(V__PROCESS,s__Process) &
s__instance(V__OBJ,V__CLASS)
&
s__patient(V__PROCESSINST,V__OBJ))
=>
s__capability(V__PROCESS,s__agent__m,V__AGENT))
)

Catalog.kif 97-106
( ! [V__ROBOT,V__MASSLIMIT,V__INSTANCE,V__OBJECT,V__UNITOFMASS,V__NUM] :
   ((s__massLimit(V__ROBOT,V__MASSLIMIT)
     &
     s__instance(V__INSTANCE,V__OBJECT)
   &
   s__subclass(V__OBJECT,s__Object) &
   s__instance(V__UNITOFMASS,s__UnitOfMass) &
   s__defaultMaximumMeasure(V__OBJECT,s__MeasureFn(V__NUM,V__UNITOFMASS))
&
s__greaterThan(V__NUM,V__MASSLIMIT))
=>
(~ s__canCarry(V__ROBOT,V__INSTANCE)))
)

Robot.kif 86-95
( ! [V__STRING,V__PRODUCTTYPE,V__LANGUAGE] :
   (s__groupingTitle(V__STRING,V__PRODUCTTYPE,V__LANGUAGE)
   =>
   s__subclass(V__PRODUCTTYPE,s__Collection))
)

Media.kif 3118-3120
( ! [V__FROG] :
   (s__secretesToxin(V__FROG,s__Batrachotoxin) =>
     s__subclass(V__FROG,s__Amphibian))
   )

WMD.kif 313-315
No TPTP formula. May not be expressible in strict first order. Cars.kif 3357-3386
( ! [V__PAPER,V__WEEK] :
   ((s__subclass(V__PAPER,s__Newspaper) &
       s__instance(V__WEEK,s__Week))
     =>
     (? [V__PUBLICATION,V__ISSUE] :
       (s__instance(V__PUBLICATION,s__Publication) &
         s__temporalPart(s__WhenFn(V__PUBLICATION)
      ,V__WEEK)
     &
     s__result(V__PUBLICATION,V__ISSUE)
   &
   s__instance(V__ISSUE,V__PAPER))))
)

Mid-level-ontology.kif 12533-12542
( ! [V__I] :
   (s__instance(V__I,s__ResistorElement) =>
     (? [V__S] :
       (s__subclass(V__S,s__InsulatorSubstance) &
         s__material(V__S,V__I))))
)

engineering.kif 849-854
( ! [V__AGENT,V__PROCESS,V__SUB] :
   ((s__biochemicalAgentDelivery(V__AGENT,V__PROCESS)
     &
     s__subclass(V__SUB,V__PROCESS))
=>
s__biochemicalAgentDelivery(V__AGENT,V__SUB))
)

WMD.kif 783-787
No TPTP formula. May not be expressible in strict first order. Hotel.kif 289-308
No TPTP formula. May not be expressible in strict first order. Economy.kif 2217-2224
( ! [V__PROGRAM,V__EPISODE,V__NUMBER] :
   ((s__subclass(V__PROGRAM,s__NewsProgram) &
       (V__EPISODE = s__SeriesVolumeFn(V__PROGRAM,V__NUMBER)))
   =>
   (? [V__DISSEMINATE] :
     (s__instance(V__DISSEMINATE,s__Disseminating) &
       s__patient(V__DISSEMINATE,V__EPISODE))))
)

Mid-level-ontology.kif 12350-12357
( ! [V__place,V__type,V__mover] :
   ((s__trafficableForTrafficType(V__place,V__type)
     &
     s__subclass(V__type,s__Agent) &
     s__instance(V__mover,V__type))
=>
s__capableAtLocation(s__Translocation,s__agent__m,V__mover,V__place))
)

Transportation.kif 2531-2536
No TPTP formula. May not be expressible in strict first order. Media.kif 1908-1912
( ! [V__ROOM,V__OBJ,V__R,V__GUEST,V__HOTEL,V__O,V__P] :
   ((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(0,s__UnitedStatesDollar),V__HOTEL))
)

Hotel.kif 333-348
( ! [V__OBJ] :
   (s__instance(V__OBJ,s__CorpuscularObject) =>
     (? [V__SUBSTANCE1,V__SUBSTANCE2] :
       (s__subclass(V__SUBSTANCE1,s__Substance) &
         s__subclass(V__SUBSTANCE2,s__Substance) &
         s__material(V__SUBSTANCE1,V__OBJ)
       &
       s__material(V__SUBSTANCE2,V__OBJ)
     &
     (~ (V__SUBSTANCE1 = V__SUBSTANCE2)))))
)

Merge.kif 1255-1263
No TPTP formula. May not be expressible in strict first order. Catalog.kif 51-62
( ! [V__AREA,V__MO,V__TEMP] :
   ((s__instance(V__AREA,s__ColdClimateZone) &
       s__subclass(V__MO,s__Month) &
       s__averageTemperatureForPeriod(V__AREA,V__MO,V__TEMP))
   =>
   s__greaterThan(s__MeasureFn(10,s__CelsiusDegree),V__TEMP))
)

Geography.kif 1474-1479
( ! [V__CHILD,V__PARENT,V__CLASS] :
   ((s__parent(V__CHILD,V__PARENT)
     &
     s__subclass(V__CLASS,s__Organism) &
     s__instance(V__PARENT,V__CLASS))
=>
s__instance(V__CHILD,V__CLASS))
)

Merge.kif 16554-16559
No TPTP formula. May not be expressible in strict first order. Economy.kif 1984-1993
( ! [V__CF] :
   (s__instance(V__CF,s__CharcoalFilter) =>
     (? [V__C] :
       (s__subclass(V__C,s__Charcoal) &
         s__material(V__C,V__CF))))
)

Cars.kif 1683-1688
No TPTP formula. May not be expressible in strict first order. Economy.kif 2292-2299
( ! [V__ARTIFACT] :
   (s__instance(V__ARTIFACT,s__GameArtifact) =>
     (? [V__GAME] :
       (s__subclass(V__GAME,s__Game) &
         s__capability(V__GAME,s__instrument__m,V__ARTIFACT))))
)

Mid-level-ontology.kif 14536-14541
( ! [V__AGENT1,V__PERSON,V__AGENT2,V__PROCESS1,V__CLASS,V__PROCESS2,V__TIME1,V__TIME2] :
   ((s__subjectiveAttribute(V__AGENT1,s__Quick,V__PERSON)
     &
     s__subjectiveAttribute(V__AGENT2,s__Slow,V__PERSON)
   &
   s__instance(V__PROCESS1,V__CLASS)
&
s__instance(V__PROCESS2,V__CLASS)
&
s__subclass(V__CLASS,s__Process) &
s__agent(V__PROCESS1,V__AGENT1)
&
s__agent(V__PROCESS2,V__AGENT2))
=>
(s__duration(s__WhenFn(V__PROCESS1)
,V__TIME1)
&
s__duration(s__WhenFn(V__PROCESS2)
,V__TIME2)
&
s__greaterThan(V__TIME2,V__TIME1)))
)

Dining.kif 1001-1013
( ! [V__X,V__CLASS,V__ATTR] :
   ((V__X = s__AttrFn(V__CLASS,V__ATTR))
   =>
   (! [V__I] :
     (s__instance(V__I,V__X)
     =>
     (s__instance(V__I,V__CLASS)
     &
     s__subclass(V__X,V__CLASS)
   &
   s__property(V__I,V__ATTR)))))
)

Merge.kif 1823-1832
( ! [V__WATER,V__TYPE,V__RIVER] :
   ((s__instance(V__WATER,s__River) &
       s__trafficableForTrafficType(V__WATER,V__TYPE)
     &
     s__subclass(V__TYPE,s__WaterVehicle))
   =>
   s__instance(V__RIVER,s__Waterway))
)

Transportation.kif 1626-1631
( ! [V__MENU] :
   (s__instance(V__MENU,s__Menu) =>
     (! [V__X] :
       (s__catalogItem(V__X,V__MENU)
       =>
       s__subclass(V__X,s__FoodForFn(s__Human)))))
)

Dining.kif 181-186
No TPTP formula. May not be expressible in strict first order. Hotel.kif 477-493
( ! [V__AGENT] :
   ((s__instance(V__AGENT,s__Agent) &
       s__subclass(s__ElectionFn(V__AGENT)
    ,s__Election))
   =>
   (s__instance(V__AGENT,s__Organization) |
     s__instance(V__AGENT,s__GeopoliticalArea)))
)

Government.kif 1652-1658
( ! [V__NUMBER,V__CLASS,V__ROW1] :
   ((s__domainSubclass(s__contraryAttribute__m,V__NUMBER,V__CLASS)
     &
     s__instance(s__contraryAttribute__m,s__Predicate) &
     s__contraryAttribute_1(V__ROW1))
=>
s__subclass(s__ListOrderFn(s__ListFn_1(V__ROW1)
,V__NUMBER)
,V__CLASS))
)

Merge.kif 3190-3195
( ! [V__TEXT,V__INT1,V__VOLUME1,V__INT2,V__VOLUME2,V__PUB1,V__PUB2,V__CBO1,V__CBO2,V__DATE1,V__DATE2] :
   ((s__subclass(V__TEXT,s__Periodical) &
       (s__SeriesVolumeFn(V__TEXT,V__INT1)
       = V__VOLUME1)
     &
     (s__SeriesVolumeFn(V__TEXT,V__INT2)
     = V__VOLUME2)
   &
   s__greaterThan(V__INT2,V__INT1)
&
s__instance(V__PUB1,s__Publication) &
s__instance(V__PUB2,s__Publication) &
s__instance(V__CBO1,V__VOLUME1)
&
s__instance(V__CBO2,V__VOLUME2)
&
s__patient(V__PUB1,V__CBO1)
&
s__patient(V__PUB2,V__CBO2)
&
s__date(V__PUB1,V__DATE1)
&
s__date(V__PUB2,V__DATE2))
=>
s__before(s__EndFn(V__DATE1)
,s__EndFn(V__DATE2)))
)

Mid-level-ontology.kif 12368-12382
( ! [V__MV,V__WC,V__COUNT,V__WEAPON,V__PC,V__ROLE] :
   ((s__weaponCarryingCapability(V__MV,V__WC,V__COUNT)
     &
     s__instance(V__WEAPON,V__WC)
   &
   s__capability(V__PC,V__ROLE,V__WEAPON)
&
(s__subclass(V__PC,s__Shooting) |
   s__subclass(V__PC,s__Damaging)))
=>
s__capability(V__PC,V__ROLE,V__MV))
)

MilitaryDevices.kif 35-43
( ! [V__X,V__Y,V__BOIL,V__MELT,V__TEMP] :
   ((s__instance(V__X,V__Y)
     &
     s__subclass(V__Y,s__PureSubstance) &
     s__boilingPoint(V__Y,s__MeasureFn(V__BOIL,s__KelvinDegree))
   &
   s__meltingPoint(V__Y,s__MeasureFn(V__MELT,s__KelvinDegree))
&
s__measure(V__X,s__MeasureFn(V__TEMP,s__KelvinDegree))
&
s__greaterThan(V__TEMP,V__MELT)
&
s__lessThan(V__TEMP,V__BOIL))
=>
s__attribute(V__X,s__Liquid))
)

Merge.kif 13740-13749
No TPTP formula. May not be expressible in strict first order. Economy.kif 1995-2002
( ! [V__AGENT,V__CATALOG,V__TIMEINT,V__CLASS] :
   ((s__offersAtTime(V__AGENT,V__CATALOG,V__TIMEINT)
     &
     s__catalogItem(V__CLASS,V__CATALOG)
   &
   s__subclass(V__CLASS,s__Process))
=>
s__capabilityDuring(V__CLASS,s__agent__m,V__AGENT,V__TIMEINT))
)

Catalog.kif 129-134
( ! [V__AREA,V__CLAIM] :
   ((s__instance(V__AREA,s__LandlockedArea) &
       s__subclass(V__CLAIM,s__MaritimeClaimArea))
     =>
     (~ s__maritimeClaimType(V__AREA,V__CLAIM)))
)

Geography.kif 969-973
( ! [V__TYPE,V__TRIP] :
   ((s__subclass(V__TYPE,s__TransportationDevice) &
       s__subclass(s__TransportationFn(V__TYPE)
    ,s__Transportation) &
     s__instance(V__TRIP,s__TransportationFn(V__TYPE)))
=>
(? [V__VEHICLE] :
(s__instance(V__VEHICLE,V__TYPE)
&
s__instrument(V__TRIP,V__VEHICLE))))
)

Transportation.kif 1515-1523
( ! [V__AREA,V__TYPE,V__POLITY] :
   ((s__instance(V__AREA,V__TYPE)
     &
     s__subclass(V__TYPE,s__MaritimeClaimArea) &
     s__claimedTerritory(V__AREA,V__POLITY))
=>
s__maritimeClaimType(V__POLITY,V__TYPE))
)

Geography.kif 984-989
( ! [V__SPECIES] :
   (s__instance(V__SPECIES,s__BiologicalSpecies) =>
     s__subclass(V__SPECIES,s__Organism))
   )

Mid-level-ontology.kif 8881-8883
( ! [V__PC,V__ROLE,V__MV] :
   ((s__capability(V__PC,V__ROLE,V__MV)
     &
     s__subclass(V__PC,s__Shooting))
   =>
   (? [V__WEAPON] :
     (s__instance(V__WEAPON,s__Weapon) &
       s__part(V__WEAPON,V__MV)
     &
     s__capability(V__PC,V__ROLE,V__WEAPON))))
)

MilitaryDevices.kif 48-56
( ! [V__AREA] :
   (s__instance(V__AREA,s__TemperateClimateZone) =>
     (? [V__MO,V__AMOUNT] :
       (s__subclass(V__MO,s__Month) &
         s__averageTemperatureForPeriod(V__AREA,V__MO,V__AMOUNT)
       &
       s__greaterThanOrEqualTo(V__AMOUNT,s__MeasureFn(-3,s__CelsiusDegree))
     &
     s__lessThanOrEqualTo(V__AMOUNT,s__MeasureFn(18,s__CelsiusDegree)))))
)

Geography.kif 1388-1395
( ! [V__FUNCTION,V__CLASS,V__ROW1,V__VALUE] :
   ((s__rangeSubclass(V__FUNCTION,V__CLASS)
     &
     (s__AssignmentFn_2(V__FUNCTION,V__ROW1)
     = V__VALUE))
=>
s__subclass(V__VALUE,V__CLASS))
)

Merge.kif 377-381
( ! [V__PUB,V__TEXT] :
   ((s__instance(V__PUB,s__Publication) &
       s__patient(V__PUB,V__TEXT))
   =>
   s__subclass(V__TEXT,s__Text))
)

Merge.kif 12718-12722
( ! [V__INDUSTRY,V__MEMB1,V__MEMB2] :
   (s__instance(V__INDUSTRY,s__Industry) =>
     ((s__member(V__MEMB1,V__INDUSTRY)
       &
       s__member(V__MEMB2,V__INDUSTRY))
   =>
   (? [V__CLASS] :
     (s__subclass(V__CLASS,s__Corporation) &
       s__immediateInstance(V__MEMB1,V__CLASS)
     &
     s__immediateInstance(V__MEMB2,V__CLASS)))))
)

Mid-level-ontology.kif 12715-12725
( ! [V__AREA,V__MO,V__TEMP] :
   ((s__instance(V__AREA,s__TemperateClimateZone) &
       s__subclass(V__MO,s__Month) &
       s__averageTemperatureForPeriod(V__AREA,V__MO,V__TEMP))
   =>
   s__greaterThanOrEqualTo(V__TEMP,s__MeasureFn(-3,s__CelsiusDegree)))
)

Geography.kif 1381-1386
( ! [V__ROOM,V__OBJ,V__R,V__GUEST,V__HOTEL,V__O,V__P,V__PRICE] :
   ((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(0,s__UnitedStatesDollar)))))
)

Hotel.kif 372-392
( ! [V__AREA,V__MO,V__TEMP] :
   ((s__instance(V__AREA,s__TropicalClimateZone) &
       s__subclass(V__MO,s__Month) &
       s__instance(V__AREA,s__GeographicArea) &
       s__averageTemperatureForPeriod(V__AREA,V__MO,V__TEMP))
   =>
   s__greaterThan(V__TEMP,s__MeasureFn(18,s__CelsiusDegree)))
)

Geography.kif 1264-1270
( ! [V__AREA,V__TYPE] :
   ((s__maritimeClaimType(V__AREA,V__TYPE)
     &
     s__subclass(V__TYPE,s__MaritimeClaimArea))
   =>
   (? [V__CLAIM] :
     (s__instance(V__CLAIM,V__TYPE)
     &
     s__claimedTerritory(V__CLAIM,V__AREA))))
)

Geography.kif 975-982
( ! [V__REGION,V__TYPE] :
   (((~ s__vegetationType(V__REGION,V__TYPE))
     &
     s__subclass(V__TYPE,s__Plant) &
     s__instance(V__REGION,s__GeographicArea))
   =>
   (~ (? [V__PLANT] :
       (s__instance(V__PLANT,V__TYPE)
       &
       s__located(V__PLANT,V__REGION)))))
)

Geography.kif 5782-5790
No TPTP formula. May not be expressible in strict first order. Mid-level-ontology.kif 11112-11123
No TPTP formula. May not be expressible in strict first order. Mid-level-ontology.kif 27827-27836
( ! [V__AREA,V__TYPE] :
   ((s__naturalHazardTypeInArea(V__AREA,V__TYPE)
     &
     s__subclass(V__TYPE,s__Object))
   =>
   (? [V__ITEM] :
     (s__instance(V__ITEM,V__TYPE)
     &
     s__located(V__ITEM,V__AREA))))
)

Geography.kif 2206-2213
( ! [V__PLACE,V__TYPE,V__MOVER] :
   ((s__trafficableForTrafficType(V__PLACE,V__TYPE)
     &
     s__subclass(V__TYPE,s__TransportationDevice) &
     s__instance(V__MOVER,V__TYPE))
=>
s__capableAtLocation(s__Transportation,s__instrument__m,V__MOVER,V__PLACE))
)

Transportation.kif 2524-2529
( ! [V__A3,V__CURRENCY,V__A2,V__AREA] :
   ((s__codeMapping(s__ISO_4217_A,V__A3,V__CURRENCY)
     &
     s__codeMapping(s__ISO_3166_1_alpha_2,V__A2,V__AREA)
   &
   s__subclass(V__AREA,s__GeopoliticalArea) &
   (V__A2 = s__SubstringFn(V__A3,0,2)))
=>
s__currencyType(V__AREA,V__CURRENCY))
)

Media.kif 2859-2865
No TPTP formula. May not be expressible in strict first order. Catalog.kif 262-276
(? [V__T] :
   (s__subclass(V__T,s__HandToolBox) &
     s__manufacturer(s__SortimoCorp,V__T)))

Cars.kif 5080-5083


Sigma web home      Suggested Upper Merged Ontology (SUMO) web home
Sigma version 2.99c (>= 2017/11/20) is open source software produced by Articulate Software and its partners