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
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 302-302
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 22310-22310
No TPTP formula. May not be expressible in strict first order.
domainEnglishFormat.kif 22309-22309
antecedent
No TPTP formula. May not be expressible in strict first order.
Merge.kif 4678-4689
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.0 and
the real number
)
No TPTP formula. May not be expressible in strict first order.
FinancialOntology.kif 2329-2334
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.
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
No TPTP formula. May not be expressible in strict first order.
People.kif 108-121
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
another real 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 other real number
is
equal
to
the real number
No TPTP formula. May not be expressible in strict first order.
People.kif 142-155
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
another real 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 other real number
is
equal
to
the real number
No TPTP formula. May not be expressible in strict first order.
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
No TPTP formula. May not be expressible in strict first order.
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
No TPTP formula. May not be expressible in strict first order.
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
No TPTP formula. May not be expressible in strict first order.
People.kif 225-242
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 178-206
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
another real number
) is
equal
to 1 and the
population
of
the geopolitical area
is
equal
to
a third real number
holds
during
the
year
the integer
and
the third real number
and 1000 is
equal
to
a fourth real 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 fifth real number
and
the fifth real number
and
the fourth real number
is
equal
to
the real number
No TPTP formula. May not be expressible in strict first order.
People.kif 78-90
The
population
growth of
a geopolitical area
and the
year
an integer
is
equal
to
a real number
if and only if there exist
a kind of year
and
another kind of year
such that (
the integer
and
another integer
) is
equal
to 1 and
a kind of year
is
equal
to the
year
the integer
and
another kind of year
is
equal
to the
year
the other integer
and the
population
of
the geopolitical area
is
equal
to
another real number
holds
during
the kind of year
and the
population
of
the geopolitical area
is
equal
to
a third real number
holds
during
the other kind of year
and
the other real number
and
the third real number
is
equal
to
a fourth real number
and (
the fourth real number
and 1) is
equal
to
the real number
No TPTP formula. May not be expressible in strict first order.
Weather.kif 1507-1512
A real number
is
equal
to The
StandardDeviationFn
of
a list
if and only if
the real number
is
equal
to the
squareRoot
of The
VarianceFn
the list
No TPTP formula. May not be expressible in strict first order.
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)
No TPTP formula. May not be expressible in strict first order.
FinancialOntology.kif 3041-3049
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 13549-13559
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 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
No TPTP formula. May not be expressible in strict first order.
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
No TPTP formula. May not be expressible in strict first order.
ComputingBrands.kif 2661-2672
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
No TPTP formula. May not be expressible in strict first order.
ComputingBrands.kif 2633-2644
If
convex
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
inside
to
the self connected object
No TPTP formula. May not be expressible in strict first order.
Merge.kif 7996-8004
If the
beginning
of
a time interval
happens
before
the
beginning
of
another time interval
and the
end
of
the time interval
is
equal
to the
end
of
the other time interval
,
then
the other time interval
finish
es
the time interval
No TPTP formula. May not be expressible in strict first order.
Media.kif 2877-2883
If
a symbolic string
in
ISO-4217-A
denotes
an UnitOfCurrency
and
another symbolic string
in
ISO-3166-1-alpha-2
denotes
a class
and
the class
is a
subclass
of
geopolitical area
and
the other symbolic string
is
equal
to the
sub
-string of
the symbolic string
from 0 to 2,
then
the UnitOfCurrency
is a
currency
type of
the class
No TPTP formula. May not be expressible in strict first order.
UXExperimentalTerms.kif 682-689
If
a real number
is the
confidence
in
an experimenting
and
the experimenting
is an
instance
of
experimenting
and
a sentence
is an
instance
of
formula
and
the sentence
is a
patient
of
the experimenting
and
the real number
is
equal
to 100,
then
the sentence
is
false
No TPTP formula. May not be expressible in strict first order.
UXExperimentalTerms.kif 673-680
If
a real number
is the
confidence
in
an experimenting
and
the experimenting
is an
instance
of
experimenting
and
a sentence
is an
instance
of
formula
and
the sentence
is a
patient
of
the experimenting
and
the real number
is
equal
to 100,
then
the sentence
is
true
No TPTP formula. May not be expressible in strict first order.
FinancialOntology.kif 782-787
If
a financial account
current
account balance
a day
for
a real number
united states dollar
(s) and
the real number
is
less
than 0 and
another real number
is
equal
to (0 and
the real number
),
then
the financial account
is
overdraft
the other real number
united states dollar
(s) for
the day
No TPTP formula. May not be expressible in strict first order.
Merge.kif 2569-2574
If
a formula
decrease
s likelihood of
another formula
and the
probability
of
the other formula
is
equal
to
a real number
and
probability
of
the formula
provided that
the other formula
holds is
another real number
,
then
the other real number
is
less
than
the real number
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 4678-4689
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.0 and
the real number
)
No TPTP formula. May not be expressible in strict first order.
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
No TPTP formula. May not be expressible in strict first order.
Mid-level-ontology.kif 716-727
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 289-310
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
another real number
,
the other real number
MINUSONE,, ,
another positive integer
and
a third positive integer
such that
the other real number
is
greater
than 1 and
the other real 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 other real number
and
the other positive integer
is a
member
of
the list
and
the other real 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 other real number
MINUSONE is
equal
to (
the other real number
and 1) and
the other real 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 1538-1549
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
a physical
is
located
at
the geographic area
and
the physical
is a
member
of
the belief group
and
the physical
is a
member
of
the collection
and
the real number
1 is a
member
count of
the collection
and
the physical
2 is
located
at
the geographic area
and
the physical
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 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
No TPTP formula. May not be expressible in strict first order.
People.kif 108-121
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
another real 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 other real number
is
equal
to
the real number
No TPTP formula. May not be expressible in strict first order.
People.kif 142-155
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
another real 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 other real number
is
equal
to
the real number
No TPTP formula. May not be expressible in strict first order.
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
No TPTP formula. May not be expressible in strict first order.
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
No TPTP formula. May not be expressible in strict first order.
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
No TPTP formula. May not be expressible in strict first order.
People.kif 225-242
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 178-206
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
another real number
) is
equal
to 1 and the
population
of
the geopolitical area
is
equal
to
a third real number
holds
during
the
year
the integer
and
the third real number
and 1000 is
equal
to
a fourth real 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 fifth real number
and
the fifth real number
and
the fourth real number
is
equal
to
the real number
No TPTP formula. May not be expressible in strict first order.
People.kif 78-90
The
population
growth of
a geopolitical area
and the
year
an integer
is
equal
to
a real number
if and only if there exist
a kind of year
and
another kind of year
such that (
the integer
and
another integer
) is
equal
to 1 and
a kind of year
is
equal
to the
year
the integer
and
another kind of year
is
equal
to the
year
the other integer
and the
population
of
the geopolitical area
is
equal
to
another real number
holds
during
the kind of year
and the
population
of
the geopolitical area
is
equal
to
a third real number
holds
during
the other kind of year
and
the other real number
and
the third real number
is
equal
to
a fourth real number
and (
the fourth real number
and 1) is
equal
to
the real number
No TPTP formula. May not be expressible in strict first order.
Weather.kif 1507-1512
A real number
is
equal
to The
StandardDeviationFn
of
a list
if and only if
the real number
is
equal
to the
squareRoot
of The
VarianceFn
the list
No TPTP formula. May not be expressible in strict first order.
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)
No TPTP formula. May not be expressible in strict first order.
People.kif 1557-1568
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
a physical
is
located
at
the geographic area
and
the physical
is a
member
of
the ethnic group
and
the physical
is a
member
of
the collection
and
the real number
1 is a
member
count of
the collection
and
the physical
2 is
located
at
the geographic area
and
the physical
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 1831-1835
A real number
is
greater
than or equal to
another real number
if and only if
the real number
is
equal
to
the other real number
or
the real number
is
greater
than
the other real number
No TPTP formula. May not be expressible in strict first order.
Mid-level-ontology.kif 29625-29638
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
No TPTP formula. May not be expressible in strict first order.
Geography.kif 3426-3435
An entity
is an
instance
of
continent
if and only if
africa
is
equal
to
the entity
or
north america
is
equal
to
the entity
or
south america
is
equal
to
the entity
or
antarctica
is
equal
to
the entity
or
europe
is
equal
to
the entity
or
asia
is
equal
to
the entity
or
oceania
is
equal
to
the entity
No TPTP formula. May not be expressible in strict first order.
Mid-level-ontology.kif 6151-6161
An entity
is an
instance
of
conjugated substance
if and only if there exist
an object
,
another object
and
a process
such that
the object
is an
instance
of
compound substance
and
the other object
is an
instance
of
compound substance
and
the object
is not
equal
to
the other object
and
the process
is an
instance
of
chemical synthesis
and
the object
is a
resource
for
the process
and
the other object
is a
resource
for
the process
and
the entity
is a
result
of
the process
No TPTP formula. May not be expressible in strict first order.
Geography.kif 3410-3416
An entity
is an
instance
of
hemisphere
if and only if
the entity
is
equal
to
northern hemisphere
or
the entity
is
equal
to
southern hemisphere
or
the entity
is
equal
to
eastern hemisphere
or
the entity
is
equal
to
western hemisphere
No TPTP formula. May not be expressible in strict first order.
Merge.kif 9419-9424
An object
is an
instance
of
self connected object
if and only if for all
another object
and
a third object
if
the object
is
equal
to the
union
of the parts of
the other object
and
the third object
,
then
the other object
is
connected
to
the third object
No TPTP formula. May not be expressible in strict first order.
People.kif 1576-1587
A real number
percent of people in
a geographic area
speak
a language
if and only if there exist
a collection
and
another collection
such that
a sentient agent
is
located
at
the geographic area
and
the sentient agent
is a
member
of
the collection
and
the language
is a
speaks
language of
the sentient agent
and
the real number
1 is a
member
count of
the collection
and
the sentient agent
2 is
located
at
the geographic area
and
the sentient agent
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 1813-1817
A real number
is
less
than or equal to
another real number
if and only if
the real number
is
equal
to
the other real number
or
the real number
is
less
than
the other real number
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 933-946
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 12798-12801
For all
a real number
the real number
Ounce
(s) is
equal
to
the real number
and 16.0
pound mass
(s)
No TPTP formula. May not be expressible in strict first order.
Merge.kif 4646-4647
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 4630-4631
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 2971-2974
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 2976-2980
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 2907-2907
Big six
is not
equal
to
group of6
appearance as argument number 0
No TPTP formula. May not be expressible in strict first order.
Merge.kif 5171-5171
The
arccosine
of the
cosine
of
a real number
is
equal
to
the real number
No TPTP formula. May not be expressible in strict first order.
Merge.kif 5181-5181
The
arcsine
of the
sine
of
a real number
is
equal
to
the real number
No TPTP formula. May not be expressible in strict first order.
Merge.kif 5161-5161
The
arctan
of the
tangent
of
a real number
is
equal
to
the real number
No TPTP formula. May not be expressible in strict first order.
Military.kif 872-881
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.
Merge.kif 13935-13935
The number of
instances
in
continent
is
equal
to 7
No TPTP formula. May not be expressible in strict first order.
Media.kif 2001-2001
The number of
instances
in
NativityMagi
is
equal
to 3
No TPTP formula. May not be expressible in strict first order.
People.kif 469-479
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.
Military.kif 895-906
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.
Economy.kif 2019-2019
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 2020-2020
1
Kilowatt hour
(s) is
equal
to 3600000.0
joule
(s)
No TPTP formula. May not be expressible in strict first order.
Merge.kif 7022-7024
1
Week duration
(s) is
equal
to 7
day duration
(s)
No TPTP formula. May not be expressible in strict first order.
Merge.kif 7049-7051
1
Year duration
(s) is
equal
to 365
day duration
(s)
No TPTP formula. May not be expressible in strict first order.
Geography.kif 382-382
1.0
Angular degree
(s) is
equal
to 60.0
arc minute
(s)
No TPTP formula. May not be expressible in strict first order.
Geography.kif 401-401
1.0
Arc minute
(s) is
equal
to 60.0
arc second
(s)
No TPTP formula. May not be expressible in strict first order.
Geography.kif 3764-3764
1.0
Fathom
(s) is
equal
to 6.0
foot length
(s)
No TPTP formula. May not be expressible in strict first order.
Mid-level-ontology.kif 13071-13073
1.0
Metric ton
(s) is
equal
to 2205.0
pound mass
(s)
No TPTP formula. May not be expressible in strict first order.
Geography.kif 3787-3789
1.0
Nautical mile
(s) is
equal
to 1852.0
meter
(s)
No TPTP formula. May not be expressible in strict first order.
Geography.kif 3783-3785
1.0
Nautical mile
(s) is
equal
to 6076.1
foot length
(s)
No TPTP formula. May not be expressible in strict first order.
Mid-level-ontology.kif 13166-13170
1.0
Square mile
(s) is
equal
to the
per
of 1.0
mile
(s) and 1.0
mile
(s)
No TPTP formula. May not be expressible in strict first order.
Mid-level-ontology.kif 13176-13180
1.0
Square yard
(s) is
equal
to the
per
of 1.0
yard length
(s) and 1.0
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.0 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.0 and
the real number
arc minute
(s)
No TPTP formula. May not be expressible in strict first order.
Merge.kif 7061-7063
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 7083-7085
A real number
angstrom
(s) is
equal
to
the real number
and 1.0E-10
meter
(s)
No TPTP formula. May not be expressible in strict first order.
Merge.kif 7277-7279
A real number
angular degree
(s) is
equal
to
the real number
and
pi
and 180.0
radian
(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