Browsing Interface
: Welcome guest :
log in
[
Home
| 
Graph
|  ]
KB:
SUMO
Language:
ChineseLanguage
ChinesePinyinWriting
ChineseSimplifiedWriting
ChineseTraditionalLanguage
EnglishLanguage
FrenchLanguage
GermanLanguage
JapaneseLanguage
SpanishLanguage
SwedishLanguage
Formal Language:
OWL
SUO-KIF
TPTP
traditionalLogic
KB Term:
Term intersection
English Word:
Any
Noun
Verb
Adjective
Adverb
MeasureFn
Sigma KEE - MeasureFn
MeasureFn
appearance as argument number 1
(
documentation
MeasureFn
ChineseLanguage
"这个
BinaryFunction
把一个
RealNumber
和一个
UnitOfMeasure
联系成这个
Number
的单位。 这是用来表达
PhysicalQuantity
的某种分量的实例。 例如:三米可以这样来表示 (
MeasureFn
3
Meter
)。")
chinese_format.kif 2434-2436
(
documentation
MeasureFn
EnglishLanguage
"This
BinaryFunction
maps a
RealNumber
and a
UnitOfMeasure
to that
Number
of units. It is used to express `measured' instances of
PhysicalQuantity
. Example: the concept of three meters is represented as (
MeasureFn
3
Meter
).")
Merge.kif 6256-6260
(
domain
MeasureFn
1
RealNumber
)
Merge.kif 6252-6252
The number 1 argument of
measure
is an
instance
of
real number
(
domain
MeasureFn
2
UnitOfMeasure
)
Merge.kif 6253-6253
The number 2 argument of
measure
is an
instance
of
unit of measure
(
instance
MeasureFn
BinaryFunction
)
Merge.kif 6250-6250
Measure
is an
instance
of
binary function
(
instance
MeasureFn
TotalValuedRelation
)
Merge.kif 6251-6251
Measure
is an
instance
of
total valued relation
(
range
MeasureFn
PhysicalQuantity
)
Merge.kif 6254-6254
The
range
of
measure
is an instance of
physical quantity
appearance as argument number 2
(
format
ChineseLanguage
MeasureFn
"%1 %2")
chinese_format.kif 633-633
(
format
EnglishLanguage
MeasureFn
"%1 %2(s)")
english_format.kif 636-636
(
termFormat
ChineseLanguage
MeasureFn
"测量")
domainEnglishFormat.kif 36654-36654
(
termFormat
ChineseLanguage
MeasureFn
"计量函数")
chinese_format.kif 634-634
(
termFormat
ChineseTraditionalLanguage
MeasureFn
"測量")
domainEnglishFormat.kif 36653-36653
(
termFormat
EnglishLanguage
MeasureFn
"measure")
domainEnglishFormat.kif 36652-36652
antecedent
(<=>
(
and
(
instance
?LD
LiquidDrop
)
(
approximateDiameter
?LD
(
MeasureFn
?S
Micrometer
))
(
lessThan
500.0 ?S))
(
instance
?LD
Droplet
))
Geography.kif 7240-7246
A self connected object
is an
instance
of
liquid drop
and the
approximate
diameter
of
the self connected object
is
a real number
micrometer
(s) and 500.0 is
less
than
the real number
if and only if
the self connected object
is an
instance
of
droplet
(<=>
(
and
(
instance
?PM
ParticulateMatter
)
(
part
?P ?PM)
(
approximateDiameter
?P
(
MeasureFn
?S
Micrometer
))
(
greaterThan
10.0 ?S)
(
greaterThan
?S 2.5))
(
exists
(?PM10)
(
and
(
instance
?PM10
CoarseParticulateMatter
)
(
part
?PM10 ?PM))))
Geography.kif 7156-7167
An object
is an
instance
of
PM
and
a self connected object
is a
part
of
the object
and the
approximate
diameter
of
the self connected object
is
a real number
micrometer
(s) and 10.0 is
greater
than
the real number
and
the real number
is
greater
than 2.5 if and only if there exists
the object
10 such that
the object
10 is an
instance
of
PM10
and
the object
10 is a
part
of
the object
(<=>
(
and
(
instance
?PM
ParticulateMatter
)
(
part
?P ?PM)
(
approximateDiameter
?P
(
MeasureFn
?S
Micrometer
))
(
greaterThanOrEqualTo
?S 2.5))
(
exists
(?PM25)
(
and
(
instance
?PM25
FineParticulateMatter
)
(
part
?PM25 ?PM))))
Geography.kif 7185-7195
An object
is an
instance
of
PM
and
a self connected object
is a
part
of
the object
and the
approximate
diameter
of
the self connected object
is
a real number
micrometer
(s) and
the real number
is
greater
than or equal to 2.5 if and only if there exists
the object
25 such that
the object
25 is an
instance
of
PM2.5
and
the object
25 is a
part
of
the object
(<=>
(
courseWRTTrueNorth
?OBJ1 ?OBJ2
(
MeasureFn
0.0
AngularDegree
))
(
orientation
?OBJ1 ?OBJ2
North
))
Geography.kif 3653-3655
An object
courseWRT
true north
another object
for 0.0
angular degree
(s) if and only if
the object
is
north
to
the other object
(<=>
(
courseWRTTrueNorth
?OBJ1 ?OBJ2
(
MeasureFn
135.0
AngularDegree
))
(
orientation
?OBJ1 ?OBJ2
Southeast
))
Geography.kif 3677-3679
An object
courseWRT
true north
another object
for 135.0
angular degree
(s) if and only if
the object
is
southeast
to
the other object
(<=>
(
courseWRTTrueNorth
?OBJ1 ?OBJ2
(
MeasureFn
180.0
AngularDegree
))
(
orientation
?OBJ1 ?OBJ2
South
))
Geography.kif 3661-3663
An object
courseWRT
true north
another object
for 180.0
angular degree
(s) if and only if
the object
is
south
to
the other object
(<=>
(
courseWRTTrueNorth
?OBJ1 ?OBJ2
(
MeasureFn
225.0
AngularDegree
))
(
orientation
?OBJ1 ?OBJ2
Southwest
))
Geography.kif 3681-3683
An object
courseWRT
true north
another object
for 225.0
angular degree
(s) if and only if
the object
is
southwest
to
the other object
(<=>
(
courseWRTTrueNorth
?OBJ1 ?OBJ2
(
MeasureFn
270.0
AngularDegree
))
(
orientation
?OBJ1 ?OBJ2
West
))
Geography.kif 3665-3667
An object
courseWRT
true north
another object
for 270.0
angular degree
(s) if and only if
the object
is
west
to
the other object
(<=>
(
courseWRTTrueNorth
?OBJ1 ?OBJ2
(
MeasureFn
315.0
AngularDegree
))
(
orientation
?OBJ1 ?OBJ2
Northwest
))
Geography.kif 3685-3687
An object
courseWRT
true north
another object
for 315.0
angular degree
(s) if and only if
the object
is
northwest
to
the other object
(<=>
(
courseWRTTrueNorth
?OBJ1 ?OBJ2
(
MeasureFn
360.0
AngularDegree
))
(
orientation
?OBJ1 ?OBJ2
North
))
Geography.kif 3669-3671
An object
courseWRT
true north
another object
for 360.0
angular degree
(s) if and only if
the object
is
north
to
the other object
(<=>
(
courseWRTTrueNorth
?OBJ1 ?OBJ2
(
MeasureFn
45.0
AngularDegree
))
(
orientation
?OBJ1 ?OBJ2
Northeast
))
Geography.kif 3673-3675
An object
courseWRT
true north
another object
for 45.0
angular degree
(s) if and only if
the object
is
northeast
to
the other object
(<=>
(
courseWRTTrueNorth
?OBJ1 ?OBJ2
(
MeasureFn
90.0
AngularDegree
))
(
orientation
?OBJ1 ?OBJ2
East
))
Geography.kif 3657-3659
An object
courseWRT
true north
another object
for 90.0
angular degree
(s) if and only if
the object
is
east
to
the other object
(<=>
(
equal
?SPEED
(
MeasureFn
?NUM
MilesPerHour
))
(
equal
?SPEED
(
SpeedFn
(
MeasureFn
?NUM
Mile
)
(
MeasureFn
1
HourDuration
))))
Weather.kif 1701-1707
A function quantity
is
equal
to
a real number
miles per hour
(s) if and only if
the function quantity
is
equal
to
the real number
mile
(s)
per
1
hour duration
(s)
(<=>
(
measure
?O
(
MeasureFn
?A
MetricTon
))
(
measure
?O
(
MeasureFn
(
MultiplicationFn
?A 2205.0)
PoundMass
)))
Mid-level-ontology.kif 13071-13077
The
measure
of
a physical
is
a real number
metric ton
(s) if and only if the
measure
of
the physical
is
the real number
and 2205.0
pound mass
(s)
(<=>
(
measure
?OBJ
(
MeasureFn
?DEG
AngularDegree
))
(
measure
?OBJ
(
MeasureFn
(
MultiplicationFn
60.0 ?DEG)
ArcMinute
)))
Geography.kif 378-380
The
measure
of
a physical
is
a real number
angular degree
(s) if and only if the
measure
of
the physical
is 60.0 and
the real number
arc minute
(s)
(<=>
(
measure
?OBJ
(
MeasureFn
?DEG
ArcMinute
))
(
measure
?OBJ
(
MeasureFn
(
MultiplicationFn
60.0 ?DEG)
ArcSecond
)))
Geography.kif 397-399
The
measure
of
a physical
is
a real number
arc minute
(s) if and only if the
measure
of
the physical
is 60.0 and
the real number
arc second
(s)
(<=>
(
measure
?OBJECT
(
MeasureFn
?NUMBER
OunceMass
))
(
measure
?OBJECT
(
MeasureFn
(
DivisionFn
?NUMBER 16.0)
PoundMass
)))
Mid-level-ontology.kif 12787-12792
The
measure
of
a physical
is
a real number
Ounce
(s) if and only if the
measure
of
the physical
is
the real number
and 16.0
pound mass
(s)
(<=>
(
measure
?SOLUTION
(
MeasureFn
?PH
PHValue
))
(
potentialOfHydrogen
?SOLUTION ?PH))
Geography.kif 2551-2554
The
measure
of
a solution
is
a real number
PH value
(s) if and only if
the real number
is a
potential
of hydrogen of
the solution
(<=>
(
sectorValueOfGDPInPeriod
?AREA ?SECTOR
(
MeasureFn
?AMOUNT ?CUNIT) ?PERIOD)
(
exists
(?TIME)
(
and
(
instance
?TIME ?PERIOD)
(
holdsDuring
?TIME
(
sectorValueOfGDP
?AREA ?SECTOR
(
MeasureFn
?AMOUNT ?CUNIT))))))
Economy.kif 1124-1132
A geopolitical area
is
sector
value of GDP in period
an industry attribute
for
a real number
an unit of measure
(s) with
a kind of time interval
if and only if there exists
a time position
such that
the time position
is an
instance
of
a kind of time interval
and
the geopolitical area
is
sector
value of GDP
the industry attribute
for
the real number
the unit of measure
(s) holds
during
the time position
(=>
(
and
(
amount
?S ?CO
(
MeasureFn
?N ?U))
(
instance
?SI ?S)
(
measure
?SI
(
MeasureFn
?N2 ?U))
(
part
?SI ?CO))
(
exists
(?L)
(
and
(
inList
(
MeasureFn
?N2 ?U) ?L)
(
equal
?L
(
AmountsFn
?S ?CO ?U))
(
equal
?N
(
ListSumFn
?L)))))
Merge.kif 7500-7515
If
amount
a kind of substance
,
a corpuscular object
and
a real number
an UnitOfMass
(s) and
a kind of substance
I is an
instance
of
the kind of substance
and the
measure
of
the kind of substance
I is
the real number
2
the UnitOfMass
(s) and
the kind of substance
I is a
part
of
the corpuscular object
,
then there exists
a list
such that
the real number
2
the UnitOfMass
(s) is a
member
of
the list
and
the list
is
equal
to
AmountsFn
the kind of substance
,
the corpuscular object
and
the UnitOfMass
and
the real number
is
equal
to the
sum
of
the list
(=>
(
and
(
approximateDiameter
?O
(
MeasureFn
?L ?LM))
(
sphereRadius
?S
(
MeasureFn
(
DivisionFn
?L 2.0) ?LM))
(
measure
?S
(
MeasureFn
?V1 ?VM))
(
measure
?O
(
MeasureFn
?V2 ?VM))
(
instance
?LM
LengthMeasure
)
(
instance
?VM
VolumeMeasure
))
(
equal
?V1 ?V2))
Mid-level-ontology.kif 17340-17351
If the
approximate
diameter
of
a self connected object
is
a real number
the real number
M(s) and the
radius
of
an object
is
the real number
and 2.0
the real number
M(s) and the
measure
of
the object
is
another real number
another unit of measure
(s) and the
measure
of
the self connected object
is
a third real number
the other unit of measure
(s) and
the real number
M is an
instance
of
length measure
and
the other unit of measure
is an
instance
of
volume measure
,
then
the other real number
is
equal
to
the third real number
(=>
(
and
(
arableLandArea
?REGION
(
MeasureFn
?FRACTION ?UNIT))
(
greaterThanOrEqualTo
?FRACTION 0.0)
(
totalArea
?REGION
(
MeasureFn
?TOTAL ?UNIT))
(
instance
?TOTAL
AreaMeasure
)
(
equal
?AMOUNT
(
MultiplicationFn
?FRACTION ?TOTAL)))
(
arableLandArea
?REGION
(
MeasureFn
?AMOUNT ?UNIT)))
Geography.kif 2083-2093
If
a real number
an unit of measure
(s) is an
arable
land area of
a geographic area
and
the real number
is
greater
than or equal to 0.0 and
another real number
the unit of measure
(s) is a
total
area of
the geographic area
and
the other real number
is an
instance
of
area measure
and
a third real number
is
equal
to
the real number
and
the other real number
,
then
the third real number
the unit of measure
(s) is an
arable
land area of
the geographic area
(=>
(
and
(
arableLandArea
?REGION
(
MeasureFn
?FRACTION ?UNIT))
(
greaterThanOrEqualTo
?FRACTION 0.0)
(
totalArea
?REGION
(
MeasureFn
?TOTAL ?UNIT))
(
instance
?UNIT
UnitOfArea
))
(
exists
(?ARABLE)
(
and
(
instance
?ARABLE
ArableLand
)
(
geographicSubregion
?ARABLE ?REGION)
(
measure
?ARABLE
(
MeasureFn
(
MultiplicationFn
?FRACTION ?TOTAL) ?UNIT)))))
Geography.kif 2095-2109
If
a real number
an unit of measure
(s) is an
arable
land area of
a geographic area
and
the real number
is
greater
than or equal to 0.0 and
another real number
the unit of measure
(s) is a
total
area of
the geographic area
and
the unit of measure
is an
instance
of
UnitOfArea
,
then there exists
another geographic area
such that
the other geographic area
is an
instance
of
arable land
and
the other geographic area
is a
geographic
subregion of
the geographic area
and the
measure
of
the other geographic area
is
the real number
and
the other real number
the unit of measure
(s)
(=>
(
and
(
attribute
?FOOD1
FamilyStylePortion
)
(
measure
?FOOD1
(
MeasureFn
?MEAS1 ?U))
(
not
(
attribute
?FOOD2
FamilyStylePortion
))
(
measure
?FOOD2
(
MeasureFn
?MEAS2 ?U))
(
instance
?FOOD1 ?CLASS)
(
instance
?FOOD2 ?CLASS)
(
instance
?U
UnitOfMeasure
))
(
greaterThan
?MEAS1 ?MEAS2))
Dining.kif 1118-1129
If
family-style portions
is an
attribute
of
an object
and the
measure
of
the object
is
a real number
an unit of measure
(s) and
family-style portions
is not an
attribute
of
another object
and the
measure
of
the other object
is
another real number
the unit of measure
(s) and
the object
is an
instance
of
a class
and
the other object
is an
instance
of
the class
and
the unit of measure
is an
instance
of
unit of measure
,
then
the real number
is
greater
than
the other real number
(=>
(
and
(
boilingPoint
?TYPE
(
MeasureFn
?TEMP1 ?MEASURE))
(
instance
?SUBSTANCE ?TYPE)
(
holdsDuring
?TIME
(
measure
?SUBSTANCE
(
MeasureFn
?TEMP2 ?MEASURE)))
(
instance
?MEASURE
UnitOfTemperature
)
(
greaterThanOrEqualTo
?TEMP2 ?TEMP1))
(
or
(
holdsDuring
?TIME
(
attribute
?SUBSTANCE
Gas
))
(
exists
(?BOIL)
(
and
(
overlapsTemporally
(
WhenFn
?BOIL) ?TIME)
(
instance
?BOIL
Boiling
)
(
patient
?BOIL ?SUBSTANCE)))))
Merge.kif 13594-13607
If
a real number
an unit of measure
(s) is a
boiling
point of
a kind of pure substance
and
an entity
is an
instance
of
a kind of pure substance
and the
measure
of
the entity
is
another real number
the unit of measure
(s) holds
during
a time interval
and
the unit of measure
is an
instance
of
UnitOfTemperature
and
the other real number
is
greater
than or equal to
the real number
,
then
gas
is an
attribute
of
the entity
holds
during
the time interval
or there exists
a process
such that
the time interval
overlap
s the
time
of existence of
the process
and
the process
is an
instance
of
boiling
and
the entity
is a
patient
of
the process
Display limited to 25 items.
Show next 25
Display limited to 25 items.
Show next 25
consequent
(<=>
(
and
(
instance
?X
Region
)
(
holdsDuring
?T
(
property
?X
StandardAmbientTemperaturePressure
)))
(
holdsDuring
?T
(
and
(
airTemperature
?X
(
MeasureFn
298.15
KelvinDegree
))
(
barometricPressure
?X
(
MeasureFn
29.530
InchMercury
)))))
Weather.kif 2679-2689
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
(<=>
(
and
(
instance
?Y
(
YearFn
?YEAR))
(
equal
(
MaleLifeExpectancyAtBirthFn
?AREA ?Y) ?REALNUMBER))
(
exists
(?LIST)
(
and
(
instance
?LIST
List
)
(
instance
(
ListLengthFn
?LIST) ?COUNT)
(
forall
(?LISTITEM)
(=>
(
inList
?LISTITEM ?LIST)
(
and
(
instance
?LISTITEM ?LIFEEXPECTANCYAGE)
(
not
(
exists
(?NUMBER)
(
and
(
instance
?NUMBER ?LIFEEXPECTANCYAGE)
(
not
(
inList
?NUMBER ?LIST)))))
(
equal
?COUNT
(
CardinalityFn
(
KappaFn
?LIFEEXPECTANCYAGE
(
and
(
instance
?BIRTH
Birth
)
(
experiencer
?BIRTH ?INDIVIDUAL)
(
instance
?INDIVIDUAL
Human
)
(
attribute
?INDIVIDUAL
Male
)
(
during
(
WhenFn
?BIRTH) ?Y)
(
equal
(
WhereFn
?BIRTH
(
WhenFn
?BIRTH)) ?AREA)
(
instance
?DEATH
Death
)
(
experiencer
?DEATH ?INDIVIDUAL)
(
holdsDuring
(
WhenFn
?DEATH)
(
age
?INDIVIDUAL
(
MeasureFn
?LIFEEXPECTANCYAGE
YearDuration
))))))))))
(
average
?LIST ?REALNUMBER))))
People.kif 372-405
A year
is an
instance
of the
year
the year
EAR and the
male
life expectancy at birth of
a geopolitical area
and
the year
is
equal
to
a real number
if and only if there exists
a list
such that
the list
is an
instance
of
list
and
length
of
the list
is an
instance
of
another integer
and for all
the list
ITEM
if
the list
ITEM is a
member
of
the list
,
then
the list
ITEM is an
instance
of
a symbolic string
and there doesn't exist
another entity
such that
the other entity
is an
instance
of
the symbolic string
and
the other entity
is not a
member
of
the list
and
the other integer
is
equal
to the number of
instances
in the
class
described by
the symbolic string
and
the real number
is an
average
of
the list
(<=>
(
attribute
?WATER
OpenSea
)
(
and
(
instance
?WATER
SaltWaterArea
)
(
not
(
instance
?WATER
LandlockedWater
))
(
distance
?LAND ?WATER
(
MeasureFn
?DIST
NauticalMile
))
(
greaterThan
?DIST 5.0)))
Geography.kif 4610-4618
Open sea
is an
attribute
of
an object
if and only if
the object
is an
instance
of
salt water area
and
the object
is not an
instance
of
landlocked water
and the
distance
between
a physical
and
the object
is
a real number
nautical mile
(s) and
the real number
is
greater
than 5.0
(<=>
(
compressionRatio
?E ?R)
(
and
(
minCylinderVolume
?E
(
MeasureFn
?MIN ?M))
(
maxCylinderVolume
?E
(
MeasureFn
?MAX ?M))
(
equal
?R
(
DivisionFn
?MIN ?MAX))))
Cars.kif 1928-1933
The compression ratio of
an engine
is
a real number
if and only if the minimum volume of the cylinders in the engine
the engine
is
another real number
an unit of measure
(s) and the maximum volume of the cylinders in the engine
the engine
is
the unit of measure
AX
the unit of measure
(s) and
the real number
is
equal
to
the other real number
and
the unit of measure
AX
(<=>
(
equal
(
DeathsPerThousandLiveBirthsFn
?AREA
(
YearFn
?YEAR)) ?REALNUMBER)
(
and
(
equal
?BIRTHCOUNT
(
CardinalityFn
(
KappaFn
?BIRTH
(
and
(
instance
?BIRTH
Birth
)
(
experiencer
?BIRTH ?INFANT)
(
instance
?INFANT
Human
)
(
during
(
WhenFn
?BIRTH)
(
YearFn
?YEAR))
(
equal
(
WhereFn
?BIRTH
(
WhenFn
?BIRTH)) ?AREA)))))
(
equal
(
DivisionFn
?BIRTHCOUNT 1000) ?THOUSANDSOFBIRTHS)
(
equal
?INFANTDEATHCOUNT
(
CardinalityFn
(
KappaFn
?DEATH
(
and
(
instance
?DEATH
Death
)
(
experiencer
?DEATH ?INFANT)
(
instance
?INFANT
Human
)
(
age
?INFANT
(
MeasureFn
?AGE
YearDuration
))
(
lessThan
?AGE 1)
(
during
(
WhenFn
?DEATH)
(
YearFn
?YEAR))
(
equal
(
WhereFn
?DEATH
(
WhenFn
?DEATH)) ?AREA)))))
(
equal
(
DivisionFn
?INFANTDEATHCOUNT ?THOUSANDSOFBIRTHS) ?REALNUMBER)))
People.kif 257-281
The
deaths
per thousand live births of
a geopolitical area
and the
year
an integer
is
equal
to
a real number
if and only if
another integer
is
equal
to the number of
instances
in the
class
described by
a symbolic string
and
the other integer
and 1000 is
equal
to
another real number
and
a third integer
is
equal
to the number of
instances
in the
class
described by
another symbolic string
and
the third integer
and
the other real number
is
equal
to
the real number
(<=>
(
equal
(
FemaleLifeExpectancyAtBirthFn
?AREA
(
YearFn
?YEAR)) ?REALNUMBER)
(
exists
(?LIST)
(
and
(
instance
?LIST
List
)
(
instance
(
ListLengthFn
?LIST) ?COUNT)
(
forall
(?LISTITEM)
(=>
(
inList
?LISTITEM ?LIST)
(
and
(
instance
?LISTITEM ?LIFEEXPECTANCYAGE)
(
not
(
exists
(?NUMBER)
(
and
(
instance
?NUMBER ?LIFEEXPECTANCYAGE)
(
not
(
inList
?NUMBER ?LIST)))))
(
equal
?COUNT
(
CardinalityFn
(
KappaFn
?LIFEEXPECTANCYAGE
(
and
(
instance
?BIRTH
Birth
)
(
experiencer
?BIRTH ?INDIVIDUAL)
(
instance
?INDIVIDUAL
Human
)
(
attribute
?INDIVIDUAL
Female
)
(
during
(
WhenFn
?BIRTH)
(
YearFn
?YEAR))
(
equal
(
WhereFn
?BIRTH
(
WhenFn
?BIRTH)) ?AREA)
(
instance
?DEATH
Death
)
(
experiencer
?DEATH ?INDIVIDUAL)
(
holdsDuring
(
WhenFn
?DEATH)
(
age
?INDIVIDUAL
(
MeasureFn
?LIFEEXPECTANCYAGE
YearDuration
))))))))))
(
average
?LIST ?REALNUMBER))))
People.kif 418-449
The
female
life expectancy at birth of
a geopolitical area
and the
year
an integer
is
equal
to
a real number
if and only if there exists
a list
such that
the list
is an
instance
of
list
and
length
of
the list
is an
instance
of
another integer
and for all
the list
ITEM
if
the list
ITEM is a
member
of
the list
,
then
the list
ITEM is an
instance
of
a symbolic string
and there doesn't exist
another entity
such that
the other entity
is an
instance
of
the symbolic string
and
the other entity
is not a
member
of
the list
and
the other integer
is
equal
to the number of
instances
in the
class
described by
the symbolic string
and
the real number
is an
average
of
the list
(<=>
(
equal
(
LifeExpectancyAtBirthFn
?AREA
(
YearFn
?YEAR)) ?REALNUMBER)
(
exists
(?LIST)
(
and
(
instance
?LIST
List
)
(
instance
(
ListLengthFn
?LIST) ?COUNT)
(
forall
(?LISTITEM)
(=>
(
inList
?LISTITEM ?LIST)
(
and
(
instance
?LISTITEM ?LIFEEXPECTANCYAGE)
(
not
(
exists
(?NUMBER)
(
and
(
instance
?NUMBER ?LIFEEXPECTANCYAGE)
(
not
(
inList
?NUMBER ?LIST)))))
(
equal
?COUNT
(
CardinalityFn
(
KappaFn
?LIFEEXPECTANCYAGE
(
and
(
instance
?BIRTH
Birth
)
(
experiencer
?BIRTH ?INDIVIDUAL)
(
instance
?INDIVIDUAL
Human
)
(
during
(
WhenFn
?BIRTH)
(
YearFn
?YEAR))
(
equal
(
WhereFn
?BIRTH
(
WhenFn
?BIRTH)) ?AREA)
(
instance
?DEATH
Death
)
(
experiencer
?DEATH ?INDIVIDUAL)
(
holdsDuring
(
WhenFn
?DEATH)
(
age
?INDIVIDUAL
(
MeasureFn
?LIFEEXPECTANCYAGE
YearDuration
))))))))))
(
average
?LIST ?REALNUMBER))))
People.kif 327-357
The
life
expectancy at birth of
a geopolitical area
and the
year
an integer
is
equal
to
a real number
if and only if there exists
a list
such that
the list
is an
instance
of
list
and
length
of
the list
is an
instance
of
another integer
and for all
the list
ITEM
if
the list
ITEM is a
member
of
the list
,
then
the list
ITEM is an
instance
of
a symbolic string
and there doesn't exist
another entity
such that
the other entity
is an
instance
of
the symbolic string
and
the other entity
is not a
member
of
the list
and
the other integer
is
equal
to the number of
instances
in the
class
described by
the symbolic string
and
the real number
is an
average
of
the list
(<=>
(
equal
?SPEED
(
MeasureFn
?NUM
MilesPerHour
))
(
equal
?SPEED
(
SpeedFn
(
MeasureFn
?NUM
Mile
)
(
MeasureFn
1
HourDuration
))))
Weather.kif 1701-1707
A function quantity
is
equal
to
a real number
miles per hour
(s) if and only if
the function quantity
is
equal
to
the real number
mile
(s)
per
1
hour duration
(s)
(<=>
(
larger
?OBJ1 ?OBJ2)
(
forall
(?QUANT1 ?QUANT2 ?UNIT)
(=>
(
and
(
measure
?OBJ1
(
MeasureFn
?QUANT1 ?UNIT))
(
measure
?OBJ2
(
MeasureFn
?QUANT2 ?UNIT))
(
instance
?UNIT
UnitOfLength
))
(
greaterThan
?QUANT1 ?QUANT2))))
Merge.kif 7662-7670
An object
is
larger
than
another object
if and only if for all
a real number
,
another real number
and
an unit of measure
if the
measure
of
the object
is
the real number
the unit of measure
(s) and the
measure
of
the other object
is
the other real number
the unit of measure
(s) and
the unit of measure
is an
instance
of
UnitOfLength
,
then
the real number
is
greater
than
the other real number
(<=>
(
measure
?O
(
MeasureFn
?A
MetricTon
))
(
measure
?O
(
MeasureFn
(
MultiplicationFn
?A 2205.0)
PoundMass
)))
Mid-level-ontology.kif 13071-13077
The
measure
of
a physical
is
a real number
metric ton
(s) if and only if the
measure
of
the physical
is
the real number
and 2205.0
pound mass
(s)
(<=>
(
measure
?OBJ
(
MeasureFn
?DEG
AngularDegree
))
(
measure
?OBJ
(
MeasureFn
(
MultiplicationFn
60.0 ?DEG)
ArcMinute
)))
Geography.kif 378-380
The
measure
of
a physical
is
a real number
angular degree
(s) if and only if the
measure
of
the physical
is 60.0 and
the real number
arc minute
(s)
(<=>
(
measure
?OBJ
(
MeasureFn
?DEG
ArcMinute
))
(
measure
?OBJ
(
MeasureFn
(
MultiplicationFn
60.0 ?DEG)
ArcSecond
)))
Geography.kif 397-399
The
measure
of
a physical
is
a real number
arc minute
(s) if and only if the
measure
of
the physical
is 60.0 and
the real number
arc second
(s)
(<=>
(
measure
?OBJECT
(
MeasureFn
?NUMBER
OunceMass
))
(
measure
?OBJECT
(
MeasureFn
(
DivisionFn
?NUMBER 16.0)
PoundMass
)))
Mid-level-ontology.kif 12787-12792
The
measure
of
a physical
is
a real number
Ounce
(s) if and only if the
measure
of
the physical
is
the real number
and 16.0
pound mass
(s)
(<=>
(
sectorValueOfGDPInPeriod
?AREA ?SECTOR
(
MeasureFn
?AMOUNT ?CUNIT) ?PERIOD)
(
exists
(?TIME)
(
and
(
instance
?TIME ?PERIOD)
(
holdsDuring
?TIME
(
sectorValueOfGDP
?AREA ?SECTOR
(
MeasureFn
?AMOUNT ?CUNIT))))))
Economy.kif 1124-1132
A geopolitical area
is
sector
value of GDP in period
an industry attribute
for
a real number
an unit of measure
(s) with
a kind of time interval
if and only if there exists
a time position
such that
the time position
is an
instance
of
a kind of time interval
and
the geopolitical area
is
sector
value of GDP
the industry attribute
for
the real number
the unit of measure
(s) holds
during
the time position
(=>
(
and
(
amount
?S ?CO
(
MeasureFn
?N ?U))
(
instance
?SI ?S)
(
measure
?SI
(
MeasureFn
?N2 ?U))
(
part
?SI ?CO))
(
exists
(?L)
(
and
(
inList
(
MeasureFn
?N2 ?U) ?L)
(
equal
?L
(
AmountsFn
?S ?CO ?U))
(
equal
?N
(
ListSumFn
?L)))))
Merge.kif 7500-7515
If
amount
a kind of substance
,
a corpuscular object
and
a real number
an UnitOfMass
(s) and
a kind of substance
I is an
instance
of
the kind of substance
and the
measure
of
the kind of substance
I is
the real number
2
the UnitOfMass
(s) and
the kind of substance
I is a
part
of
the corpuscular object
,
then there exists
a list
such that
the real number
2
the UnitOfMass
(s) is a
member
of
the list
and
the list
is
equal
to
AmountsFn
the kind of substance
,
the corpuscular object
and
the UnitOfMass
and
the real number
is
equal
to the
sum
of
the list
(=>
(
and
(
arableLandArea
?REGION
(
MeasureFn
?FRACTION ?UNIT))
(
greaterThanOrEqualTo
?FRACTION 0.0)
(
totalArea
?REGION
(
MeasureFn
?TOTAL ?UNIT))
(
instance
?TOTAL
AreaMeasure
)
(
equal
?AMOUNT
(
MultiplicationFn
?FRACTION ?TOTAL)))
(
arableLandArea
?REGION
(
MeasureFn
?AMOUNT ?UNIT)))
Geography.kif 2083-2093
If
a real number
an unit of measure
(s) is an
arable
land area of
a geographic area
and
the real number
is
greater
than or equal to 0.0 and
another real number
the unit of measure
(s) is a
total
area of
the geographic area
and
the other real number
is an
instance
of
area measure
and
a third real number
is
equal
to
the real number
and
the other real number
,
then
the third real number
the unit of measure
(s) is an
arable
land area of
the geographic area
(=>
(
and
(
arableLandArea
?REGION
(
MeasureFn
?FRACTION ?UNIT))
(
greaterThanOrEqualTo
?FRACTION 0.0)
(
totalArea
?REGION
(
MeasureFn
?TOTAL ?UNIT))
(
instance
?UNIT
UnitOfArea
))
(
exists
(?ARABLE)
(
and
(
instance
?ARABLE
ArableLand
)
(
geographicSubregion
?ARABLE ?REGION)
(
measure
?ARABLE
(
MeasureFn
(
MultiplicationFn
?FRACTION ?TOTAL) ?UNIT)))))
Geography.kif 2095-2109
If
a real number
an unit of measure
(s) is an
arable
land area of
a geographic area
and
the real number
is
greater
than or equal to 0.0 and
another real number
the unit of measure
(s) is a
total
area of
the geographic area
and
the unit of measure
is an
instance
of
UnitOfArea
,
then there exists
another geographic area
such that
the other geographic area
is an
instance
of
arable land
and
the other geographic area
is a
geographic
subregion of
the geographic area
and the
measure
of
the other geographic area
is
the real number
and
the other real number
the unit of measure
(s)
(=>
(
and
(
attribute
?H
Muslim
)
(
equal
(
WealthFn
?H) ?W))
(
modalAttribute
(
exists
(?Z ?T ?U)
(
and
(
instance
?Z
Zakat
)
(
instance
?Y
Year
)
(
during
?Y
(
WhenFn
?H))
(
holdsDuring
?Y
(
attribute
?H
FullyFormed
))
(
agent
?Z ?H)
(
patient
?Z ?T)
(
monetaryValue
?T
(
MeasureFn
?C ?U))
(
instance
?U
UnitOfCurrency
)
(
greaterThan
?C
(
MultiplicationFn
?W 0.025))))
Obligation
))
ArabicCulture.kif 193-212
If
muslim
is an
attribute
of
an agent
and
value
of belongings of
the agent
is
equal
to
a currency measure
,
then the statement there exist
an entity
,
another entity
and
a third entity
such that
the entity
is an
instance
of
zakat
and
a fourth entity
is an
instance
of
year
and
the fourth entity
takes place
during
the
time
of existence of
the agent
and
fully formed
is an
attribute
of
the agent
holds
during
the fourth entity
and
the agent
is an
agent
of
the entity
and
the other entity
is a
patient
of
the entity
and
value
of
the other entity
is
a fifth entity
the third entity
(s) and
the third entity
is an
instance
of
UnitOfCurrency
and
the fifth entity
is
greater
than
the currency measure
and 0.025 has the
modal
force
of
obligation
(=>
(
and
(
attribute
?P
CollegeFreshman
)
(
occupiesPosition
?H ?P ?ORG))
(
exists
(?T)
(
and
(
holdsDuring
(
MeasureFn
?T
YearDuration
)
(
student
?H ?ORG))
(
lessThan
?T 1))))
Mid-level-ontology.kif 18079-18088
If
college freshman
is an
attribute
of
a position
and
a human
holds the
position
of
the position
in
an organization
,
then there exists
a real number
such that
the human
is a
student
of
the organization
holds
during
the real number
year duration
(s) and
the real number
is
less
than 1
(=>
(
and
(
attribute
?P
CollegeJunior
)
(
occupiesPosition
?H ?P ?ORG))
(
exists
(?T)
(
and
(
holdsDuring
(
MeasureFn
?T
YearDuration
)
(
student
?H ?ORG))
(
greaterThanOrEqualTo
?T 2)
(
lessThan
?T 3))))
Mid-level-ontology.kif 18094-18104
If
college junior
is an
attribute
of
a position
and
a human
holds the
position
of
the position
in
an organization
,
then there exists
a real number
such that
the human
is a
student
of
the organization
holds
during
the real number
year duration
(s) and
the real number
is
greater
than or equal to 2 and
the real number
is
less
than 3
(=>
(
and
(
attribute
?P
CollegeSenior
)
(
occupiesPosition
?H ?P ?ORG))
(
exists
(?T)
(
and
(
holdsDuring
(
MeasureFn
?T
YearDuration
)
(
student
?H ?ORG))
(
greaterThanOrEqualTo
?T 3)
(
lessThan
?T 4))))
Mid-level-ontology.kif 18110-18120
If
college senior
is an
attribute
of
a position
and
a human
holds the
position
of
the position
in
an organization
,
then there exists
a real number
such that
the human
is a
student
of
the organization
holds
during
the real number
year duration
(s) and
the real number
is
greater
than or equal to 3 and
the real number
is
less
than 4
(=>
(
and
(
attribute
?P
CollegeSophomore
)
(
occupiesPosition
?H ?P ?ORG))
(
exists
(?T)
(
and
(
holdsDuring
(
MeasureFn
?T
YearDuration
)
(
student
?H ?ORG))
(
greaterThanOrEqualTo
?T 1)
(
lessThan
?T 2))))
Mid-level-ontology.kif 18126-18136
If
college sophomore
is an
attribute
of
a position
and
a human
holds the
position
of
the position
in
an organization
,
then there exists
a real number
such that
the human
is a
student
of
the organization
holds
during
the real number
year duration
(s) and
the real number
is
greater
than or equal to 1 and
the real number
is
less
than 2
(=>
(
and
(
attribute
?ROOM
Oversized
)
(
immediateInstance
?ROOM ?HOTELUNIT)
(
subclass
?HOTELUNIT
HotelUnit
))
(
exists
(?NORMAL ?AREA1 ?AREA2 ?U)
(
and
(
immediateInstance
?NORMAL ?HOTELUNIT)
(
instance
?U
UnitOfArea
)
(
measure
?NORMAL
(
MeasureFn
?AREA1 ?U))
(
measure
?ROOM
(
MeasureFn
?AREA2 ?U))
(
instance
?AREA1
AreaMeasure
)
(
instance
?AREA2
AreaMeasure
)
(
greaterThan
?AREA2 ?AREA1))))
Hotel.kif 1164-1179
If
oversized
is an
attribute
of
an object
and
the object
is an
immediate
instance of
a class
and
the class
is a
subclass
of
hotel unit
,
then there exist
a physical
,
a real number
,, ,
another real number
and
an unit of measure
such that
the physical
is an
immediate
instance of
the class
and
the unit of measure
is an
instance
of
UnitOfArea
and the
measure
of
the physical
is
the real number
the unit of measure
(s) and the
measure
of
the object
is
the other real number
the unit of measure
(s) and
the real number
is an
instance
of
area measure
and
the other real number
is an
instance
of
area measure
and
the other real number
is
greater
than
the real number
(=>
(
and
(
citizen
?AGENT ?POLITY)
(
subProposition
UniversalSuffrageLaw
(
RegionalLawFn
?POLITY)))
(
confersRight
(
forall
(?VOTINGAGE ?AGE ?ELECTION)
(=>
(
and
(
citizen
?AGENT ?POLITY)
(
suffrageAgeMinimum
?POLITY
(
MeasureFn
?VOTINGAGE
YearDuration
))
(
age
?AGENT
(
MeasureFn
?AGE
YearDuration
))
(
greaterThanOrEqualTo
?AGE ?VOTINGAGE)
(
instance
?ELECTION
(
ElectionFn
?POLITY)))
(
exists
(?VOTING)
(
and
(
instance
?VOTING
(
VotingFn
?ELECTION))
(
agent
?VOTING ?AGENT)))))
(
RegionalLawFn
?POLITY) ?AGENT))
Government.kif 1117-1137
If
a human
is a
citizen
of
a nation
and
universal suffrage law
is a
sub
-proposition of the
regional
law of
the nation
,
then the
regional
law of
the nation
allow
s
the human
to perform task of the type for all
an entity
,
another entity
and
a third entity
if
the human
is a
citizen
of
the nation
and
the entity
year duration
(s) is a
suffrage
age minimum of
the nation
and the
age
of
the human
is
the other entity
year duration
(s) and
the other entity
is
greater
than or equal to
the entity
and
the third entity
is an
instance
of the
election
of
the nation
,
then there exists
a fourth entity
such that
the fourth entity
is an
instance
of the
voting
of
the third entity
and
the human
is an
agent
of
the fourth entity
(=>
(
and
(
comparativeArea
?REGION1 ?RELATION ?FACTOR ?REGION2)
(
instance
?UNIT
UnitOfArea
)
(
measure
?REGION1
(
MeasureFn
?NUM1 ?UNIT))
(
measure
?REGION2
(
MeasureFn
?NUM2 ?UNIT)))
(?RELATION
(
MeasureFn
?NUM1 ?UNIT)
(
MeasureFn
(
MultiplicationFn
?FACTOR ?NUM2) ?UNIT)))
Geography.kif 666-676
If
a geographic area
comparative
area
a BinaryRelationExtendedToQuantities
for
a positive real number
with
another geographic area
and
an unit of measure
is an
instance
of
UnitOfArea
and the
measure
of
the geographic area
is
a real number
the unit of measure
(s) and the
measure
of
the other geographic area
is
another real number
the unit of measure
(s),
then
the BinaryRelationExtendedToQuantities
the real number
the unit of measure
(s) and
the positive real number
and
the other real number
the unit of measure
(s)
Display limited to 25 items.
Show next 25
Display limited to 25 items.
Show next 25
statement
(
boilingPoint
Actinium
(
MeasureFn
3470.0
KelvinDegree
))
Mid-level-ontology.kif 28728-28728
3470.0
Kelvin degree
(s) is a
boiling
point of
actinium
(
boilingPoint
Aluminum
(
MeasureFn
2740.0
KelvinDegree
))
Mid-level-ontology.kif 28576-28576
2740.0
Kelvin degree
(s) is a
boiling
point of
aluminum
(
boilingPoint
Americium
(
MeasureFn
2880.0
KelvinDegree
))
Mid-level-ontology.kif 28740-28740
2880.0
Kelvin degree
(s) is a
boiling
point of
americium
(
boilingPoint
Antimony
(
MeasureFn
2023.0
KelvinDegree
))
Mid-level-ontology.kif 28652-28652
2023.0
Kelvin degree
(s) is a
boiling
point of
antimony
(
boilingPoint
Argon
(
MeasureFn
87.29
KelvinDegree
))
Mid-level-ontology.kif 28586-28586
87.29
Kelvin degree
(s) is a
boiling
point of
argon
(
boilingPoint
Arsenic
(
MeasureFn
886.0
KelvinDegree
))
Mid-level-ontology.kif 28616-28616
886.0
Kelvin degree
(s) is a
boiling
point of
arsenic
(
boilingPoint
Astatine
(
MeasureFn
610.0
KelvinDegree
))
Mid-level-ontology.kif 28720-28720
610.0
Kelvin degree
(s) is a
boiling
point of
astatine
(
boilingPoint
Barium
(
MeasureFn
1913.0
KelvinDegree
))
Mid-level-ontology.kif 28662-28662
1913.0
Kelvin degree
(s) is a
boiling
point of
barium
(
boilingPoint
Beryllium
(
MeasureFn
3243.0
KelvinDegree
))
Mid-level-ontology.kif 28558-28558
3243.0
Kelvin degree
(s) is a
boiling
point of
beryllium
(
boilingPoint
Bismuth
(
MeasureFn
1833.0
KelvinDegree
))
Mid-level-ontology.kif 28716-28716
1833.0
Kelvin degree
(s) is a
boiling
point of
bismuth
(
boilingPoint
Boron
(
MeasureFn
2823.0
KelvinDegree
))
Mid-level-ontology.kif 28560-28560
2823.0
Kelvin degree
(s) is a
boiling
point of
boron
(
boilingPoint
Bromine
(
MeasureFn
331.93
KelvinDegree
))
Mid-level-ontology.kif 28620-28620
331.93
Kelvin degree
(s) is a
boiling
point of
bromine
(
boilingPoint
Cadmium
(
MeasureFn
1038.0
KelvinDegree
))
Mid-level-ontology.kif 28646-28646
1038.0
Kelvin degree
(s) is a
boiling
point of
cadmium
(
boilingPoint
Caesium
(
MeasureFn
963.0
KelvinDegree
))
Mid-level-ontology.kif 28660-28660
963.0
Kelvin degree
(s) is a
boiling
point of
caesium
(
boilingPoint
Calcium
(
MeasureFn
1760.0
KelvinDegree
))
Mid-level-ontology.kif 28590-28590
1760.0
Kelvin degree
(s) is a
boiling
point of
calcium
(
boilingPoint
Carbon
(
MeasureFn
5100.0
KelvinDegree
))
Mid-level-ontology.kif 28562-28562
5100.0
Kelvin degree
(s) is a
boiling
point of
carbon
(
boilingPoint
Cerium
(
MeasureFn
3530.0
KelvinDegree
))
Mid-level-ontology.kif 28666-28666
3530.0
Kelvin degree
(s) is a
boiling
point of
cerium
(
boilingPoint
Chlorine
(
MeasureFn
238.55
KelvinDegree
))
Mid-level-ontology.kif 28584-28584
238.55
Kelvin degree
(s) is a
boiling
point of
chlorine
(
boilingPoint
Chromium
(
MeasureFn
2755.0
KelvinDegree
))
Mid-level-ontology.kif 28598-28598
2755.0
Kelvin degree
(s) is a
boiling
point of
chromium
(
boilingPoint
Cobalt
(
MeasureFn
3143.0
KelvinDegree
))
Mid-level-ontology.kif 28604-28604
3143.0
Kelvin degree
(s) is a
boiling
point of
cobalt
(
boilingPoint
Copper
(
MeasureFn
2868.0
KelvinDegree
))
Mid-level-ontology.kif 28608-28608
2868.0
Kelvin degree
(s) is a
boiling
point of
copper
(
boilingPoint
Dysprosium
(
MeasureFn
2608.0
KelvinDegree
))
Mid-level-ontology.kif 28682-28682
2608.0
Kelvin degree
(s) is a
boiling
point of
dysprosium
(
boilingPoint
Erbium
(
MeasureFn
2783.0
KelvinDegree
))
Mid-level-ontology.kif 28686-28686
2783.0
Kelvin degree
(s) is a
boiling
point of
erbium
(
boilingPoint
Europium
(
MeasureFn
1870.0
KelvinDegree
))
Mid-level-ontology.kif 28676-28676
1870.0
Kelvin degree
(s) is a
boiling
point of
europium
(
boilingPoint
Fluorine
(
MeasureFn
85.01
KelvinDegree
))
Mid-level-ontology.kif 28568-28568
85.01
Kelvin degree
(s) is a
boiling
point of
fluorine
Display limited to 25 items.
Show next 25
Display limited to 25 items.
Show next 25
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 3.0 is
open source software
produced by
Articulate Software
and its partners