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

Formal Language: 



KB Term:  Term intersection
English Word: 

  Region

Sigma KEE - Region
Region(region)Abraham's_bosom, Annwfn, Annwn, Antarctic_Circle, Appleton_layer, Aquarius, Aquarius_the_Water_Bearer, Archer, Arctic_Circle, Aries, Aries_the_Ram, Asgard, Balance, Brobdingnag, Bull, Cancer, Cancer_the_Crab, Capricorn, Capricorn_the_Goat, Celestial_City, City_of_God, Cockaigne, Crab, D-layer, D_region, E_layer, E_region, Earth, Eden, Edgeworth-Kuiper_belt, El_Dorado, Elysian_Fields, Elysium, F_layer, F_region, Fish, GHQ, Garden_of_Eden, Gehenna, Gemini, Gemini_the_Twins, Goat, Green_Line, Greenwich_Meridian, Hades, Heaven, Heavenly_City, Heaviside_layer, Hell, Holy_City...

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


s__documentation(s__Region,s__ChineseLanguage,'这是一个地理位置。 Region 包括 Object 的表面、虚构的 地方 和 GeographicArea 。注:Region 是唯一能够定位于作自身的 Object 。 另外要注意的是 Region 不是 SelfConnectedObject 的子类别, 因为有一些 Region ,像群岛有些 part 跟其他部分 不 connected 。')

Merge.kif 1284-1287
s__documentation(s__Region,s__EnglishLanguage,'A topographic location. Regions encompass surfaces of Objects, imaginary places, and GeographicAreas. Note that a Region is the only kind of Object which can be located at itself. Note too that Region is not a subclass of SelfConnectedObject, because some Regions, e.g. archipelagos, have parts which are not connected with one another.')

Merge.kif 1278-1283
s__partition__3(s__Region,s__GeographicArea,s__SpaceRegion)

Mid-level-ontology.kif 8698-8698 Region is exhaustively partitioned into geographic area and space region
s__subclass(s__Region,s__Object)

s__instance(s__Object,s__SetOrClass)

s__instance(s__Region,s__SetOrClass)

Merge.kif 1277-1277 Region is a subclass of object

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


s__range(s__FlowRegionFn__m,s__Region)

Geography.kif 4598-4598 The range of flow region is an instance of region
s__range(s__InnerBoundaryFn__m,s__Region)

Geography.kif 789-789 The range of inner boundary is an instance of region
s__range(s__LatitudeFn__m,s__Region)

Geography.kif 410-410 The range of latitude is an instance of region
s__range(s__OuterBoundaryFn__m,s__Region)

Geography.kif 801-801 The range of outer boundary is an instance of region
s__range(s__WhereFn__m,s__Region)

Merge.kif 4362-4362 The range of where is an instance of region
s__instance(s__Atmosphere,s__SetOrClass)

s__instance(s__Region,s__SetOrClass)

s__subclass(s__Atmosphere,s__Region)

Weather.kif 10-10 Atmosphere is a subclass of region
s__instance(s__DiningArea,s__SetOrClass)

s__instance(s__Region,s__SetOrClass)

s__subclass(s__DiningArea,s__Region)

Mid-level-ontology.kif 13247-13247 Dining area is a subclass of region
s__subclass(s__FlowRegion,s__Region)

s__instance(s__Region,s__SetOrClass)

s__instance(s__FlowRegion,s__SetOrClass)

Mid-level-ontology.kif 8762-8762 Flow region is a subclass of region
s__instance(s__GeographicArea,s__SetOrClass)

s__subclass(s__GeographicArea,s__Region)

s__instance(s__Region,s__SetOrClass)

Merge.kif 14028-14028 Geographic area is a subclass of region
s__instance(s__Region,s__SetOrClass)

s__instance(s__Hole,s__SetOrClass)

s__subclass(s__Hole,s__Region)

Merge.kif 9875-9875 Hole is a subclass of region
s__instance(s__HydrophilicSide,s__SetOrClass)

s__subclass(s__HydrophilicSide,s__Region)

s__instance(s__Region,s__SetOrClass)

VirusProteinAndCellPart.kif 424-424 Hydrophilic side is a subclass of region
s__instance(s__HydrophobicSide,s__SetOrClass)

s__subclass(s__HydrophobicSide,s__Region)

s__instance(s__Region,s__SetOrClass)

VirusProteinAndCellPart.kif 413-413 Hydrophobic side is a subclass of region
s__instance(s__Indoors,s__SetOrClass)

s__subclass(s__Indoors,s__Region)

s__instance(s__Region,s__SetOrClass)

Mid-level-ontology.kif 8866-8866 Indoors is a subclass of region
s__instance(s__Region,s__SetOrClass)

s__subclass(s__KitchenArea,s__Region)

s__instance(s__KitchenArea,s__SetOrClass)

Mid-level-ontology.kif 13223-13223 Kitchen area is a subclass of region
s__instance(s__Latitude,s__SetOrClass)

s__subclass(s__Latitude,s__Region)

s__instance(s__Region,s__SetOrClass)

Geography.kif 302-302 Latitude is a subclass of region
s__instance(s__Longitude,s__SetOrClass)

s__instance(s__Region,s__SetOrClass)

s__subclass(s__Longitude,s__Region)

Geography.kif 311-311 Longitude is a subclass of region
s__subclass(s__Outdoors,s__Region)

s__instance(s__Outdoors,s__SetOrClass)

s__instance(s__Region,s__SetOrClass)

Mid-level-ontology.kif 8854-8854 Outdoors is a subclass of region
s__instance(s__ParkingRegion,s__SetOrClass)

s__subclass(s__ParkingRegion,s__Region)

s__instance(s__Region,s__SetOrClass)

TransportDetail.kif 31-31 Parking area is a subclass of region
s__instance(s__Patio,s__SetOrClass)

s__subclass(s__Patio,s__Region)

s__instance(s__Region,s__SetOrClass)

Mid-level-ontology.kif 24725-24725 Patio is a subclass of region
s__subclass(s__PerimeterArea,s__Region)

s__instance(s__PerimeterArea,s__SetOrClass)

s__instance(s__Region,s__SetOrClass)

Geography.kif 754-754 Perimeter area is a subclass of region
s__subclass(s__PlayArea,s__Region)

s__instance(s__PlayArea,s__SetOrClass)

s__instance(s__Region,s__SetOrClass)

Dining.kif 939-939 Playground is a subclass of region
s__instance(s__Region,s__SetOrClass)

s__instance(s__RealEstate,s__SetOrClass)

s__subclass(s__RealEstate,s__Region)

FinancialOntology.kif 1296-1296 Real estate is a subclass of region
s__subclass(s__Road,s__Region)

s__instance(s__Road,s__SetOrClass)

s__instance(s__Region,s__SetOrClass)

Mid-level-ontology.kif 20045-20045 Road is a subclass of region
s__instance(s__SittingArea,s__SetOrClass)

s__instance(s__Region,s__SetOrClass)

s__subclass(s__SittingArea,s__Region)

Mid-level-ontology.kif 13210-13210 Sitting area is a subclass of region
s__subclass(s__SpaceRegion,s__Region)

s__instance(s__Region,s__SetOrClass)

s__instance(s__SpaceRegion,s__SetOrClass)

Mid-level-ontology.kif 8786-8786 Space region is a subclass of region

Display limited to 25 items. Show next 25

Display limited to 25 items. Show next 25

appearance as argument number 3
-------------------------


s__domain(s__InnerBoundaryFn__m,1,s__Region)

Geography.kif 788-788 The number 1 argument of inner boundary is an instance of region
s__domain(s__MaritimeClaimsTerritorialSeaFn__m,1,s__Region)

Geography.kif 773-773 The number 1 argument of maritime claims territorial sea is an instance of region
s__domain(s__MealAttributeFn__m,2,s__Region)

Food.kif 294-294 The number 2 argument of meal attribute function is an instance of region
s__domain(s__OuterBoundaryFn__m,1,s__Region)

Geography.kif 800-800 The number 1 argument of outer boundary is an instance of region
s__domain(s__PerimeterAreaFn__m,1,s__Region)

Geography.kif 761-761 The number 1 argument of perimeter area is an instance of region
s__domain(s__VelocityFn__m,3,s__Region)

Merge.kif 6882-6882 The number 3 argument of velocity is an instance of region
s__domain(s__areaOfOperation__m,1,s__Region)

MilitaryProcesses.kif 1302-1302 The number 1 argument of area of operation is an instance of region
s__domain(s__baptismplace__m,2,s__Region)

Biography.kif 78-78 The number 2 argument of baptismplace is an instance of region
s__domain(s__canonicalPlaceName__m,1,s__Region)

Mid-level-ontology.kif 22371-22371 The number 1 argument of canonicalPlaceName is an instance of region
s__domain(s__capableAtLocation__m,4,s__Region)

Transportation.kif 2631-2631 The number 4 argument of capable at location is an instance of region
s__domain(s__capacityByArrangement__m,1,s__Region)

Hotel.kif 755-755 The number 1 argument of capacity by arrangement is an instance of region
s__domain(s__cloudCoverFraction__m,1,s__Region)

Weather.kif 482-482 The number 1 argument of cloud cover fraction is an instance of region
s__domain(s__daylightHoursInterval__m,1,s__Region)

Weather.kif 462-462 The number 1 argument of daylight hours interval is an instance of region
s__domain(s__daylightHoursTotal__m,1,s__Region)

Weather.kif 472-472 The number 1 argument of daylight hours total is an instance of region
s__domain(s__highTide__m,1,s__Region)

Geography.kif 4677-4677 The number 1 argument of highTide is an instance of region
s__domain(s__lowTide__m,1,s__Region)

Geography.kif 4686-4686 The number 1 argument of lowTide is an instance of region
s__domain(s__mapOfArea__m,1,s__Region)

Geography.kif 524-524 The number 1 argument of map of area is an instance of region
s__domain(s__providesDestination__m,2,s__Region)

Transportation.kif 3340-3340 The number 2 argument of provides destination is an instance of region
s__domain(s__routeBetween__m,2,s__Region)

Transportation.kif 2848-2848 The number 2 argument of route between is an instance of region
s__domain(s__routeBetween__m,3,s__Region)

Transportation.kif 2849-2849 The number 3 argument of route between is an instance of region
s__domain(s__routeEnd__m,1,s__Region)

Transportation.kif 2718-2718 The number 1 argument of routeEnd is an instance of region
s__domain(s__routeStart__m,1,s__Region)

Transportation.kif 2695-2695 The number 1 argument of routeStart is an instance of region
s__domain(s__totalArea__m,1,s__Region)

Geography.kif 535-535 The number 1 argument of total area is an instance of region
s__domain(s__visibilityInMeteorology__m,1,s__Region)

Weather.kif 1108-1108 The number 1 argument of visibility in meteorology is an instance of region

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


No TPTP formula. May not be expressible in strict first order. Weather.kif 1086-1096 An entity is an instance of region and the entity has an 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__REGION]
   ((s__exists__m[V__EMIT]
       (s__instance(V__EMIT,s__RadiatingLight)s__and__ms__patient(V__EMIT,V__REGION)
      s__and__ms__instance(V__REGION,s__Region)))
  s__<⇒
  s__attribute(V__REGION,s__Illuminated))
)

Merge.kif 13627-13633 There exists a process such that the process is an instance of radiating light and an object is a patient of the process and the object is an instance of region if and only if illuminated is an attribute of the object
( ∀ [V__I]
   ((s__attribute(V__I,s__Inhabited)s__and__ms__instance(V__I,s__Region))
    s__=>(s__exists__m[V__H]
       (s__instance(V__H,s__Human)s__and__ms__inhabits(V__H,V__I))))
)

Mid-level-ontology.kif 28278-28285
( ∀ [V__U]
   ((s__attribute(V__U,s__Uninhabited)s__and__ms__instance(V__U,s__Region))
    s__=>(s__not__m(s__exists__m[V__H]
       (s__instance(V__H,s__Human)s__and__ms__inhabits(V__H,V__U)))))
)

Mid-level-ontology.kif 28262-28270
( ∀ [V__ROW5,V__ROW6,V__ROW3,V__ROW4,V__ROW1,V__ROW2,V__DIRECTION,V__NUM]
   ((s__instance(V__ROW5,s__AngleMeasure)s__and__ms__instance(V__ROW6,s__AngleMeasure)s__and__ms__instance(V__ROW3,s__AngleMeasure)s__and__ms__instance(V__ROW4,s__AngleMeasure)s__and__ms__instance(V__ROW1,s__AngleMeasure)s__and__ms__instance(V__ROW2,s__AngleMeasure)s__and__ms__instance(V__DIRECTION,s__DirectionalAttribute)s__and__ms__instance(V__NUM,s__RealNumber))
    s__=>((s__instance(s__LatitudeFn__7Fn(V__DIRECTION,V__ROW1,V__ROW2,V__ROW3,V__ROW4,V__ROW5,V__ROW6)
      ,s__Region)s__and__m(s__ListOrderFn(s__ListFn__6Fn(V__ROW1,V__ROW2,V__ROW3,V__ROW4,V__ROW5,V__ROW6)
    ,1)
  s__equal__ms__MeasureFn(V__NUM,s__AngularDegree)))
s__=>s__lessThanOrEqualTo(V__NUM,90)))
)

( ∀ [V__ROW5,V__ROW3,V__ROW4,V__ROW1,V__ROW2,V__DIRECTION,V__NUM]
   ((s__instance(V__ROW5,s__AngleMeasure)s__and__ms__instance(V__ROW3,s__AngleMeasure)s__and__ms__instance(V__ROW4,s__AngleMeasure)s__and__ms__instance(V__ROW1,s__AngleMeasure)s__and__ms__instance(V__ROW2,s__AngleMeasure)s__and__ms__instance(V__DIRECTION,s__DirectionalAttribute)s__and__ms__instance(V__NUM,s__RealNumber))
    s__=>((s__instance(s__LatitudeFn__6Fn(V__DIRECTION,V__ROW1,V__ROW2,V__ROW3,V__ROW4,V__ROW5)
      ,s__Region)s__and__m(s__ListOrderFn(s__ListFn__5Fn(V__ROW1,V__ROW2,V__ROW3,V__ROW4,V__ROW5)
    ,1)
  s__equal__ms__MeasureFn(V__NUM,s__AngularDegree)))
s__=>s__lessThanOrEqualTo(V__NUM,90)))
)

( ∀ [V__ROW3,V__ROW1,V__ROW2,V__DIRECTION,V__NUM]
   ((s__instance(V__ROW3,s__AngleMeasure)s__and__ms__instance(V__ROW1,s__AngleMeasure)s__and__ms__instance(V__ROW2,s__AngleMeasure)s__and__ms__instance(V__DIRECTION,s__DirectionalAttribute)s__and__ms__instance(V__NUM,s__RealNumber))
    s__=>((s__instance(s__LatitudeFn__4Fn(V__DIRECTION,V__ROW1,V__ROW2,V__ROW3)
      ,s__Region)s__and__m(s__ListOrderFn(s__ListFn__3Fn(V__ROW1,V__ROW2,V__ROW3)
    ,1)
  s__equal__ms__MeasureFn(V__NUM,s__AngularDegree)))
s__=>s__lessThanOrEqualTo(V__NUM,90)))
)

( ∀ [V__ROW1,V__DIRECTION,V__NUM]
   ((s__instance(V__ROW1,s__AngleMeasure)s__and__ms__instance(V__DIRECTION,s__DirectionalAttribute)s__and__ms__instance(V__NUM,s__RealNumber))
    s__=>((s__instance(s__LatitudeFn__2Fn(V__DIRECTION,V__ROW1)
      ,s__Region)s__and__m(s__ListOrderFn(s__ListFn__1Fn(V__ROW1)
    ,1)
  s__equal__ms__MeasureFn(V__NUM,s__AngularDegree)))
s__=>s__lessThanOrEqualTo(V__NUM,90)))
)

( ∀ [V__ROW7,V__ROW5,V__ROW6,V__ROW3,V__ROW4,V__ROW1,V__ROW2,V__DIRECTION,V__NUM]
   ((s__instance(V__ROW7,s__AngleMeasure)s__and__ms__instance(V__ROW5,s__AngleMeasure)s__and__ms__instance(V__ROW6,s__AngleMeasure)s__and__ms__instance(V__ROW3,s__AngleMeasure)s__and__ms__instance(V__ROW4,s__AngleMeasure)s__and__ms__instance(V__ROW1,s__AngleMeasure)s__and__ms__instance(V__ROW2,s__AngleMeasure)s__and__ms__instance(V__DIRECTION,s__DirectionalAttribute)s__and__ms__instance(V__NUM,s__RealNumber))
    s__=>((s__instance(s__LatitudeFn__8Fn(V__DIRECTION,V__ROW1,V__ROW2,V__ROW3,V__ROW4,V__ROW5,V__ROW6,V__ROW7)
      ,s__Region)s__and__m(s__ListOrderFn(s__ListFn__7Fn(V__ROW1,V__ROW2,V__ROW3,V__ROW4,V__ROW5,V__ROW6,V__ROW7)
    ,1)
  s__equal__ms__MeasureFn(V__NUM,s__AngularDegree)))
s__=>s__lessThanOrEqualTo(V__NUM,90)))
)

( ∀ [V__ROW3,V__ROW4,V__ROW1,V__ROW2,V__DIRECTION,V__NUM]
   ((s__instance(V__ROW3,s__AngleMeasure)s__and__ms__instance(V__ROW4,s__AngleMeasure)s__and__ms__instance(V__ROW1,s__AngleMeasure)s__and__ms__instance(V__ROW2,s__AngleMeasure)s__and__ms__instance(V__DIRECTION,s__DirectionalAttribute)s__and__ms__instance(V__NUM,s__RealNumber))
    s__=>((s__instance(s__LatitudeFn__5Fn(V__DIRECTION,V__ROW1,V__ROW2,V__ROW3,V__ROW4)
      ,s__Region)s__and__m(s__ListOrderFn(s__ListFn__4Fn(V__ROW1,V__ROW2,V__ROW3,V__ROW4)
    ,1)
  s__equal__ms__MeasureFn(V__NUM,s__AngularDegree)))
s__=>s__lessThanOrEqualTo(V__NUM,90)))
)

( ∀ [V__ROW1,V__ROW2,V__DIRECTION,V__NUM]
   ((s__instance(V__ROW1,s__AngleMeasure)s__and__ms__instance(V__ROW2,s__AngleMeasure)s__and__ms__instance(V__DIRECTION,s__DirectionalAttribute)s__and__ms__instance(V__NUM,s__RealNumber))
    s__=>((s__instance(s__LatitudeFn__3Fn(V__DIRECTION,V__ROW1,V__ROW2)
      ,s__Region)s__and__m(s__ListOrderFn(s__ListFn__2Fn(V__ROW1,V__ROW2)
    ,1)
  s__equal__ms__MeasureFn(V__NUM,s__AngularDegree)))
s__=>s__lessThanOrEqualTo(V__NUM,90)))
)

Geography.kif 427-431
( ∀ [V__ROW7,V__ROW5,V__ROW6,V__ROW3,V__ROW4,V__ROW1,V__ROW2,V__DIRECTION,V__NUM]
   ((s__instance(V__ROW7,s__AngleMeasure)s__and__ms__instance(V__ROW5,s__AngleMeasure)s__and__ms__instance(V__ROW6,s__AngleMeasure)s__and__ms__instance(V__ROW3,s__AngleMeasure)s__and__ms__instance(V__ROW4,s__AngleMeasure)s__and__ms__instance(V__ROW1,s__AngleMeasure)s__and__ms__instance(V__ROW2,s__AngleMeasure)s__and__ms__instance(V__DIRECTION,s__DirectionalAttribute)s__and__ms__instance(V__NUM,s__RealNumber))
    s__=>((s__instance(s__LongitudeFn__8Fn(V__DIRECTION,V__ROW1,V__ROW2,V__ROW3,V__ROW4,V__ROW5,V__ROW6,V__ROW7)
      ,s__Region)s__and__m(s__ListOrderFn(s__ListFn__7Fn(V__ROW1,V__ROW2,V__ROW3,V__ROW4,V__ROW5,V__ROW6,V__ROW7)
    ,1)
  s__equal__ms__MeasureFn(V__NUM,s__AngularDegree)))
s__=>s__lessThanOrEqualTo(V__NUM,180)))
)

( ∀ [V__ROW3,V__ROW4,V__ROW1,V__ROW2,V__DIRECTION,V__NUM]
   ((s__instance(V__ROW3,s__AngleMeasure)s__and__ms__instance(V__ROW4,s__AngleMeasure)s__and__ms__instance(V__ROW1,s__AngleMeasure)s__and__ms__instance(V__ROW2,s__AngleMeasure)s__and__ms__instance(V__DIRECTION,s__DirectionalAttribute)s__and__ms__instance(V__NUM,s__RealNumber))
    s__=>((s__instance(s__LongitudeFn__5Fn(V__DIRECTION,V__ROW1,V__ROW2,V__ROW3,V__ROW4)
      ,s__Region)s__and__m(s__ListOrderFn(s__ListFn__4Fn(V__ROW1,V__ROW2,V__ROW3,V__ROW4)
    ,1)
  s__equal__ms__MeasureFn(V__NUM,s__AngularDegree)))
s__=>s__lessThanOrEqualTo(V__NUM,180)))
)

( ∀ [V__ROW1,V__ROW2,V__DIRECTION,V__NUM]
   ((s__instance(V__ROW1,s__AngleMeasure)s__and__ms__instance(V__ROW2,s__AngleMeasure)s__and__ms__instance(V__DIRECTION,s__DirectionalAttribute)s__and__ms__instance(V__NUM,s__RealNumber))
    s__=>((s__instance(s__LongitudeFn__3Fn(V__DIRECTION,V__ROW1,V__ROW2)
      ,s__Region)s__and__m(s__ListOrderFn(s__ListFn__2Fn(V__ROW1,V__ROW2)
    ,1)
  s__equal__ms__MeasureFn(V__NUM,s__AngularDegree)))
s__=>s__lessThanOrEqualTo(V__NUM,180)))
)

( ∀ [V__ROW3,V__ROW1,V__ROW2,V__DIRECTION,V__NUM]
   ((s__instance(V__ROW3,s__AngleMeasure)s__and__ms__instance(V__ROW1,s__AngleMeasure)s__and__ms__instance(V__ROW2,s__AngleMeasure)s__and__ms__instance(V__DIRECTION,s__DirectionalAttribute)s__and__ms__instance(V__NUM,s__RealNumber))
    s__=>((s__instance(s__LongitudeFn__4Fn(V__DIRECTION,V__ROW1,V__ROW2,V__ROW3)
      ,s__Region)s__and__m(s__ListOrderFn(s__ListFn__3Fn(V__ROW1,V__ROW2,V__ROW3)
    ,1)
  s__equal__ms__MeasureFn(V__NUM,s__AngularDegree)))
s__=>s__lessThanOrEqualTo(V__NUM,180)))
)

( ∀ [V__ROW1,V__DIRECTION,V__NUM]
   ((s__instance(V__ROW1,s__AngleMeasure)s__and__ms__instance(V__DIRECTION,s__DirectionalAttribute)s__and__ms__instance(V__NUM,s__RealNumber))
    s__=>((s__instance(s__LongitudeFn__2Fn(V__DIRECTION,V__ROW1)
      ,s__Region)s__and__m(s__ListOrderFn(s__ListFn__1Fn(V__ROW1)
    ,1)
  s__equal__ms__MeasureFn(V__NUM,s__AngularDegree)))
s__=>s__lessThanOrEqualTo(V__NUM,180)))
)

( ∀ [V__ROW5,V__ROW6,V__ROW3,V__ROW4,V__ROW1,V__ROW2,V__DIRECTION,V__NUM]
   ((s__instance(V__ROW5,s__AngleMeasure)s__and__ms__instance(V__ROW6,s__AngleMeasure)s__and__ms__instance(V__ROW3,s__AngleMeasure)s__and__ms__instance(V__ROW4,s__AngleMeasure)s__and__ms__instance(V__ROW1,s__AngleMeasure)s__and__ms__instance(V__ROW2,s__AngleMeasure)s__and__ms__instance(V__DIRECTION,s__DirectionalAttribute)s__and__ms__instance(V__NUM,s__RealNumber))
    s__=>((s__instance(s__LongitudeFn__7Fn(V__DIRECTION,V__ROW1,V__ROW2,V__ROW3,V__ROW4,V__ROW5,V__ROW6)
      ,s__Region)s__and__m(s__ListOrderFn(s__ListFn__6Fn(V__ROW1,V__ROW2,V__ROW3,V__ROW4,V__ROW5,V__ROW6)
    ,1)
  s__equal__ms__MeasureFn(V__NUM,s__AngularDegree)))
s__=>s__lessThanOrEqualTo(V__NUM,180)))
)

( ∀ [V__ROW5,V__ROW3,V__ROW4,V__ROW1,V__ROW2,V__DIRECTION,V__NUM]
   ((s__instance(V__ROW5,s__AngleMeasure)s__and__ms__instance(V__ROW3,s__AngleMeasure)s__and__ms__instance(V__ROW4,s__AngleMeasure)s__and__ms__instance(V__ROW1,s__AngleMeasure)s__and__ms__instance(V__ROW2,s__AngleMeasure)s__and__ms__instance(V__DIRECTION,s__DirectionalAttribute)s__and__ms__instance(V__NUM,s__RealNumber))
    s__=>((s__instance(s__LongitudeFn__6Fn(V__DIRECTION,V__ROW1,V__ROW2,V__ROW3,V__ROW4,V__ROW5)
      ,s__Region)s__and__m(s__ListOrderFn(s__ListFn__5Fn(V__ROW1,V__ROW2,V__ROW3,V__ROW4,V__ROW5)
    ,1)
  s__equal__ms__MeasureFn(V__NUM,s__AngularDegree)))
s__=>s__lessThanOrEqualTo(V__NUM,180)))
)

Geography.kif 467-471
( ∀ [V__OP,V__REGION]
   ((s__instance(V__OP,s__MilitaryOperation)s__and__ms__eventLocated(V__OP,V__REGION)
    s__and__ms__instance(V__REGION,s__Region))
  s__=>s__areaOfOperation(V__REGION,V__OP))
)

MilitaryProcesses.kif 1314-1319
( ∀ [V__X]
   ((s__instance(V__X,s__Region)s__and__ms__attribute(V__X,s__Vacuum))
    s__=>(s__not__m(s__exists__m[V__O]
       (s__instance(V__O,s__Object)s__and__ms__located(V__O,V__X)))))
)

Cars.kif 368-376
( ∀ [V__ONE,V__TWO]
   (s__instance(V__ONE,s__Object)s__=>((s__overlapsSpatially(V__ONE,V__TWO)
      s__and__ms__instance(V__TWO,s__Region)s__and__m(s__not__m(V__ONEs__equal__mV__TWO)))
  s__=>s__partlyLocated(V__ONE,V__TWO)))
)

Geography.kif 3342-3347
( ∀ [V__A,V__Distance,V__Area,V__D2,V__Time,V__Observe,V__B]
   ((s__instance(V__A,s__Agent)s__and__ms__instance(V__Distance,s__LengthMeasure)s__and__ms__instance(V__Area,s__Region)s__and__ms__instance(V__D2,s__LengthMeasure))
    s__=>((s__visibilityInMeteorology(V__Area,V__Time,V__Distance)
      s__and__ms__instance(V__Time,s__NightTime)s__and__ms__instance(V__Observe,s__Looking)s__and__ms__instance(V__B,s__Region)s__and__ms__attribute(V__B,s__Illuminated)s__and__ms__measure(V__B,s__MeasureFn(1000,s__Candela))
    s__and__ms__agent(V__Observe,V__A)
  s__and__ms__patient(V__Observe,V__B)
s__and__ms__orientation(V__A,V__B,s__Horizontal)s__and__ms__eventLocated(V__Observe,V__Area)
s__and__ms__during(s__WhenFn(V__Observe)
,V__Time)
s__and__ms__instance(V__B,s__Object))
s__=>(s__distance(V__A,V__B,V__D2)
s__and__ms__greaterThan(V__Distance,V__D2))))
)

Weather.kif 1155-1172
( ∀ [V__ROW1,V__DIRECTION]
   ((s__instance(V__ROW1,s__AngleMeasure)s__and__ms__instance(V__DIRECTION,s__DirectionalAttribute))
    s__=>(s__instance(s__LatitudeFn__2Fn(V__DIRECTION,V__ROW1)
    ,s__Region)s__=>((V__DIRECTIONs__equal__ms__North)s__or__m(V__DIRECTIONs__equal__ms__South))))
   )

( ∀ [V__ROW3,V__ROW4,V__ROW1,V__ROW2,V__DIRECTION]
   ((s__instance(V__ROW3,s__AngleMeasure)s__and__ms__instance(V__ROW4,s__AngleMeasure)s__and__ms__instance(V__ROW1,s__AngleMeasure)s__and__ms__instance(V__ROW2,s__AngleMeasure)s__and__ms__instance(V__DIRECTION,s__DirectionalAttribute))
    s__=>(s__instance(s__LatitudeFn__5Fn(V__DIRECTION,V__ROW1,V__ROW2,V__ROW3,V__ROW4)
    ,s__Region)s__=>((V__DIRECTIONs__equal__ms__North)s__or__m(V__DIRECTIONs__equal__ms__South))))
   )

( ∀ [V__ROW5,V__ROW6,V__ROW3,V__ROW4,V__ROW1,V__ROW2,V__DIRECTION]
   ((s__instance(V__ROW5,s__AngleMeasure)s__and__ms__instance(V__ROW6,s__AngleMeasure)s__and__ms__instance(V__ROW3,s__AngleMeasure)s__and__ms__instance(V__ROW4,s__AngleMeasure)s__and__ms__instance(V__ROW1,s__AngleMeasure)s__and__ms__instance(V__ROW2,s__AngleMeasure)s__and__ms__instance(V__DIRECTION,s__DirectionalAttribute))
    s__=>(s__instance(s__LatitudeFn__7Fn(V__DIRECTION,V__ROW1,V__ROW2,V__ROW3,V__ROW4,V__ROW5,V__ROW6)
    ,s__Region)s__=>((V__DIRECTIONs__equal__ms__North)s__or__m(V__DIRECTIONs__equal__ms__South))))
   )

( ∀ [V__ROW5,V__ROW3,V__ROW4,V__ROW1,V__ROW2,V__DIRECTION]
   ((s__instance(V__ROW5,s__AngleMeasure)s__and__ms__instance(V__ROW3,s__AngleMeasure)s__and__ms__instance(V__ROW4,s__AngleMeasure)s__and__ms__instance(V__ROW1,s__AngleMeasure)s__and__ms__instance(V__ROW2,s__AngleMeasure)s__and__ms__instance(V__DIRECTION,s__DirectionalAttribute))
    s__=>(s__instance(s__LatitudeFn__6Fn(V__DIRECTION,V__ROW1,V__ROW2,V__ROW3,V__ROW4,V__ROW5)
    ,s__Region)s__=>((V__DIRECTIONs__equal__ms__North)s__or__m(V__DIRECTIONs__equal__ms__South))))
   )

( ∀ [V__ROW3,V__ROW1,V__ROW2,V__DIRECTION]
   ((s__instance(V__ROW3,s__AngleMeasure)s__and__ms__instance(V__ROW1,s__AngleMeasure)s__and__ms__instance(V__ROW2,s__AngleMeasure)s__and__ms__instance(V__DIRECTION,s__DirectionalAttribute))
    s__=>(s__instance(s__LatitudeFn__4Fn(V__DIRECTION,V__ROW1,V__ROW2,V__ROW3)
    ,s__Region)s__=>((V__DIRECTIONs__equal__ms__North)s__or__m(V__DIRECTIONs__equal__ms__South))))
   )

( ∀ [V__ROW1,V__ROW2,V__DIRECTION]
   ((s__instance(V__ROW1,s__AngleMeasure)s__and__ms__instance(V__ROW2,s__AngleMeasure)s__and__ms__instance(V__DIRECTION,s__DirectionalAttribute))
    s__=>(s__instance(s__LatitudeFn__3Fn(V__DIRECTION,V__ROW1,V__ROW2)
    ,s__Region)s__=>((V__DIRECTIONs__equal__ms__North)s__or__m(V__DIRECTIONs__equal__ms__South))))
   )

Geography.kif 421-425
( ∀ [V__ROW5,V__ROW3,V__ROW4,V__ROW1,V__ROW2,V__DIRECTION]
   ((s__instance(V__ROW5,s__AngleMeasure)s__and__ms__instance(V__ROW3,s__AngleMeasure)s__and__ms__instance(V__ROW4,s__AngleMeasure)s__and__ms__instance(V__ROW1,s__AngleMeasure)s__and__ms__instance(V__ROW2,s__AngleMeasure)s__and__ms__instance(V__DIRECTION,s__DirectionalAttribute))
    s__=>(s__instance(s__LongitudeFn__6Fn(V__DIRECTION,V__ROW1,V__ROW2,V__ROW3,V__ROW4,V__ROW5)
    ,s__Region)s__=>((V__DIRECTIONs__equal__ms__East)s__or__m(V__DIRECTIONs__equal__ms__West))))
   )

( ∀ [V__ROW1,V__ROW2,V__DIRECTION]
   ((s__instance(V__ROW1,s__AngleMeasure)s__and__ms__instance(V__ROW2,s__AngleMeasure)s__and__ms__instance(V__DIRECTION,s__DirectionalAttribute))
    s__=>(s__instance(s__LongitudeFn__3Fn(V__DIRECTION,V__ROW1,V__ROW2)
    ,s__Region)s__=>((V__DIRECTIONs__equal__ms__East)s__or__m(V__DIRECTIONs__equal__ms__West))))
   )

( ∀ [V__ROW3,V__ROW1,V__ROW2,V__DIRECTION]
   ((s__instance(V__ROW3,s__AngleMeasure)s__and__ms__instance(V__ROW1,s__AngleMeasure)s__and__ms__instance(V__ROW2,s__AngleMeasure)s__and__ms__instance(V__DIRECTION,s__DirectionalAttribute))
    s__=>(s__instance(s__LongitudeFn__4Fn(V__DIRECTION,V__ROW1,V__ROW2,V__ROW3)
    ,s__Region)s__=>((V__DIRECTIONs__equal__ms__East)s__or__m(V__DIRECTIONs__equal__ms__West))))
   )

( ∀ [V__ROW5,V__ROW6,V__ROW3,V__ROW4,V__ROW1,V__ROW2,V__DIRECTION]
   ((s__instance(V__ROW5,s__AngleMeasure)s__and__ms__instance(V__ROW6,s__AngleMeasure)s__and__ms__instance(V__ROW3,s__AngleMeasure)s__and__ms__instance(V__ROW4,s__AngleMeasure)s__and__ms__instance(V__ROW1,s__AngleMeasure)s__and__ms__instance(V__ROW2,s__AngleMeasure)s__and__ms__instance(V__DIRECTION,s__DirectionalAttribute))
    s__=>(s__instance(s__LongitudeFn__7Fn(V__DIRECTION,V__ROW1,V__ROW2,V__ROW3,V__ROW4,V__ROW5,V__ROW6)
    ,s__Region)s__=>((V__DIRECTIONs__equal__ms__East)s__or__m(V__DIRECTIONs__equal__ms__West))))
   )

( ∀ [V__ROW3,V__ROW4,V__ROW1,V__ROW2,V__DIRECTION]
   ((s__instance(V__ROW3,s__AngleMeasure)s__and__ms__instance(V__ROW4,s__AngleMeasure)s__and__ms__instance(V__ROW1,s__AngleMeasure)s__and__ms__instance(V__ROW2,s__AngleMeasure)s__and__ms__instance(V__DIRECTION,s__DirectionalAttribute))
    s__=>(s__instance(s__LongitudeFn__5Fn(V__DIRECTION,V__ROW1,V__ROW2,V__ROW3,V__ROW4)
    ,s__Region)s__=>((V__DIRECTIONs__equal__ms__East)s__or__m(V__DIRECTIONs__equal__ms__West))))
   )

( ∀ [V__ROW1,V__DIRECTION]
   ((s__instance(V__ROW1,s__AngleMeasure)s__and__ms__instance(V__DIRECTION,s__DirectionalAttribute))
    s__=>(s__instance(s__LongitudeFn__2Fn(V__DIRECTION,V__ROW1)
    ,s__Region)s__=>((V__DIRECTIONs__equal__ms__East)s__or__m(V__DIRECTIONs__equal__ms__West))))
   )

Geography.kif 461-465
( ∀ [V__REGION]
   (s__instance(V__REGION,s__Region)s__=>(s__exists__m[V__PHYS]
       (s__instance(V__PHYS,s__Physical)s__and__ms__located(V__PHYS,V__REGION))))
)

Merge.kif 1289-1292
( ∀ [V__REGION]
   (s__instance(V__REGION,s__Region)s__=>s__superficialPart(s__InnerBoundaryFn(V__REGION)
  ,V__REGION))
)

Geography.kif 795-797
( ∀ [V__REGION]
   (s__instance(V__REGION,s__Region)s__=>s__superficialPart(s__OuterBoundaryFn(V__REGION)
  ,V__REGION))
)

Geography.kif 807-809

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


( ∀ [V__DRYSPELL,V__AREA]
   ((s__instance(V__DRYSPELL,s__Drought)s__and__ms__eventLocated(V__DRYSPELL,V__AREA))
  s__=>(s__not__m(s__exists__m[V__RAIN,V__PLACE]
     (s__instance(V__RAIN,s__Raining)s__and__ms__instance(V__PLACE,s__Region)s__and__ms__eventLocated(V__RAIN,V__PLACE)
    s__and__ms__overlapsSpatially(V__PLACE,V__AREA)
  s__and__ms__overlapsTemporally(V__RAIN,V__DRYSPELL)))))
)

Weather.kif 908-919
No TPTP formula. May not be expressible in strict first order. MilitaryProcesses.kif 566-576
( ∀ [V__PLACE1,V__MOVEMENT]
   (s__instance(V__PLACE1,s__Object)s__=>((s__instance(V__MOVEMENT,s__Translocation)s__and__ms__origin(V__MOVEMENT,V__PLACE1))
    s__=>(s__exists__m[V__PLACE2,V__STAGE]
       (s__instance(V__STAGE,s__Process)s__and__m(s__instance(V__PLACE2,s__Region)s__and__m(s__not__m(V__PLACE1s__equal__mV__PLACE2))
      s__and__ms__subProcess(V__STAGE,V__MOVEMENT)
    s__and__ms__located(V__STAGE,V__PLACE2))))))
)

Merge.kif 11505-11514
No TPTP formula. May not be expressible in strict first order. Mid-level-ontology.kif 28190-28219
No TPTP formula. May not be expressible in strict first order. Dining.kif 913-937
( ∀ [V__X]
   (s__instance(V__X,s__Object)s__=>(s__attribute(V__X,s__DownAndInRoom)s__=>(s__exists__m[V__LOC,V__INDOOR]
         (s__instance(V__INDOOR,s__Indoors)s__and__ms__instance(V__LOC,s__Region)s__and__ms__orientation(V__LOC,V__X,s__Adjacent)s__and__ms__orientation(V__LOC,V__X,s__Outside)s__and__ms__located(V__LOC,V__INDOOR)))))
)

Hotel.kif 1010-1018
( ∀ [V__X]
   (s__instance(V__X,s__Object)s__=>(s__attribute(V__X,s__DownAndOutRoom)s__=>(s__exists__m[V__LOC,V__OUTDOOR]
         (s__instance(V__OUTDOOR,s__Outdoors)s__and__ms__instance(V__LOC,s__Region)s__and__ms__orientation(V__LOC,V__X,s__Adjacent)s__and__ms__orientation(V__LOC,V__X,s__Outside)s__and__ms__located(V__LOC,V__OUTDOOR)))))
)

Hotel.kif 1025-1033
( ∀ [V__P1,V__P2,V__X,V__PM]
   ((s__instance(V__P1,s__UnitOfMeasure)s__and__ms__instance(V__P2,s__UnitOfMeasure)s__and__ms__instance(V__X,s__Object)s__and__ms__instance(V__PM,s__RealNumber))
    s__=>(s__attribute(V__X,s__PartialVacuum)s__=>(s__exists__m[V__O,V__G]
         (s__instance(V__O,s__SelfConnectedObject)s__and__ms__instance(V__G,s__Region)s__and__m(s__not__m(V__Gs__equal__mV__X))
        s__and__ms__connected(V__X,V__O)
      s__and__ms__connected(V__G,V__O)
    s__and__ms__measure(V__G,s__MeasureFn(V__PM,V__P1))
s__and__ms__measure(V__X,s__MeasureFn(V__PM,V__P2))
s__and__ms__instance(V__PM,s__UnitOfAtmosphericPressure)s__and__ms__greaterThan(V__P1,V__P2)))))
)

Cars.kif 383-396
( ∀ [V__P1,V__P2,V__X,V__PM]
   ((s__instance(V__P1,s__UnitOfMeasure)s__and__ms__instance(V__P2,s__UnitOfMeasure)s__and__ms__instance(V__X,s__Object)s__and__ms__instance(V__PM,s__RealNumber))
    s__=>(s__attribute(V__X,s__Pressurized)s__=>(s__exists__m[V__O,V__G]
         (s__instance(V__O,s__SelfConnectedObject)s__and__ms__instance(V__G,s__Region)s__and__m(s__not__m(V__Gs__equal__mV__X))
        s__and__ms__connected(V__X,V__O)
      s__and__ms__connected(V__G,V__O)
    s__and__ms__measure(V__G,s__MeasureFn(V__PM,V__P1))
s__and__ms__measure(V__X,s__MeasureFn(V__PM,V__P2))
s__and__ms__instance(V__PM,s__UnitOfAtmosphericPressure)s__and__ms__greaterThan(V__P2,V__P1)))))
)

Cars.kif 403-416
No TPTP formula. May not be expressible in strict first order. engineering.kif 1134-1146
No TPTP formula. May not be expressible in strict first order. Weather.kif 721-735
No TPTP formula. May not be expressible in strict first order. Weather.kif 1290-1304
No TPTP formula. May not be expressible in strict first order. Weather.kif 1346-1359
( ∀ [V__REGION,V__OBJ]
   ((s__instance(V__REGION,s__Object)s__and__ms__instance(V__OBJ,s__Object))
    s__=>(s__orientation(V__OBJ,V__REGION,s__Inside)s__=>s__instance(V__REGION,s__Region)))
   )

Mid-level-ontology.kif 8840-8842
( ∀ [V__REGION,V__OBJ]
   ((s__instance(V__REGION,s__Object)s__and__ms__instance(V__OBJ,s__Object))
    s__=>(s__orientation(V__OBJ,V__REGION,s__Outside)s__=>s__instance(V__REGION,s__Region)))
   )

Mid-level-ontology.kif 8836-8838
( ∀ [V__DIR,V__PLACE]
   ((s__instance(V__DIR,s__DirectionalAttribute)s__and__ms__instance(V__PLACE,s__Object))
    s__=>(s__surfaceWindDirection(V__PLACE,V__DIR)
    s__=>(s__exists__m[V__WIND,V__FROM]
       (s__instance(V__WIND,s__Wind)s__and__ms__instance(V__FROM,s__Region)s__and__ms__eventPartlyLocated(V__WIND,V__PLACE)
      s__and__ms__origin(V__WIND,V__FROM)
    s__and__ms__orientation(V__FROM,V__PLACE,V__DIR)))))
)

Weather.kif 166-174


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 2.99c (>= 2017/11/20) is open source software produced by Articulate Software and its partners