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

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 1175-1181
s__partition__3(s__Region,s__GeographicArea,s__SpaceRegion)

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

s__instance(s__Object,s__Class)

s__instance(s__Region,s__Class)

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

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


s__range(s__FlowRegionFn__m,s__Region)

Geography.kif 4712-4712 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 4121-4121 The range of where is an instance of region
s__subclass(s__Atmosphere,s__Region)

s__instance(s__Region,s__Class)

s__instance(s__Atmosphere,s__Class)

Weather.kif 10-10 Atmosphere is a subclass of region
s__subclass(s__DiningArea,s__Region)

s__instance(s__Region,s__Class)

s__instance(s__DiningArea,s__Class)

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

s__instance(s__Region,s__Class)

s__instance(s__FlowRegion,s__Class)

Mid-level-ontology.kif 8622-8622 Flow region is a subclass of region
s__subclass(s__GeographicArea,s__Region)

s__instance(s__Region,s__Class)

s__instance(s__GeographicArea,s__Class)

Merge.kif 13405-13405 Geographic area is a subclass of region
s__instance(s__Hole,s__Class)

s__instance(s__Region,s__Class)

s__subclass(s__Hole,s__Region)

Merge.kif 9466-9466 Hole is a subclass of region
s__instance(s__HydrophilicSide,s__Class)

s__subclass(s__HydrophilicSide,s__Region)

s__instance(s__Region,s__Class)

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

s__subclass(s__HydrophobicSide,s__Region)

s__instance(s__Region,s__Class)

VirusProteinAndCellPart.kif 485-485 Hydrophobic side is a subclass of region
s__subclass(s__Indoors,s__Region)

s__instance(s__Indoors,s__Class)

s__instance(s__Region,s__Class)

Mid-level-ontology.kif 8720-8720 Indoors is a subclass of region
s__instance(s__KitchenArea,s__Class)

s__subclass(s__KitchenArea,s__Region)

s__instance(s__Region,s__Class)

Mid-level-ontology.kif 14840-14840 Kitchen area is a subclass of region
s__subclass(s__Latitude,s__Region)

s__instance(s__Region,s__Class)

s__instance(s__Latitude,s__Class)

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

s__subclass(s__Longitude,s__Region)

s__instance(s__Region,s__Class)

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

s__instance(s__Region,s__Class)

s__instance(s__Outdoors,s__Class)

Mid-level-ontology.kif 8708-8708 Outdoors is a subclass of region
s__subclass(s__ParkingRegion,s__Region)

s__instance(s__ParkingRegion,s__Class)

s__instance(s__Region,s__Class)

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

s__instance(s__Region,s__Class)

s__instance(s__Patio,s__Class)

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

s__instance(s__PerimeterArea,s__Class)

s__instance(s__Region,s__Class)

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

s__instance(s__PlayArea,s__Class)

s__instance(s__Region,s__Class)

Dining.kif 935-935 Playground is a subclass of region
s__instance(s__RealEstate,s__Class)

s__instance(s__Region,s__Class)

s__subclass(s__RealEstate,s__Region)

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

s__instance(s__Region,s__Class)

s__instance(s__Road,s__Class)

Mid-level-ontology.kif 21527-21527 Road is a subclass of region
s__subclass(s__SittingArea,s__Region)

s__instance(s__Region,s__Class)

s__instance(s__SittingArea,s__Class)

Mid-level-ontology.kif 14827-14827 Sitting area is a subclass of region
s__instance(s__SpaceRegion,s__Class)

s__subclass(s__SpaceRegion,s__Region)

s__instance(s__Region,s__Class)

Mid-level-ontology.kif 8646-8646 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 227-227 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 6462-6462 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 23786-23786 The number 1 argument of canonicalPlaceName is an instance of region
s__domain(s__capableAtLocation__m,n__4,s__Region)

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

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

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

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

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

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

Geography.kif 4803-4803 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 3403-3403 The number 2 argument of provides destination is an instance of region
s__domain(s__routeBetween__m,n__2,s__Region)

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

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

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

Transportation.kif 2761-2761 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 2695-2695 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 2673-2683 An entity is an instance of region and the entity the attribute standard ambient temperature and pressure holds during a time position if and only if 298.15 kelvin degree(s) is an air temperature of the entity and 29.530 inch mercury(s) is a barometric pressure of the entity holds during the time position
( ! [V__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 13044-13050 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 29352-29359
( ! [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 29336-29344
( ! [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__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__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__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)))))
)
)

Geography.kif 427-431
( ! [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__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)))))
)
)

( ! [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__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__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)))))
)
)

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 3377-3382
( ! [V__A,V__Time,V__B,V__U,V__Distance,V__Observe,V__Area] :
   (((s__instance(V__A,s__Agent) &
         s__instance(V__Distance,s__RealNumber) &
         s__instance(V__Area,s__Region))
       =>
       (((s__visibilityInMeteorology(V__Area,V__Time,s__MeasureFn(V__Distance,V__U))
         &
         s__instance(V__U,s__UnitOfMeasure) &
         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))
=>
(( ? [V__D2] :
((s__instance(V__D2,s__RealNumber) &
   (s__distance(V__A,V__B,s__MeasureFn(V__D2,V__U))
&
s__greaterThan(V__Distance,V__D2)))))))))
)
)

Weather.kif 2743-2764
( ! [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))))))
       )
     )

( ! [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__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))))))
       )
     )

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__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__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__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))))))
       )
     )

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 1183-1186
( ! [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 2464-2475
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 11075-11084
No TPTP formula. May not be expressible in strict first order. Mid-level-ontology.kif 29263-29292
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 1035-1043
( ! [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 1050-1058
( ! [V__P1,V__P2,V__X,V__PM] :
   (((s__instance(V__P1,s__RealNumber) &
         s__instance(V__P2,s__RealNumber) &
         s__instance(V__X,s__Object) &
         s__instance(V__PM,s__UnitOfMeasure))
       =>
       ((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__P1,V__PM))
           &
           s__measure(V__X,s__MeasureFn(V__P2,V__PM))
       &
       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__RealNumber) &
         s__instance(V__P2,s__RealNumber) &
         s__instance(V__X,s__Object) &
         s__instance(V__PM,s__UnitOfMeasure))
       =>
       ((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__P1,V__PM))
           &
           s__measure(V__X,s__MeasureFn(V__P2,V__PM))
       &
       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 1109-1123
No TPTP formula. May not be expressible in strict first order. Weather.kif 2858-2872
No TPTP formula. May not be expressible in strict first order. Weather.kif 2909-2922
( ! [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 8694-8696
( ! [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 8690-8692
( ! [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 178-186


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 3.0 is open source software produced by Articulate Software and its partners