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

Formal Language: 



KB Term:  Term intersection
English Word: 

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...

VerbNet: remove-10.1|reap, remove-10.1|reap,


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


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

chinese_format.kif 1626-1629
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 1143-1148
s__partition__3(s__Region,s__GeographicArea,s__SpaceRegion)

Mid-level-ontology.kif 8701-8701 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 1141-1141 Region is a subclass of object

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


s__range(s__FlowRegionFn__m,s__Region)

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

Geography.kif 796-796 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 808-808 The range of outer boundary is an instance of region
s__range(s__WhereFn__m,s__Region)

Merge.kif 4041-4041 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 8765-8765 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 12983-12983 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 9234-9234 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 8869-8869 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 8857-8857 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 24738-24738 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 761-761 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 935-935 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 1295-1295 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 20058-20058 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 8789-8789 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,n__1,s__Region)

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

Weather.kif 1205-1205 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 1183-1193 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__REGION] :
   ((( ? [V__EMIT] :
         ((s__instance(V__EMIT,s__RadiatingLight) &
             s__patient(V__EMIT,V__REGION)
           &
           s__instance(V__REGION,s__Region))))
     =>
     s__attribute(V__REGION,s__Illuminated))
   &
   (s__attribute(V__REGION,s__Illuminated) =>
     ( ? [V__EMIT] :
       ((s__instance(V__EMIT,s__RadiatingLight) &
           s__patient(V__EMIT,V__REGION)
         &
         s__instance(V__REGION,s__Region)))))
)
)

Merge.kif 12622-12628 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__instance(V__I,s__Region))
     =>
     ( ? [V__H] :
       ((s__instance(V__H,s__Human) &
           s__inhabits(V__H,V__I))))
   )
)

Mid-level-ontology.kif 28284-28291
( ! [V__U] :
   ((s__attribute(V__U,s__Uninhabited) &
       s__instance(V__U,s__Region))
     =>
     ~(( ? [V__H] :
         ((s__instance(V__H,s__Human) &
             s__inhabits(V__H,V__U)))))
   )
)

Mid-level-ontology.kif 28268-28276
( ! [V__ROW5,V__ROW6,V__ROW3,V__ROW4,V__ROW2,V__DIRECTION,V__NUM] :
   ((s__instance(V__ROW5,s__AngleMeasure) &
       s__instance(V__ROW6,s__AngleMeasure) &
       s__instance(V__ROW3,s__AngleMeasure) &
       s__instance(V__ROW4,s__AngleMeasure) &
       s__instance(V__ROW2,s__AngleMeasure) &
       s__instance(V__DIRECTION,s__DirectionalAttribute) &
       s__instance(V__NUM,s__RealNumber))
     =>
     (s__instance(s__LatitudeFn__6Fn(V__DIRECTION,V__ROW2,V__ROW3,V__ROW4,V__ROW5,V__ROW6)
    ,s__Region) &
     (s__ListOrderFn(s__ListFn__5Fn(V__ROW2,V__ROW3,V__ROW4,V__ROW5,V__ROW6)
    ,n__1)
   = s__MeasureFn(V__NUM,s__AngularDegree)))
=>
s__lessThanOrEqualTo(V__NUM,n__90)
)
)

( ! [V__ROW2,V__DIRECTION,V__NUM] :
   ((s__instance(V__ROW2,s__AngleMeasure) &
       s__instance(V__DIRECTION,s__DirectionalAttribute) &
       s__instance(V__NUM,s__RealNumber))
     =>
     (s__instance(s__LatitudeFn__2Fn(V__DIRECTION,V__ROW2)
    ,s__Region) &
     (s__ListOrderFn(s__ListFn__1Fn(V__ROW2)
    ,n__1)
   = s__MeasureFn(V__NUM,s__AngularDegree)))
=>
s__lessThanOrEqualTo(V__NUM,n__90)
)
)

( ! [V__ROW5,V__ROW3,V__ROW4,V__ROW2,V__DIRECTION,V__NUM] :
   ((s__instance(V__ROW5,s__AngleMeasure) &
       s__instance(V__ROW3,s__AngleMeasure) &
       s__instance(V__ROW4,s__AngleMeasure) &
       s__instance(V__ROW2,s__AngleMeasure) &
       s__instance(V__DIRECTION,s__DirectionalAttribute) &
       s__instance(V__NUM,s__RealNumber))
     =>
     (s__instance(s__LatitudeFn__5Fn(V__DIRECTION,V__ROW2,V__ROW3,V__ROW4,V__ROW5)
    ,s__Region) &
     (s__ListOrderFn(s__ListFn__4Fn(V__ROW2,V__ROW3,V__ROW4,V__ROW5)
    ,n__1)
   = s__MeasureFn(V__NUM,s__AngularDegree)))
=>
s__lessThanOrEqualTo(V__NUM,n__90)
)
)

( ! [V__ROW3,V__ROW2,V__DIRECTION,V__NUM] :
   ((s__instance(V__ROW3,s__AngleMeasure) &
       s__instance(V__ROW2,s__AngleMeasure) &
       s__instance(V__DIRECTION,s__DirectionalAttribute) &
       s__instance(V__NUM,s__RealNumber))
     =>
     (s__instance(s__LatitudeFn__3Fn(V__DIRECTION,V__ROW2,V__ROW3)
    ,s__Region) &
     (s__ListOrderFn(s__ListFn__2Fn(V__ROW2,V__ROW3)
    ,n__1)
   = s__MeasureFn(V__NUM,s__AngularDegree)))
=>
s__lessThanOrEqualTo(V__NUM,n__90)
)
)

( ! [V__ROW7,V__ROW5,V__ROW6,V__ROW3,V__ROW4,V__ROW2,V__DIRECTION,V__NUM] :
   ((s__instance(V__ROW7,s__AngleMeasure) &
       s__instance(V__ROW5,s__AngleMeasure) &
       s__instance(V__ROW6,s__AngleMeasure) &
       s__instance(V__ROW3,s__AngleMeasure) &
       s__instance(V__ROW4,s__AngleMeasure) &
       s__instance(V__ROW2,s__AngleMeasure) &
       s__instance(V__DIRECTION,s__DirectionalAttribute) &
       s__instance(V__NUM,s__RealNumber))
     =>
     (s__instance(s__LatitudeFn__7Fn(V__DIRECTION,V__ROW2,V__ROW3,V__ROW4,V__ROW5,V__ROW6,V__ROW7)
    ,s__Region) &
     (s__ListOrderFn(s__ListFn__6Fn(V__ROW2,V__ROW3,V__ROW4,V__ROW5,V__ROW6,V__ROW7)
    ,n__1)
   = s__MeasureFn(V__NUM,s__AngularDegree)))
=>
s__lessThanOrEqualTo(V__NUM,n__90)
)
)

( ! [V__ROW3,V__ROW4,V__ROW2,V__DIRECTION,V__NUM] :
   ((s__instance(V__ROW3,s__AngleMeasure) &
       s__instance(V__ROW4,s__AngleMeasure) &
       s__instance(V__ROW2,s__AngleMeasure) &
       s__instance(V__DIRECTION,s__DirectionalAttribute) &
       s__instance(V__NUM,s__RealNumber))
     =>
     (s__instance(s__LatitudeFn__4Fn(V__DIRECTION,V__ROW2,V__ROW3,V__ROW4)
    ,s__Region) &
     (s__ListOrderFn(s__ListFn__3Fn(V__ROW2,V__ROW3,V__ROW4)
    ,n__1)
   = s__MeasureFn(V__NUM,s__AngularDegree)))
=>
s__lessThanOrEqualTo(V__NUM,n__90)
)
)

( ! [V__ROW7,V__ROW8,V__ROW5,V__ROW6,V__ROW3,V__ROW4,V__ROW2,V__DIRECTION,V__NUM] :
   ((s__instance(V__ROW7,s__AngleMeasure) &
       s__instance(V__ROW8,s__AngleMeasure) &
       s__instance(V__ROW5,s__AngleMeasure) &
       s__instance(V__ROW6,s__AngleMeasure) &
       s__instance(V__ROW3,s__AngleMeasure) &
       s__instance(V__ROW4,s__AngleMeasure) &
       s__instance(V__ROW2,s__AngleMeasure) &
       s__instance(V__DIRECTION,s__DirectionalAttribute) &
       s__instance(V__NUM,s__RealNumber))
     =>
     (s__instance(s__LatitudeFn__8Fn(V__DIRECTION,V__ROW2,V__ROW3,V__ROW4,V__ROW5,V__ROW6,V__ROW7,V__ROW8)
    ,s__Region) &
     (s__ListOrderFn(s__ListFn__7Fn(V__ROW2,V__ROW3,V__ROW4,V__ROW5,V__ROW6,V__ROW7,V__ROW8)
    ,n__1)
   = s__MeasureFn(V__NUM,s__AngularDegree)))
=>
s__lessThanOrEqualTo(V__NUM,n__90)
)
)

Geography.kif 427-431
( ! [V__ROW5,V__ROW3,V__ROW4,V__ROW2,V__DIRECTION,V__NUM] :
   ((s__instance(V__ROW5,s__AngleMeasure) &
       s__instance(V__ROW3,s__AngleMeasure) &
       s__instance(V__ROW4,s__AngleMeasure) &
       s__instance(V__ROW2,s__AngleMeasure) &
       s__instance(V__DIRECTION,s__DirectionalAttribute) &
       s__instance(V__NUM,s__RealNumber))
     =>
     (s__instance(s__LongitudeFn__5Fn(V__DIRECTION,V__ROW2,V__ROW3,V__ROW4,V__ROW5)
    ,s__Region) &
     (s__ListOrderFn(s__ListFn__4Fn(V__ROW2,V__ROW3,V__ROW4,V__ROW5)
    ,n__1)
   = s__MeasureFn(V__NUM,s__AngularDegree)))
=>
s__lessThanOrEqualTo(V__NUM,n__180)
)
)

( ! [V__ROW3,V__ROW4,V__ROW2,V__DIRECTION,V__NUM] :
   ((s__instance(V__ROW3,s__AngleMeasure) &
       s__instance(V__ROW4,s__AngleMeasure) &
       s__instance(V__ROW2,s__AngleMeasure) &
       s__instance(V__DIRECTION,s__DirectionalAttribute) &
       s__instance(V__NUM,s__RealNumber))
     =>
     (s__instance(s__LongitudeFn__4Fn(V__DIRECTION,V__ROW2,V__ROW3,V__ROW4)
    ,s__Region) &
     (s__ListOrderFn(s__ListFn__3Fn(V__ROW2,V__ROW3,V__ROW4)
    ,n__1)
   = s__MeasureFn(V__NUM,s__AngularDegree)))
=>
s__lessThanOrEqualTo(V__NUM,n__180)
)
)

( ! [V__ROW7,V__ROW8,V__ROW5,V__ROW6,V__ROW3,V__ROW4,V__ROW2,V__DIRECTION,V__NUM] :
   ((s__instance(V__ROW7,s__AngleMeasure) &
       s__instance(V__ROW8,s__AngleMeasure) &
       s__instance(V__ROW5,s__AngleMeasure) &
       s__instance(V__ROW6,s__AngleMeasure) &
       s__instance(V__ROW3,s__AngleMeasure) &
       s__instance(V__ROW4,s__AngleMeasure) &
       s__instance(V__ROW2,s__AngleMeasure) &
       s__instance(V__DIRECTION,s__DirectionalAttribute) &
       s__instance(V__NUM,s__RealNumber))
     =>
     (s__instance(s__LongitudeFn__8Fn(V__DIRECTION,V__ROW2,V__ROW3,V__ROW4,V__ROW5,V__ROW6,V__ROW7,V__ROW8)
    ,s__Region) &
     (s__ListOrderFn(s__ListFn__7Fn(V__ROW2,V__ROW3,V__ROW4,V__ROW5,V__ROW6,V__ROW7,V__ROW8)
    ,n__1)
   = s__MeasureFn(V__NUM,s__AngularDegree)))
=>
s__lessThanOrEqualTo(V__NUM,n__180)
)
)

( ! [V__ROW7,V__ROW5,V__ROW6,V__ROW3,V__ROW4,V__ROW2,V__DIRECTION,V__NUM] :
   ((s__instance(V__ROW7,s__AngleMeasure) &
       s__instance(V__ROW5,s__AngleMeasure) &
       s__instance(V__ROW6,s__AngleMeasure) &
       s__instance(V__ROW3,s__AngleMeasure) &
       s__instance(V__ROW4,s__AngleMeasure) &
       s__instance(V__ROW2,s__AngleMeasure) &
       s__instance(V__DIRECTION,s__DirectionalAttribute) &
       s__instance(V__NUM,s__RealNumber))
     =>
     (s__instance(s__LongitudeFn__7Fn(V__DIRECTION,V__ROW2,V__ROW3,V__ROW4,V__ROW5,V__ROW6,V__ROW7)
    ,s__Region) &
     (s__ListOrderFn(s__ListFn__6Fn(V__ROW2,V__ROW3,V__ROW4,V__ROW5,V__ROW6,V__ROW7)
    ,n__1)
   = s__MeasureFn(V__NUM,s__AngularDegree)))
=>
s__lessThanOrEqualTo(V__NUM,n__180)
)
)

( ! [V__ROW2,V__DIRECTION,V__NUM] :
   ((s__instance(V__ROW2,s__AngleMeasure) &
       s__instance(V__DIRECTION,s__DirectionalAttribute) &
       s__instance(V__NUM,s__RealNumber))
     =>
     (s__instance(s__LongitudeFn__2Fn(V__DIRECTION,V__ROW2)
    ,s__Region) &
     (s__ListOrderFn(s__ListFn__1Fn(V__ROW2)
    ,n__1)
   = s__MeasureFn(V__NUM,s__AngularDegree)))
=>
s__lessThanOrEqualTo(V__NUM,n__180)
)
)

( ! [V__ROW3,V__ROW2,V__DIRECTION,V__NUM] :
   ((s__instance(V__ROW3,s__AngleMeasure) &
       s__instance(V__ROW2,s__AngleMeasure) &
       s__instance(V__DIRECTION,s__DirectionalAttribute) &
       s__instance(V__NUM,s__RealNumber))
     =>
     (s__instance(s__LongitudeFn__3Fn(V__DIRECTION,V__ROW2,V__ROW3)
    ,s__Region) &
     (s__ListOrderFn(s__ListFn__2Fn(V__ROW2,V__ROW3)
    ,n__1)
   = s__MeasureFn(V__NUM,s__AngularDegree)))
=>
s__lessThanOrEqualTo(V__NUM,n__180)
)
)

( ! [V__ROW5,V__ROW6,V__ROW3,V__ROW4,V__ROW2,V__DIRECTION,V__NUM] :
   ((s__instance(V__ROW5,s__AngleMeasure) &
       s__instance(V__ROW6,s__AngleMeasure) &
       s__instance(V__ROW3,s__AngleMeasure) &
       s__instance(V__ROW4,s__AngleMeasure) &
       s__instance(V__ROW2,s__AngleMeasure) &
       s__instance(V__DIRECTION,s__DirectionalAttribute) &
       s__instance(V__NUM,s__RealNumber))
     =>
     (s__instance(s__LongitudeFn__6Fn(V__DIRECTION,V__ROW2,V__ROW3,V__ROW4,V__ROW5,V__ROW6)
    ,s__Region) &
     (s__ListOrderFn(s__ListFn__5Fn(V__ROW2,V__ROW3,V__ROW4,V__ROW5,V__ROW6)
    ,n__1)
   = s__MeasureFn(V__NUM,s__AngularDegree)))
=>
s__lessThanOrEqualTo(V__NUM,n__180)
)
)

Geography.kif 467-474
( ! [V__OP,V__REGION] :
   ((s__instance(V__OP,s__MilitaryOperation) &
       s__eventLocated(V__OP,V__REGION)
     &
     s__instance(V__REGION,s__Region))
   =>
   s__areaOfOperation(V__REGION,V__OP)
)
)

MilitaryProcesses.kif 1325-1330
( ! [V__X] :
   ((s__instance(V__X,s__Region) &
       s__attribute(V__X,s__Vacuum))
     =>
     ~(( ? [V__O] :
         ((s__instance(V__O,s__Object) &
             s__located(V__O,V__X)))))
   )
)

Cars.kif 368-376
( ! [V__TWO,V__ONE] :
   (s__instance(V__ONE,s__Object) =>
     (s__overlapsSpatially(V__ONE,V__TWO)
     &
     s__instance(V__TWO,s__Region) &
     ~((V__ONE = V__TWO)))
   =>
   s__partlyLocated(V__ONE,V__TWO)
)
)

Geography.kif 3355-3360
( ! [V__A,V__Time,V__B,V__Distance,V__Observe,V__Area,V__D2] :
   ((s__instance(V__A,s__Agent) &
       s__instance(V__Distance,s__LengthMeasure) &
       s__instance(V__Area,s__Region) &
       s__instance(V__D2,s__LengthMeasure))
     =>
     (s__visibilityInMeteorology(V__Area,V__Time,V__Distance)
     &
     s__instance(V__Time,s__NightTime) &
     s__instance(V__Observe,s__Looking) &
     s__instance(V__B,s__Region) &
     s__attribute(V__B,s__Illuminated) &
     s__measure(V__B,s__MeasureFn(n__1000,s__Candela))
   &
   s__agent(V__Observe,V__A)
&
s__patient(V__Observe,V__B)
&
s__orientation(V__A,V__B,s__Horizontal) &
s__eventLocated(V__Observe,V__Area)
&
s__during(s__WhenFn(V__Observe)
,V__Time)
&
s__instance(V__B,s__Object))
=>
(s__distance(V__A,V__B,V__D2)
&
s__greaterThan(V__Distance,V__D2))
)
)

Weather.kif 1252-1269
( ! [V__ROW5,V__ROW6,V__ROW3,V__ROW4,V__ROW2,V__DIRECTION] :
   ((s__instance(V__ROW5,s__AngleMeasure) &
       s__instance(V__ROW6,s__AngleMeasure) &
       s__instance(V__ROW3,s__AngleMeasure) &
       s__instance(V__ROW4,s__AngleMeasure) &
       s__instance(V__ROW2,s__AngleMeasure) &
       s__instance(V__DIRECTION,s__DirectionalAttribute))
     =>
     s__instance(s__LatitudeFn__6Fn(V__DIRECTION,V__ROW2,V__ROW3,V__ROW4,V__ROW5,V__ROW6)
  ,s__Region) =>
   ((V__DIRECTION = s__North) |
       (V__DIRECTION = s__South))
       )
     )

( ! [V__ROW5,V__ROW3,V__ROW4,V__ROW2,V__DIRECTION] :
   ((s__instance(V__ROW5,s__AngleMeasure) &
       s__instance(V__ROW3,s__AngleMeasure) &
       s__instance(V__ROW4,s__AngleMeasure) &
       s__instance(V__ROW2,s__AngleMeasure) &
       s__instance(V__DIRECTION,s__DirectionalAttribute))
     =>
     s__instance(s__LatitudeFn__5Fn(V__DIRECTION,V__ROW2,V__ROW3,V__ROW4,V__ROW5)
  ,s__Region) =>
   ((V__DIRECTION = s__North) |
       (V__DIRECTION = s__South))
       )
     )

( ! [V__ROW3,V__ROW4,V__ROW2,V__DIRECTION] :
   ((s__instance(V__ROW3,s__AngleMeasure) &
       s__instance(V__ROW4,s__AngleMeasure) &
       s__instance(V__ROW2,s__AngleMeasure) &
       s__instance(V__DIRECTION,s__DirectionalAttribute))
     =>
     s__instance(s__LatitudeFn__4Fn(V__DIRECTION,V__ROW2,V__ROW3,V__ROW4)
  ,s__Region) =>
   ((V__DIRECTION = s__North) |
       (V__DIRECTION = s__South))
       )
     )

( ! [V__ROW2,V__DIRECTION] :
   ((s__instance(V__ROW2,s__AngleMeasure) &
       s__instance(V__DIRECTION,s__DirectionalAttribute))
     =>
     s__instance(s__LatitudeFn__2Fn(V__DIRECTION,V__ROW2)
  ,s__Region) =>
   ((V__DIRECTION = s__North) |
       (V__DIRECTION = s__South))
       )
     )

( ! [V__ROW7,V__ROW5,V__ROW6,V__ROW3,V__ROW4,V__ROW2,V__DIRECTION] :
   ((s__instance(V__ROW7,s__AngleMeasure) &
       s__instance(V__ROW5,s__AngleMeasure) &
       s__instance(V__ROW6,s__AngleMeasure) &
       s__instance(V__ROW3,s__AngleMeasure) &
       s__instance(V__ROW4,s__AngleMeasure) &
       s__instance(V__ROW2,s__AngleMeasure) &
       s__instance(V__DIRECTION,s__DirectionalAttribute))
     =>
     s__instance(s__LatitudeFn__7Fn(V__DIRECTION,V__ROW2,V__ROW3,V__ROW4,V__ROW5,V__ROW6,V__ROW7)
  ,s__Region) =>
   ((V__DIRECTION = s__North) |
       (V__DIRECTION = s__South))
       )
     )

( ! [V__ROW3,V__ROW2,V__DIRECTION] :
   ((s__instance(V__ROW3,s__AngleMeasure) &
       s__instance(V__ROW2,s__AngleMeasure) &
       s__instance(V__DIRECTION,s__DirectionalAttribute))
     =>
     s__instance(s__LatitudeFn__3Fn(V__DIRECTION,V__ROW2,V__ROW3)
  ,s__Region) =>
   ((V__DIRECTION = s__North) |
       (V__DIRECTION = s__South))
       )
     )

Geography.kif 421-425
( ! [V__ROW5,V__ROW6,V__ROW3,V__ROW4,V__ROW2,V__DIRECTION] :
   ((s__instance(V__ROW5,s__AngleMeasure) &
       s__instance(V__ROW6,s__AngleMeasure) &
       s__instance(V__ROW3,s__AngleMeasure) &
       s__instance(V__ROW4,s__AngleMeasure) &
       s__instance(V__ROW2,s__AngleMeasure) &
       s__instance(V__DIRECTION,s__DirectionalAttribute))
     =>
     s__instance(s__LongitudeFn__6Fn(V__DIRECTION,V__ROW2,V__ROW3,V__ROW4,V__ROW5,V__ROW6)
  ,s__Region) =>
   ((V__DIRECTION = s__East) |
       (V__DIRECTION = s__West))
       )
     )

( ! [V__ROW5,V__ROW3,V__ROW4,V__ROW2,V__DIRECTION] :
   ((s__instance(V__ROW5,s__AngleMeasure) &
       s__instance(V__ROW3,s__AngleMeasure) &
       s__instance(V__ROW4,s__AngleMeasure) &
       s__instance(V__ROW2,s__AngleMeasure) &
       s__instance(V__DIRECTION,s__DirectionalAttribute))
     =>
     s__instance(s__LongitudeFn__5Fn(V__DIRECTION,V__ROW2,V__ROW3,V__ROW4,V__ROW5)
  ,s__Region) =>
   ((V__DIRECTION = s__East) |
       (V__DIRECTION = s__West))
       )
     )

( ! [V__ROW3,V__ROW4,V__ROW2,V__DIRECTION] :
   ((s__instance(V__ROW3,s__AngleMeasure) &
       s__instance(V__ROW4,s__AngleMeasure) &
       s__instance(V__ROW2,s__AngleMeasure) &
       s__instance(V__DIRECTION,s__DirectionalAttribute))
     =>
     s__instance(s__LongitudeFn__4Fn(V__DIRECTION,V__ROW2,V__ROW3,V__ROW4)
  ,s__Region) =>
   ((V__DIRECTION = s__East) |
       (V__DIRECTION = s__West))
       )
     )

( ! [V__ROW3,V__ROW2,V__DIRECTION] :
   ((s__instance(V__ROW3,s__AngleMeasure) &
       s__instance(V__ROW2,s__AngleMeasure) &
       s__instance(V__DIRECTION,s__DirectionalAttribute))
     =>
     s__instance(s__LongitudeFn__3Fn(V__DIRECTION,V__ROW2,V__ROW3)
  ,s__Region) =>
   ((V__DIRECTION = s__East) |
       (V__DIRECTION = s__West))
       )
     )

( ! [V__ROW2,V__DIRECTION] :
   ((s__instance(V__ROW2,s__AngleMeasure) &
       s__instance(V__DIRECTION,s__DirectionalAttribute))
     =>
     s__instance(s__LongitudeFn__2Fn(V__DIRECTION,V__ROW2)
  ,s__Region) =>
   ((V__DIRECTION = s__East) |
       (V__DIRECTION = s__West))
       )
     )

( ! [V__ROW7,V__ROW5,V__ROW6,V__ROW3,V__ROW4,V__ROW2,V__DIRECTION] :
   ((s__instance(V__ROW7,s__AngleMeasure) &
       s__instance(V__ROW5,s__AngleMeasure) &
       s__instance(V__ROW6,s__AngleMeasure) &
       s__instance(V__ROW3,s__AngleMeasure) &
       s__instance(V__ROW4,s__AngleMeasure) &
       s__instance(V__ROW2,s__AngleMeasure) &
       s__instance(V__DIRECTION,s__DirectionalAttribute))
     =>
     s__instance(s__LongitudeFn__7Fn(V__DIRECTION,V__ROW2,V__ROW3,V__ROW4,V__ROW5,V__ROW6,V__ROW7)
  ,s__Region) =>
   ((V__DIRECTION = s__East) |
       (V__DIRECTION = s__West))
       )
     )

Geography.kif 461-465
( ! [V__REGION] :
   (s__instance(V__REGION,s__Region) =>
     ( ? [V__PHYS] :
       ((s__instance(V__PHYS,s__Physical) &
           s__located(V__PHYS,V__REGION))))
   )
)

Merge.kif 1150-1153
( ! [V__REGION] :
   (s__instance(V__REGION,s__Region) =>
     s__superficialPart(s__InnerBoundaryFn(V__REGION)
  ,V__REGION)
)
)

Geography.kif 802-804
( ! [V__REGION] :
   (s__instance(V__REGION,s__Region) =>
     s__superficialPart(s__OuterBoundaryFn(V__REGION)
  ,V__REGION)
)
)

Geography.kif 814-816

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


( ! [V__DRYSPELL,V__AREA] :
   ((s__instance(V__DRYSPELL,s__Drought) &
       s__eventLocated(V__DRYSPELL,V__AREA))
   =>
   ~(( ? [V__RAIN, V__PLACE] :
       ((s__instance(V__RAIN,s__Raining) &
           s__instance(V__PLACE,s__Region) &
           s__eventLocated(V__RAIN,V__PLACE)
         &
         s__overlapsSpatially(V__PLACE,V__AREA)
       &
       s__overlapsTemporally(V__RAIN,V__DRYSPELL)))))
)
)

Weather.kif 985-996
No TPTP formula. May not be expressible in strict first order. MilitaryProcesses.kif 577-587
( ! [V__PLACE1,V__MOVEMENT] :
   (s__instance(V__PLACE1,s__Object) =>
     (s__instance(V__MOVEMENT,s__Translocation) &
       s__origin(V__MOVEMENT,V__PLACE1))
   =>
   ( ? [V__PLACE2, V__STAGE] :
     ((s__instance(V__STAGE,s__Process) &
         (s__instance(V__PLACE2,s__Region) &
           ~((V__PLACE1 = V__PLACE2))
           &
           s__subProcess(V__STAGE,V__MOVEMENT)
         &
         s__located(V__STAGE,V__PLACE2)))))
)
)

Merge.kif 10748-10757
No TPTP formula. May not be expressible in strict first order. Mid-level-ontology.kif 28196-28225
No TPTP formula. May not be expressible in strict first order. Dining.kif 909-933
( ! [V__X] :
   (s__instance(V__X,s__Object) =>
     s__attribute(V__X,s__DownAndInRoom) =>
     ( ? [V__LOC, V__INDOOR] :
       ((s__instance(V__INDOOR,s__Indoors) &
           s__instance(V__LOC,s__Region) &
           s__orientation(V__LOC,V__X,s__Adjacent) &
           s__orientation(V__LOC,V__X,s__Outside) &
           s__located(V__LOC,V__INDOOR))))
   )
)

Hotel.kif 1014-1022
( ! [V__X] :
   (s__instance(V__X,s__Object) =>
     s__attribute(V__X,s__DownAndOutRoom) =>
     ( ? [V__LOC, V__OUTDOOR] :
       ((s__instance(V__OUTDOOR,s__Outdoors) &
           s__instance(V__LOC,s__Region) &
           s__orientation(V__LOC,V__X,s__Adjacent) &
           s__orientation(V__LOC,V__X,s__Outside) &
           s__located(V__LOC,V__OUTDOOR))))
   )
)

Hotel.kif 1029-1037
( ! [V__P1,V__P2,V__X,V__PM] :
   ((s__instance(V__P1,s__UnitOfMeasure) &
       s__instance(V__P2,s__UnitOfMeasure) &
       s__instance(V__X,s__Object) &
       s__instance(V__PM,s__RealNumber))
     =>
     s__attribute(V__X,s__PartialVacuum) =>
     ( ? [V__O, V__G] :
       ((s__instance(V__O,s__SelfConnectedObject) &
           s__instance(V__G,s__Region) &
           ~((V__G = V__X))
           &
           s__connected(V__X,V__O)
         &
         s__connected(V__G,V__O)
       &
       s__measure(V__G,s__MeasureFn(V__PM,V__P1))
   &
   s__measure(V__X,s__MeasureFn(V__PM,V__P2))
&
s__instance(V__PM,s__UnitOfAtmosphericPressure) &
s__greaterThan(V__P1,V__P2))))
)
)

Cars.kif 383-396
( ! [V__P1,V__P2,V__X,V__PM] :
   ((s__instance(V__P1,s__UnitOfMeasure) &
       s__instance(V__P2,s__UnitOfMeasure) &
       s__instance(V__X,s__Object) &
       s__instance(V__PM,s__RealNumber))
     =>
     s__attribute(V__X,s__Pressurized) =>
     ( ? [V__O, V__G] :
       ((s__instance(V__O,s__SelfConnectedObject) &
           s__instance(V__G,s__Region) &
           ~((V__G = V__X))
           &
           s__connected(V__X,V__O)
         &
         s__connected(V__G,V__O)
       &
       s__measure(V__G,s__MeasureFn(V__PM,V__P1))
   &
   s__measure(V__X,s__MeasureFn(V__PM,V__P2))
&
s__instance(V__PM,s__UnitOfAtmosphericPressure) &
s__greaterThan(V__P2,V__P1))))
)
)

Cars.kif 403-416
No TPTP formula. May not be expressible in strict first order. engineering.kif 1138-1150
No TPTP formula. May not be expressible in strict first order. Weather.kif 720-734
No TPTP formula. May not be expressible in strict first order. Weather.kif 1386-1400
No TPTP formula. May not be expressible in strict first order. Weather.kif 1442-1455
( ! [V__REGION,V__OBJ] :
   ((s__instance(V__REGION,s__Object) &
       s__instance(V__OBJ,s__Object))
     =>
     s__orientation(V__OBJ,V__REGION,s__Inside) =>
     s__instance(V__REGION,s__Region) )
   )

Mid-level-ontology.kif 8843-8845
( ! [V__REGION,V__OBJ] :
   ((s__instance(V__REGION,s__Object) &
       s__instance(V__OBJ,s__Object))
     =>
     s__orientation(V__OBJ,V__REGION,s__Outside) =>
     s__instance(V__REGION,s__Region) )
   )

Mid-level-ontology.kif 8839-8841
( ! [V__DIR,V__PLACE] :
   ((s__instance(V__DIR,s__DirectionalAttribute) &
       s__instance(V__PLACE,s__Object))
     =>
     s__surfaceWindDirection(V__PLACE,V__DIR)
   =>
   ( ? [V__WIND, V__FROM] :
     ((s__instance(V__WIND,s__Wind) &
         s__instance(V__FROM,s__Region) &
         s__eventPartlyLocated(V__WIND,V__PLACE)
       &
       s__origin(V__WIND,V__FROM)
     &
     s__orientation(V__FROM,V__PLACE,V__DIR))))
)
)

Weather.kif 165-173


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



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