Browsing Interface
: Welcome guest :
log in
[
Home
|
Graph
| ]
KB:
SUMO
Language:
ChineseLanguage
ChineseTraditionalLanguage
ChinesehLanguage
EnglishLanguage
FrenchLanguage
GermanLanguage
JapaneseLanguage
SpanishLanguage
SwedishLanguage
Formal Language:
OWL
SUO-KIF
TPTP
traditionalLogic
KB Term:
Term intersection
English Word:
Any
Noun
Verb
Adjective
Adverb
equal
Sigma KEE - equal
equal
appearance as argument number 1
No TPTP formula. May not be expressible in strict first order.
chinese_format.kif 1391-1392
appearance as argument number 2
No TPTP formula. May not be expressible in strict first order.
chinese_format.kif 297-297
No TPTP formula. May not be expressible in strict first order.
english_format.kif 305-305
No TPTP formula. May not be expressible in strict first order.
chinese_format.kif 298-298
No TPTP formula. May not be expressible in strict first order.
domainEnglishFormat.kif 22251-22251
No TPTP formula. May not be expressible in strict first order.
domainEnglishFormat.kif 22250-22250
antecedent
No TPTP formula. May not be expressible in strict first order.
Merge.kif 4585-4596
The
absolute
value
of
a real number
is
equal
to
a nonnegative real number
and
the real number
is an
instance
of
real number
and
the nonnegative real number
is an
instance
of
real number
if and only if
the real number
is an
instance
of
nonnegative real number
and
the real number
is
equal
to
the nonnegative real number
or
the real number
is an
instance
of
negative real number
and
the nonnegative real number
is
equal
to (0 and
the real number
)
No TPTP formula. May not be expressible in strict first order.
Merge.kif 2977-2993
A list
is
equal
to the
list
composed of
another list
and
a third list
and
the other list
is not
equal
to
null list
and
the third list
is not
equal
to
null list
if and only if for all
a positive integer
and
another positive integer
if
the positive integer
is
less
than or equal to
length
of
the other list
and
the other positive integer
is
less
than or equal to
length
of
the third list
and
the positive integer
is an
instance
of
positive integer
and
the other positive integer
is an
instance
of
positive integer
,
then
the positive integer
th
element
of
the list
is
equal
to
the positive integer
th
element
of
the other list
and (
length
of
the other list
and
the other positive integer
)th
element
of
the list
is
equal
to
the other positive integer
th
element
of
the third list
No TPTP formula. May not be expressible in strict first order.
FinancialOntology.kif 2251-2256
A financial account
is an
instance
of
financial account
and
a cognitive agent
possess
es
a financial asset
and
the financial account
is
equal
to the
account
of
the financial asset
if and only if
the cognitive agent
holds
account
the financial account
No TPTP formula. May not be expressible in strict first order.
Geography.kif 3761-3765
An unit of measure
is an
instance
of
unit of measure
and
a number
is
equal
to 1 the
square
unit of
the unit of measure
(s) if and only if
the number
is
equal
to 1
the unit of measure
(s) and 1
the unit of measure
(s)
No TPTP formula. May not be expressible in strict first order.
People.kif 104-117
The
births
per thousand of
a geopolitical area
and the
year
an integer
is
equal
to
a real number
if and only if the
population
of
the geopolitical area
and 1000 is
equal
to
a number
and
another integer
is
equal
to the number of
instances
in the
class
described by
a symbolic string
and
the other integer
and
the number
is
equal
to
the real number
No TPTP formula. May not be expressible in strict first order.
People.kif 138-151
The
deaths
per thousand of
a geopolitical area
and the
year
an integer
is
equal
to
a real number
if and only if the
population
of
the geopolitical area
and 1000 is
equal
to
a number
and
another integer
is
equal
to the number of
instances
in the
class
described by
a symbolic string
and
the other integer
and
the number
is
equal
to
the real number
No TPTP formula. May not be expressible in strict first order.
People.kif 253-277
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
a 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 number
is
equal
to
the real number
No TPTP formula. May not be expressible in strict first order.
People.kif 411-442
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
No TPTP formula. May not be expressible in strict first order.
Merge.kif 3105-3110
The
last
of
a list
is
equal
to
an entity
if and only if there exists
a positive integer
such that
length
of
the list
is
equal
to
the positive integer
and
the positive integer
th
element
of
the list
is
equal
to
the entity
No TPTP formula. May not be expressible in strict first order.
People.kif 323-353
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
No TPTP formula. May not be expressible in strict first order.
People.kif 367-398
The
male
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
No TPTP formula. May not be expressible in strict first order.
People.kif 221-238
The
male
to female ratio of
a geopolitical area
is
equal
to
a real number
if and only if
an integer
is
equal
to the number of
instances
in the
class
described by
a symbolic string
and
another integer
is
equal
to the number of
instances
in the
class
described by
another symbolic string
and
the integer
and
the other integer
is
equal
to
the real number
No TPTP formula. May not be expressible in strict first order.
People.kif 174-202
The
migrants
per thousand of
a geopolitical area
and the
year
an integer
is
equal
to
a real number
if and only if (
the integer
and
a number
) is
equal
to 1 and the
population
of
the geopolitical area
is
equal
to
another number
holds
during
the
year
the integer
and
the other number
and 1000 is
equal
to
a third number
and
another integer
is
equal
to the number of
instances
in the
class
described by
a symbolic string
and
a third integer
is
equal
to the number of
instances
in the
class
described by
the symbolic string
and (
the other integer
and
the third integer
) is
equal
to
a fourth number
and
the fourth number
and
the third number
is
equal
to
the real number
No TPTP formula. May not be expressible in strict first order.
People.kif 77-86
The
population
growth of
a geopolitical area
and the
year
an integer
is
equal
to
a real number
if and only if (
the integer
and
another integer
) is
equal
to 1 and the
population
of
the geopolitical area
is
equal
to
a number
holds
during
the
year
the integer
and the
population
of
the geopolitical area
is
equal
to
another number
holds
during
the
year
the other integer
and
the number
and
the other number
is
equal
to
a third number
and (
the third number
and 1) is
equal
to
the real number
No TPTP formula. May not be expressible in strict first order.
Merge.kif 4898-4900
An integer
mod
another integer
is
equal
to
a third integer
if and only if (the
largest
integer less than or equal to
the integer
and
the other integer
and
the other integer
and
the third integer
) is
equal
to
the integer
No TPTP formula. May not be expressible in strict first order.
Merge.kif 7414-7416
Value
of belongings of
an agent
is
equal
to
a currency measure
if and only if
value
of
belongings
of
the agent
is
the currency measure
No TPTP formula. May not be expressible in strict first order.
Merge.kif 4084-4086
The place
where
a physical
was at
a time point
is
equal
to
a region
if and only if
the physical
is
exactly
located in
the region
holds
during
the time point
No TPTP formula. May not be expressible in strict first order.
Weather.kif 1113-1118
No TPTP formula. May not be expressible in strict first order.
FinancialOntology.kif 3229-3236
There exist
a number
,
a chargingA fee
and
the chargingA fee
Amount such that
a human
is
income
earned
the number
for
an organizational process
and
the chargingA fee
Amount is the
amount
charged
in
the chargingA fee
and
the organizational process
cause
s
the chargingA fee
and
a third number
is
equal
to (
the number
and
the chargingA fee
Amount) if and only if the
after
tax
income
derived by
the human
from
the organizational process
is
the third number
No TPTP formula. May not be expressible in strict first order.
FinancialOntology.kif 2949-2957
There exist
a financial instrument
,
the financial instrument
Price and
another currency measure
such that
an agreement
is an
instance
of
option
and
the financial instrument
is an
underlier
of
the agreement
and
the financial instrument
is
price
the financial instrument
Price for
an agent
and
the other currency measure
is a
strike
price of
the agreement
and
the financial instrument
Price is
equal
to
the other currency measure
if and only if
the agent
is an
at
the money of
the agreement
No TPTP formula. May not be expressible in strict first order.
Mid-level-ontology.kif 11715-11725
If
a cognitive agent
has the responsibility to make
a proposition
a deontic attribute
in
an agreement
and
the deontic attribute
is
equal
to
obligation
or
the deontic attribute
is
equal
to
promise
,
then the statement there exists
an entity
such that
the entity
express
es the content of
the proposition
and
the cognitive agent
is an
agent
of
the entity
has the
modal
force
of
likely
No TPTP formula. May not be expressible in strict first order.
Geography.kif 2040-2047
If
a number
is an
arable
land area of
a geographic area
and
the number
is
greater
than or equal to 0 and
a real number
an unit of measure
(s) is a
total
area of
the geographic area
and
the unit of measure
is an
instance
of
UnitOfArea
and
a constant quantity
is
equal
to
the number
and
the real number
the unit of measure
(s),
then
the constant quantity
is an
arable
land area of
the geographic area
No TPTP formula. May not be expressible in strict first order.
Geography.kif 2031-2038
If
a number
is an
arable
land area of
a geographic area
and
the number
is
greater
than or equal to 0 and
another number
is a
total
area of
the geographic area
and
the other number
is an
instance
of
area measure
and
a third number
is
equal
to
the number
and
the other number
,
then
the third number
is an
arable
land area of
the geographic area
No TPTP formula. May not be expressible in strict first order.
ArabicCulture.kif 193-210
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
and
another entity
such that
the entity
is an
instance
of
zakat
and
a third entity
is an
instance
of
year
and
the third entity
takes place
during
the
time
of existence of
the agent
and
fully formed
is an
attribute
of
the agent
holds
during
the third 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 fourth entity
and
the fourth entity
is
greater
than
the currency measure
and 0.025 has the
modal
force
of
obligation
No TPTP formula. May not be expressible in strict first order.
ComputingBrands.kif 2664-2675
If
concave
is an
attribute
of
a self connected object
and
the self connected object
is a
surface
of
another self connected object
and
an object
is a
part
of
the other self connected object
and
another object
is a
part
of
the other self connected object
and
a third object
is
equal
to the line between
the object
and
the other object
and
the object
is not
equal
to
the other object
and
a fourth object
is a
part
of
the third object
,
then
the fourth object
is
outside
to
the self connected object
Display limited to 25 items.
Show next 25
Display limited to 25 items.
Show next 25
consequent
No TPTP formula. May not be expressible in strict first order.
Merge.kif 4585-4596
The
absolute
value
of
a real number
is
equal
to
a nonnegative real number
and
the real number
is an
instance
of
real number
and
the nonnegative real number
is an
instance
of
real number
if and only if
the real number
is an
instance
of
nonnegative real number
and
the real number
is
equal
to
the nonnegative real number
or
the real number
is an
instance
of
negative real number
and
the nonnegative real number
is
equal
to (0 and
the real number
)
No TPTP formula. May not be expressible in strict first order.
Merge.kif 2977-2993
A list
is
equal
to the
list
composed of
another list
and
a third list
and
the other list
is not
equal
to
null list
and
the third list
is not
equal
to
null list
if and only if for all
a positive integer
and
another positive integer
if
the positive integer
is
less
than or equal to
length
of
the other list
and
the other positive integer
is
less
than or equal to
length
of
the third list
and
the positive integer
is an
instance
of
positive integer
and
the other positive integer
is an
instance
of
positive integer
,
then
the positive integer
th
element
of
the list
is
equal
to
the positive integer
th
element
of
the other list
and (
length
of
the other list
and
the other positive integer
)th
element
of
the list
is
equal
to
the other positive integer
th
element
of
the third list
No TPTP formula. May not be expressible in strict first order.
Merge.kif 2116-2133
A relation
is an
instance
of
total valued relation
and
the relation
is an
instance
of
predicate
if and only if there exists
a positive integer
such that
the relation
is an
instance
of
relation
and
the relation
%&has
the positive integer
argument
(s) and
if for all
another positive integer
,
an entity
and
a set or class
if
the other positive integer
is
less
than
the positive integer
and the number
the other positive integer
argument of
the relation
is an
instance
of
the set or class
and
the entity
is
equal
to
the other positive integer
th
element
of (@ROW),
then
the entity
is an
instance
of
the set or class
,
then there exists
a fourth entity
such that
the relation
@ROW and
the fourth entity
No TPTP formula. May not be expressible in strict first order.
Geography.kif 3761-3765
An unit of measure
is an
instance
of
unit of measure
and
a number
is
equal
to 1 the
square
unit of
the unit of measure
(s) if and only if
the number
is
equal
to 1
the unit of measure
(s) and 1
the unit of measure
(s)
No TPTP formula. May not be expressible in strict first order.
Mid-level-ontology.kif 926-937
Polyphonic music
is an
attribute
of
an object
if and only if there exist
a process
and
another process
such that
the object
is an
instance
of
making music
and
the process
is an
instance
of
making music
and
the other process
is an
instance
of
making music
and
the process
is a
subprocess
of
the object
and
the other process
is a
subprocess
of
the object
and
the process
is not
equal
to
the other process
and
the process
occur
s at the same time as
the object
and
the other process
occur
s at the same time as
the object
No TPTP formula. May not be expressible in strict first order.
People.kif 285-306
A real number
is an
average
of
a list
if and only if there exists
another list
such that
length
of
the other list
is
equal
to
length
of
the list
and 1th
element
of
the other list
is
equal
to 1th
element
of
the list
and for all
a positive integer
if
the positive integer
is a
member
of
the other list
,
then there exist
a number
,
the number
MINUSONE,, ,
another positive integer
and
a third positive integer
such that
the number
is
greater
than 1 and
the number
is
less
than or equal to
length
of
the other list
and
the positive integer
th
element
of
the other list
is
equal
to
the number
and
the other positive integer
is a
member
of
the list
and
the number
is
equal
to
the other positive integer
th
element
of
the list
and
the third positive integer
is a
member
of
the other list
and
the number
MINUSONE is
equal
to (
the number
and 1) and
the number
MINUSONE is
equal
to
the third positive integer
th
element
of
the other list
and
the positive integer
is
equal
to (
the other positive integer
and
the third positive integer
)
and
a fourth positive integer
is
equal
to
length
of
the other list
and
the real number
is
equal
to
the fourth positive integer
th
element
of
the other list
and
the fourth positive integer
No TPTP formula. May not be expressible in strict first order.
People.kif 1530-1541
A real number
percent of people in
a geographic area
believe
in
a belief group
if and only if there exist
a collection
and
another collection
such that
an object
is
located
at
the geographic area
and
the object
is a
member
of
the belief group
and
the object
is a
member
of
the collection
and
the real number
1 is a
member
count of
the collection
and
the object
2 is
located
at
the geographic area
and
the object
2 is a
member
of
the other collection
and
the real number
2 is a
member
count of
the other collection
and
the real number
and 100 is
equal
to
the real number
1 and
the real number
2
No TPTP formula. May not be expressible in strict first order.
Cars.kif 1918-1923
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
No TPTP formula. May not be expressible in strict first order.
Merge.kif 7875-7877
A physical
occur
s at the same time as
another physical
if and only if the
time
of existence of
the physical
is
equal
to the
time
of existence of
the other physical
No TPTP formula. May not be expressible in strict first order.
People.kif 104-117
The
births
per thousand of
a geopolitical area
and the
year
an integer
is
equal
to
a real number
if and only if the
population
of
the geopolitical area
and 1000 is
equal
to
a number
and
another integer
is
equal
to the number of
instances
in the
class
described by
a symbolic string
and
the other integer
and
the number
is
equal
to
the real number
No TPTP formula. May not be expressible in strict first order.
People.kif 138-151
The
deaths
per thousand of
a geopolitical area
and the
year
an integer
is
equal
to
a real number
if and only if the
population
of
the geopolitical area
and 1000 is
equal
to
a number
and
another integer
is
equal
to the number of
instances
in the
class
described by
a symbolic string
and
the other integer
and
the number
is
equal
to
the real number
No TPTP formula. May not be expressible in strict first order.
People.kif 253-277
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
a 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 number
is
equal
to
the real number
No TPTP formula. May not be expressible in strict first order.
People.kif 411-442
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
No TPTP formula. May not be expressible in strict first order.
Merge.kif 3105-3110
The
last
of
a list
is
equal
to
an entity
if and only if there exists
a positive integer
such that
length
of
the list
is
equal
to
the positive integer
and
the positive integer
th
element
of
the list
is
equal
to
the entity
No TPTP formula. May not be expressible in strict first order.
People.kif 323-353
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
No TPTP formula. May not be expressible in strict first order.
People.kif 367-398
The
male
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
No TPTP formula. May not be expressible in strict first order.
People.kif 221-238
The
male
to female ratio of
a geopolitical area
is
equal
to
a real number
if and only if
an integer
is
equal
to the number of
instances
in the
class
described by
a symbolic string
and
another integer
is
equal
to the number of
instances
in the
class
described by
another symbolic string
and
the integer
and
the other integer
is
equal
to
the real number
No TPTP formula. May not be expressible in strict first order.
People.kif 174-202
The
migrants
per thousand of
a geopolitical area
and the
year
an integer
is
equal
to
a real number
if and only if (
the integer
and
a number
) is
equal
to 1 and the
population
of
the geopolitical area
is
equal
to
another number
holds
during
the
year
the integer
and
the other number
and 1000 is
equal
to
a third number
and
another integer
is
equal
to the number of
instances
in the
class
described by
a symbolic string
and
a third integer
is
equal
to the number of
instances
in the
class
described by
the symbolic string
and (
the other integer
and
the third integer
) is
equal
to
a fourth number
and
the fourth number
and
the third number
is
equal
to
the real number
No TPTP formula. May not be expressible in strict first order.
People.kif 77-86
The
population
growth of
a geopolitical area
and the
year
an integer
is
equal
to
a real number
if and only if (
the integer
and
another integer
) is
equal
to 1 and the
population
of
the geopolitical area
is
equal
to
a number
holds
during
the
year
the integer
and the
population
of
the geopolitical area
is
equal
to
another number
holds
during
the
year
the other integer
and
the number
and
the other number
is
equal
to
a third number
and (
the third number
and 1) is
equal
to
the real number
No TPTP formula. May not be expressible in strict first order.
Merge.kif 4898-4900
An integer
mod
another integer
is
equal
to
a third integer
if and only if (the
largest
integer less than or equal to
the integer
and
the other integer
and
the other integer
and
the third integer
) is
equal
to
the integer
No TPTP formula. May not be expressible in strict first order.
Weather.kif 1113-1118
No TPTP formula. May not be expressible in strict first order.
People.kif 1549-1560
A real number
percent
of people in
a geographic area
are
an ethnic group
if and only if there exist
a collection
and
another collection
such that
an object
is
located
at
the geographic area
and
the object
is a
member
of
the ethnic group
and
the object
is a
member
of
the collection
and
the real number
1 is a
member
count of
the collection
and
the object
2 is
located
at
the geographic area
and
the object
2 is a
member
of
the other collection
and
the real number
2 is a
member
count of
the other collection
and
the real number
and 100 is
equal
to
the real number
1 and
the real number
2
No TPTP formula. May not be expressible in strict first order.
Merge.kif 7665-7673
A time interval
finish
es
another time interval
if and only if the
beginning
of
the other time interval
happens
before
the
beginning
of
the time interval
and the
end
of
the other time interval
is
equal
to the
end
of
the time interval
No TPTP formula. May not be expressible in strict first order.
Merge.kif 1798-1802
A quantity
is
greater
than or equal to
another quantity
if and only if
the quantity
is
equal
to
the other quantity
or
the quantity
is
greater
than
the other quantity
No TPTP formula. May not be expressible in strict first order.
Mid-level-ontology.kif 28413-28426
Alone
is an
attribute
of
an entity
holds
during
a time interval
if and only if there don't exist
the entity
2 and
a process
such that
the entity
is not
equal
to
the entity
2 and
the entity
2 is an
instance
of
agent
and
the process
is an
instance
of
social interaction
and the
time
of existence of
the process
takes place
during
the time interval
and
the entity
is an
involved
in event of
the process
and
the entity
2 is an
involved
in event of
the process
Display limited to 25 items.
Show next 25
Display limited to 25 items.
Show next 25
statement
No TPTP formula. May not be expressible in strict first order.
Military.kif 928-941
The
reaching
military age annually male of
a geopolitical area
and
a year
is
equal
to the number of
instances
in the
class
described by
a symbolic string
No TPTP formula. May not be expressible in strict first order.
Mid-level-ontology.kif 10979-10982
For all
a real number
the real number
Ounce
(s) is
equal
to
the real number
and 16
pound mass
(s)
No TPTP formula. May not be expressible in strict first order.
Merge.kif 4553-4554
For all
an integer
(
the integer
+2) is
equal
to (
the integer
and 1)
No TPTP formula. May not be expressible in strict first order.
Merge.kif 4537-4538
For all
an integer
(
the integer
+1) is
equal
to (
the integer
and 1)
No TPTP formula. May not be expressible in strict first order.
Merge.kif 2931-2934
For all @ROW and
another entity
length
of (@ROW and
the other entity
) is
equal
to (
length
of (@ROW)+1)
No TPTP formula. May not be expressible in strict first order.
Merge.kif 2936-2940
For all @ROW and
another entity
length
of (@ROW and
the other entity
)th
element
of (@ROW and
the other entity
) is
equal
to
the other entity
No TPTP formula. May not be expressible in strict first order.
Government.kif 2846-2846
Big six
is not
equal
to
group of6
appearance as argument number 0
No TPTP formula. May not be expressible in strict first order.
Military.kif 867-876
The
available
for military service male of
a geopolitical area
is
equal
to the number of
instances
in the
class
described by
a symbolic string
No TPTP formula. May not be expressible in strict first order.
Mid-level-ontology.kif 7572-7572
The
beginning
of
before common era
is
equal
to
negative infinity
No TPTP formula. May not be expressible in strict first order.
Merge.kif 13181-13181
The number of
instances
in
continent
is
equal
to 7
No TPTP formula. May not be expressible in strict first order.
Media.kif 2005-2005
The number of
instances
in
NativityMagi
is
equal
to 3
No TPTP formula. May not be expressible in strict first order.
People.kif 462-472
The
children
born per woman of
a geopolitical area
and the
year
an integer
is
equal
to the number of
instances
in the
class
described by
a symbolic string
No TPTP formula. May not be expressible in strict first order.
Mid-level-ontology.kif 7580-7580
The
end
of
common era
is
equal
to
positive infinity
No TPTP formula. May not be expressible in strict first order.
Military.kif 890-901
The
fit
for military service male of
a geopolitical area
is
equal
to the number of
instances
in the
class
described by
a symbolic string
No TPTP formula. May not be expressible in strict first order.
Merge.kif 7086-7086
0.0
Angular degree
(s) is
equal
to 360.0
angular degree
(s)
No TPTP formula. May not be expressible in strict first order.
Geography.kif 382-382
1
Angular degree
(s) is
equal
to 60
arc minute
(s)
No TPTP formula. May not be expressible in strict first order.
Geography.kif 401-401
1
Arc minute
(s) is
equal
to 60
arc second
(s)
No TPTP formula. May not be expressible in strict first order.
Mid-level-ontology.kif 11256-11262
1
Cubic foot
(s) is
equal
to 1
foot length
(s) and 1
foot length
(s) and 1
foot length
(s)
No TPTP formula. May not be expressible in strict first order.
Geography.kif 3677-3677
1
Fathom
(s) is
equal
to 6
foot length
(s)
No TPTP formula. May not be expressible in strict first order.
Economy.kif 2012-2012
1
Kilowatt hour
(s) is
equal
to 3.6 1
million
joule
s(s)
No TPTP formula. May not be expressible in strict first order.
Economy.kif 2013-2013
1
Kilowatt hour
(s) is
equal
to 3600000
joule
(s)
No TPTP formula. May not be expressible in strict first order.
Mid-level-ontology.kif 11228-11230
1
Metric ton
(s) is
equal
to 2205
pound mass
(s)
No TPTP formula. May not be expressible in strict first order.
Geography.kif 3697-3697
1
Nautical mile
(s) is
equal
to 1852
meter
(s)
No TPTP formula. May not be expressible in strict first order.
Geography.kif 3696-3696
1
Nautical mile
(s) is
equal
to 6076.1
foot length
(s)
No TPTP formula. May not be expressible in strict first order.
Geography.kif 624-625
1
Square kilometer
(s) is
equal
to 1 1
thousand
meter
s(s) and 1 1
thousand
meter
s(s)
No TPTP formula. May not be expressible in strict first order.
Geography.kif 3749-3750
1
Square meter
(s) is
equal
to 1
meter
(s) and 1
meter
(s)
No TPTP formula. May not be expressible in strict first order.
Mid-level-ontology.kif 11312-11316
1
Square mile
(s) is
equal
to the
per
of 1
mile
(s) and 1
mile
(s)
No TPTP formula. May not be expressible in strict first order.
Mid-level-ontology.kif 11322-11326
1
Square yard
(s) is
equal
to the
per
of 1
yard length
(s) and 1
yard length
(s)
No TPTP formula. May not be expressible in strict first order.
Geography.kif 402-402
A real number
arc minute
(s) is
equal
to 60 and
the real number
arc second
(s)
No TPTP formula. May not be expressible in strict first order.
Geography.kif 383-383
A real number
angular degree
(s) is
equal
to 60 and
the real number
arc minute
(s)
No TPTP formula. May not be expressible in strict first order.
Merge.kif 6860-6862
A real number
amu
(s) is
equal
to
the real number
and 1.6605402E-24
gram
(s)
No TPTP formula. May not be expressible in strict first order.
Merge.kif 6882-6884
A real number
angstrom
(s) is
equal
to
the real number
and 1.0E-10
meter
(s)
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
equal