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

Formal Language: 



KB Term:  Term intersection
English Word: 

Sigma KEE - elevation
elevation

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


s__documentation(s__elevation__m,s__EnglishLanguage,'"(elevation ?OBJECT ?HEIGHT) means that the physical Object ?OBJECT is located on the surface of PlanetEarth at the vertical distance ?HEIGHT above (or below, for a negative quantity) SeaLevel. ?OBJECT may be a superficialPart of Earths surface, such as a GeographicArea. Elevation is measured from SeaLevel to the vertical top of the object."')

Geography.kif 1865-1870
s__domain(s__elevation__m,n__1,s__Object)

Geography.kif 1862-1862 The number 1 argument of elevation is an instance of object
s__domain(s__elevation__m,n__2,s__LengthMeasure)

Geography.kif 1863-1863 The number 2 argument of elevation is an instance of length measure
s__instance(s__BinaryPredicate,s__SetOrClass)

s__instance(s__elevation__m,s__BinaryPredicate)

Geography.kif 1861-1861 elevation is an instance of binary predicate

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


s__format(s__ChineseLanguage,s__elevation__m,'"%2 %n 是 %1 的 elevation "')

domainEnglishFormat.kif 891-891
s__format(s__ChineseTraditionalLanguage,s__elevation__m,'"%2 %n 是 %1 的 elevation "')

domainEnglishFormat.kif 890-890
s__format(s__EnglishLanguage,s__elevation__m,'"%2 is %n an elevation of %1"')

domainEnglishFormat.kif 889-889
s__termFormat(s__ChineseLanguage,s__elevation__m,'"海拔"')

domainEnglishFormat.kif 21807-21807
s__termFormat(s__ChineseTraditionalLanguage,s__elevation__m,'"海拔"')

domainEnglishFormat.kif 21806-21806
s__termFormat(s__EnglishLanguage,s__elevation__m,'"elevation"')

domainEnglishFormat.kif 21805-21805

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


( ! [V__OBJECT,V__NUM,V__UNIT] :
   ((s__instance(V__NUM,s__RealNumber) =>
       (((s__elevation(V__OBJECT,s__MeasureFn(V__NUM,V__UNIT))
         &
         s__instance(V__UNIT,s__UnitOfLength) &
         s__instance(V__OBJECT,s__LandForm))
       =>
       (( ? [V__HIGHPOINT] :
           ((s__instance(V__HIGHPOINT,s__SelfConnectedObject) &
               (s__top(V__HIGHPOINT,V__OBJECT)
               &
               s__distance(V__HIGHPOINT,s__SeaLevel,s__MeasureFn(V__NUM,V__UNIT))))))))))
)
)

Geography.kif 1893-1901
( ! [V__OBJECT,V__HEIGHT,V__PLACE] :
   (((s__instance(V__OBJECT,s__Object) &
         s__instance(V__HEIGHT,s__LengthMeasure))
       =>
       (((s__elevation(V__OBJECT,V__HEIGHT)
           &
           s__located(V__OBJECT,V__PLACE)
         &
         s__instance(V__PLACE,s__GeographicArea))
       =>
       (s__superficialPart(V__PLACE,s__PlanetEarth)))))
)
)

Geography.kif 1878-1883
( ! [V__AREA,V__ELEV1] :
   ((s__instance(V__ELEV1,s__LengthMeasure) =>
       (((s__instance(V__AREA,s__GeographicArea) &
             s__geographicSubregion(s__ElevationHighPointFn(V__AREA)
          ,V__AREA)
         &
         s__elevation(s__ElevationHighPointFn(V__AREA)
      ,V__ELEV1))
   =>
   (~(( ? [V__OTHER, V__ELEV2] :
         ((s__instance(V__OTHER,s__GeographicArea) &
             s__instance(V__ELEV2,s__LengthMeasure) &
             (s__geographicSubregion(V__OTHER,V__AREA)
             &
             ~((V__OTHER = s__ElevationHighPointFn(V__AREA)))
           &
           s__elevation(V__OTHER,V__ELEV2)
         &
         s__greaterThan(V__ELEV2,V__ELEV1))))))))))
)
)

Geography.kif 1935-1946
( ! [V__U,V__AREA,V__ELEV1] :
   ((s__instance(V__ELEV1,s__RealNumber) =>
       (((s__instance(V__AREA,s__GeographicArea) &
             s__geographicSubregion(s__ElevationLowPointFn(V__AREA)
          ,V__AREA)
         &
         s__instance(V__U,s__UnitOfLength) &
         s__elevation(s__ElevationLowPointFn(V__AREA)
      ,s__MeasureFn(V__ELEV1,V__U)))
=>
(~(( ? [V__OTHER, V__ELEV2] :
       ((s__instance(V__OTHER,s__GeographicArea) &
           s__instance(V__ELEV2,s__RealNumber) &
           (s__geographicSubregion(V__OTHER,V__AREA)
           &
           ~((V__OTHER = s__ElevationLowPointFn(V__AREA)))
         &
         s__elevation(V__OTHER,s__MeasureFn(V__ELEV2,V__U))
     &
     s__lessThan(V__ELEV2,V__ELEV1))))))))))
)
)

Geography.kif 1911-1925
No TPTP formula. May not be expressible in strict first order. Geography.kif 6309-6322
( ! [V__DIST,V__TIME,V__PLACE,V__ZEPHYR,V__X] :
   (((s__instance(V__DIST,s__LengthMeasure) &
         s__instance(V__TIME,s__TimeDuration) &
         s__instance(V__X,s__RealNumber))
       =>
       (((s__instance(V__ZEPHYR,s__WindFlow) &
             s__instance(V__PLACE,s__Object) &
             s__partlyLocated(V__ZEPHYR,V__PLACE)
           &
           s__elevation(V__ZEPHYR,s__MeasureFn(V__X,s__FootLength))
         &
         s__lessThanOrEqualTo(V__X,n__500)
       &
       s__measure(V__ZEPHYR,s__SpeedFn(V__DIST,V__TIME)))
=>
(s__surfaceWindSpeed(V__PLACE,s__SpeedFn(V__DIST,V__TIME))))))
)
)

Weather.kif 148-157
( ! [V__OBJECT,V__HEIGHT] :
   (((s__instance(V__OBJECT,s__Object) &
         s__instance(V__HEIGHT,s__LengthMeasure))
       =>
       ((s__elevation(V__OBJECT,V__HEIGHT)
         =>
         (( ? [V__DATUM] :
             ((s__instance(V__DATUM,s__Object) &
                 (s__properPart(V__DATUM,s__SeaLevel) &
                   s__orientation(V__OBJECT,V__DATUM,s__Vertical) &
                   s__distance(V__OBJECT,V__DATUM,V__HEIGHT)))))))))
)
)

Geography.kif 1885-1891
( ! [V__OBJECT,V__HEIGHT] :
   (((s__instance(V__OBJECT,s__Object) &
         s__instance(V__HEIGHT,s__LengthMeasure))
       =>
       ((s__elevation(V__OBJECT,V__HEIGHT)
         =>
         (( ? [V__PLACE] :
             ((s__instance(V__PLACE,s__GeographicArea) &
                 s__located(V__OBJECT,V__PLACE))))))))
)
)

Geography.kif 1872-1877

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


( ! [V__AREA,V__ELEV1] :
   ((s__instance(V__ELEV1,s__LengthMeasure) =>
       (((s__instance(V__AREA,s__GeographicArea) &
             s__geographicSubregion(s__ElevationHighPointFn(V__AREA)
          ,V__AREA)
         &
         s__elevation(s__ElevationHighPointFn(V__AREA)
      ,V__ELEV1))
   =>
   (~(( ? [V__OTHER, V__ELEV2] :
         ((s__instance(V__OTHER,s__GeographicArea) &
             s__instance(V__ELEV2,s__LengthMeasure) &
             (s__geographicSubregion(V__OTHER,V__AREA)
             &
             ~((V__OTHER = s__ElevationHighPointFn(V__AREA)))
           &
           s__elevation(V__OTHER,V__ELEV2)
         &
         s__greaterThan(V__ELEV2,V__ELEV1))))))))))
)
)

Geography.kif 1935-1946
( ! [V__U,V__AREA,V__ELEV1] :
   ((s__instance(V__ELEV1,s__RealNumber) =>
       (((s__instance(V__AREA,s__GeographicArea) &
             s__geographicSubregion(s__ElevationLowPointFn(V__AREA)
          ,V__AREA)
         &
         s__instance(V__U,s__UnitOfLength) &
         s__elevation(s__ElevationLowPointFn(V__AREA)
      ,s__MeasureFn(V__ELEV1,V__U)))
=>
(~(( ? [V__OTHER, V__ELEV2] :
       ((s__instance(V__OTHER,s__GeographicArea) &
           s__instance(V__ELEV2,s__RealNumber) &
           (s__geographicSubregion(V__OTHER,V__AREA)
           &
           ~((V__OTHER = s__ElevationLowPointFn(V__AREA)))
         &
         s__elevation(V__OTHER,s__MeasureFn(V__ELEV2,V__U))
     &
     s__lessThan(V__ELEV2,V__ELEV1))))))))))
)
)

Geography.kif 1911-1925
( ! [V__BAROMETER,V__OBJ,V__MEASURE,V__QUANTITY] :
   (((s__instance(V__OBJ,s__SelfConnectedObject) &
         s__instance(V__QUANTITY,s__LengthMeasure))
       =>
       (((s__instance(V__MEASURE,s__Measuring) &
             s__patient(V__MEASURE,V__OBJ)
           &
           s__surface(V__OBJ,s__PlanetEarth) &
           s__result(V__MEASURE,V__QUANTITY)
         &
         s__instrument(V__MEASURE,V__BAROMETER)
       &
       s__instance(V__BAROMETER,s__BarometricAltimeter))
     =>
     (s__elevation(V__OBJ,V__QUANTITY)))))
)
)

MilitaryDevices.kif 1488-1496
No TPTP formula. May not be expressible in strict first order. Geography.kif 6309-6322
( ! [V__ocean,V__top] :
   ((s__instance(V__top,s__SelfConnectedObject) =>
       (((s__instance(V__ocean,s__Ocean) &
             s__surface(V__top,V__ocean))
         =>
         (s__elevation(V__top,s__MeasureFn(n__0,s__FootLength))))))
)
)

Geography.kif 4624-4628
( ! [V__ocean,V__top] :
   ((s__instance(V__top,s__SelfConnectedObject) =>
       (((s__instance(V__ocean,s__Ocean) &
             s__surface(V__top,V__ocean))
         =>
         (s__elevation(V__top,s__MeasureFn(n__0,s__Meter))))))
)
)

Geography.kif 4618-4622
No TPTP formula. May not be expressible in strict first order. Weather.kif 1731-1741

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


s__elevation(s__ElevationHighPointFn(s__SouthernOcean),s__MeasureFn(n__0,s__Meter))

Geography.kif 4485-4485 0 Meter(s) is an elevation of the elevation high point of southern ocean
s__elevation(s__ElevationLowPointFn(s__SouthernOcean),s__MeasureFn(n___7235,s__Meter))

Geography.kif 4486-4486 -7235 Meter(s) is an elevation of the elevation low point of southern ocean
s__elevation(s__SeaLevel,s__MeasureFn(n__0,s__Meter))

Geography.kif 4616-4616 0 Meter(s) is an elevation of sea level


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