Browsing Interface
: Welcome guest :
log in
[
Home
|
Graph
| ]
KB:
SUMO
Language:
ChineseLanguage
ChinesePinyinWriting
ChineseSimplifiedWriting
ChineseTraditionalLanguage
EnglishLanguage
FrenchLanguage
GermanLanguage
Hindi
ItalianLanguage
JapaneseLanguage
PortugueseLanguage
SpanishLanguage
SwedishLanguage
cb
cz
de
hi
ro
sv
tg
Formal Language:
OWL
SUO-KIF
TPTP
traditionalLogic
KB Term:
Term intersection
English Word:
Any
Noun
Verb
Adjective
Adverb
subclass
Sigma KEE - subclass
subclass
appearance as argument number 1
No TPTP formula. May not be expressible in strict first order.
chinese_format.kif 1371-1373
No TPTP formula. May not be expressible in strict first order.
Merge.kif 133-135
No TPTP formula. May not be expressible in strict first order.
japanese_format.kif 27-29
No TPTP formula. May not be expressible in strict first order.
spanish_format.kif 28-30
No TPTP formula. May not be expressible in strict first order.
Merge.kif 131-131
The number 1 argument of
subclass
is an
instance
of
class
No TPTP formula. May not be expressible in strict first order.
Merge.kif 132-132
The number 2 argument of
subclass
is an
instance
of
class
No TPTP formula. May not be expressible in strict first order.
Merge.kif 129-129
subclass
is an
instance
of
binary predicate
No TPTP formula. May not be expressible in strict first order.
Merge.kif 130-130
subclass
is an
instance
of
partial ordering relation
appearance as argument number 2
No TPTP formula. May not be expressible in strict first order.
chinese_format.kif 319-319
No TPTP formula. May not be expressible in strict first order.
english_format.kif 324-324
No TPTP formula. May not be expressible in strict first order.
french_format.kif 182-182
No TPTP formula. May not be expressible in strict first order.
relations-it.txt 271-271
No TPTP formula. May not be expressible in strict first order.
japanese_format.kif 2002-2002
No TPTP formula. May not be expressible in strict first order.
portuguese_format.kif 134-134
No TPTP formula. May not be expressible in strict first order.
relations-cz.txt 175-175
No TPTP formula. May not be expressible in strict first order.
relations-de.txt 419-419
No TPTP formula. May not be expressible in strict first order.
relations-hindi.txt 308-308
No TPTP formula. May not be expressible in strict first order.
relations-ro.kif 202-202
No TPTP formula. May not be expressible in strict first order.
relations-sv.txt 192-192
No TPTP formula. May not be expressible in strict first order.
relations-tg.txt 463-463
No TPTP formula. May not be expressible in strict first order.
Merge.kif 5377-5377
subset
is a
subrelation
of
subclass
No TPTP formula. May not be expressible in strict first order.
domainEnglishFormat.kif 55725-55725
No TPTP formula. May not be expressible in strict first order.
chinese_format.kif 320-320
No TPTP formula. May not be expressible in strict first order.
domainEnglishFormat.kif 55724-55724
No TPTP formula. May not be expressible in strict first order.
domainEnglishFormat.kif 55723-55723
antecedent
No TPTP formula. May not be expressible in strict first order.
Hotel.kif 1186-1201
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
unit of area
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
No TPTP formula. May not be expressible in strict first order.
Biography.kif 730-740
If
writer
is an
attribute
of
an agent
and
an entity
is an
instance
of
a kind of content bearing object
and
a kind of content bearing object
is a
subclass
of
text
or
the kind of content bearing object
is a
subclass
of
document
and
a process
is an
instance
of
writing
and
the agent
is an
agent
of
the process
and
the entity
is a
result
of
the process
,
then
the agent
is the
author
of
the kind of content bearing object
No TPTP formula. May not be expressible in strict first order.
WMD.kif 789-793
If
a kind of process
is a
biochemical
agent delivery of
a kind of biochemical agent
and
another kind of process
is a
subclass
of
a kind of process
,
then
another kind of process
is a
biochemical
agent delivery of
a kind of biochemical agent
No TPTP formula. May not be expressible in strict first order.
WMD.kif 976-980
If
a kind of organism
is a
biological
agent carrier of
a kind of biological agent
and
another kind of organism
is a
subclass
of
a kind of organism
,
then
another kind of organism
is a
biological
agent carrier of
a kind of biological agent
No TPTP formula. May not be expressible in strict first order.
MilitaryDevices.kif 48-56
If
an object
is
capable
of doing
a kind of process
as a
a case role
and
a kind of process
is a
subclass
of
shooting
,
then there exists
another object
such that
the other object
is an
instance
of
weapon
and
the other object
is a
part
of
the object
and
the other object
is
capable
of doing
the kind of process
as a
the case role
No TPTP formula. May not be expressible in strict first order.
Government.kif 619-625
If the
day
a positive integer
is a
commemorates
date of
a kind of holiday
and
an entity
is an
instance
of
a kind of holiday
and
the kind of holiday
is a
subclass
of
fixed holiday
and
an integer
is
less
than or equal to
another entity
-YEAR,
then
the entity
is an
instance
of the
day
the positive integer
No TPTP formula. May not be expressible in strict first order.
Hotel.kif 504-520
If
an agent
is a
customer
of
a cognitive agent
and
the agent
has
a kind of physical
and
a kind of physical
is a
subclass
of
object
and
an entity
is an
instance
of
the kind of physical
,
then
the agent
allow
s
the cognitive agent
to perform task of the type there exists
another entity
such that
the other entity
is an
instance
of
process
and
the entity
is a
resource
for
the other entity
or
the entity
is an
instrument
for
the other entity
or
the entity
is a
patient
of
the other entity
and
the cognitive agent
is an
agent
of
the other entity
or
the cognitive agent
experience
s
the other entity
No TPTP formula. May not be expressible in strict first order.
Hotel.kif 522-538
If
an agent
is a
customer
of
a cognitive agent
and
the agent
has
a kind of physical
and
a kind of physical
is a
subclass
of
process
,
then the statement there exist
an entity
,
another entity
and
a third entity
such that
the other entity
is an
element
of
belongings
of
the agent
and
the agent
is an
agent
of
the entity
and
the cognitive agent
is a
patient
of
the entity
and
the entity
is an
instance
of
the kind of physical
or
the third entity
is an
instance
of
the kind of physical
and
the entity
is a
subprocess
of
the third entity
and
the entity
is
located
at
the other entity
has the
modal
force
of
possibility
No TPTP formula. May not be expressible in strict first order.
Mid-level-ontology.kif 13417-13428
If the
maximum
expected value of
a kind of object
is
a real number
an unit of measure
(s) and
a class
is a
subclass
of
non composite unit of measure
and
the unit of measure
is an
instance
of
the class
,
then the statement there exist
an entity
,
the real number
UANTITY and
a third entity
such that
the entity
is an
instance
of
a kind of object
and the
measure
of
the entity
is
the real number
UANTITY
the third entity
(s) and
the third entity
is an
instance
of
the class
and
the real number
UANTITY
the third entity
(s) is
greater
than
the real number
the unit of measure
(s) has the
modal
force
of
unlikely
No TPTP formula. May not be expressible in strict first order.
Mid-level-ontology.kif 13386-13397
If the
minimum
expected value of
a kind of object
is
a real number
an unit of measure
(s) and
a class
is a
subclass
of
non composite unit of measure
and
the unit of measure
is an
instance
of
the class
,
then the statement there exist
an entity
,
the real number
UANTITY and
a third entity
such that
the entity
is an
instance
of
a kind of object
and the
measure
of
the entity
is
the real number
UANTITY
the third entity
(s) and
the third entity
is an
instance
of
the class
and
the real number
UANTITY is
less
than
the real number
has the
modal
force
of
unlikely
No TPTP formula. May not be expressible in strict first order.
WMD.kif 957-961
If
a disease or syndrome
is
disease
treatment
a kind of biologically active substance
for
a kind of process
and
another kind of process
is a
subclass
of
a kind of process
,
then
the disease or syndrome
is
disease
treatment
a kind of biologically active substance
for
another kind of process
No TPTP formula. May not be expressible in strict first order.
WMD.kif 963-967
If
a disease or syndrome
is
disease
treatment
a kind of biologically active substance
for
a kind of process
and
another kind of biologically active substance
is a
subclass
of
a kind of biologically active substance
,
then
the disease or syndrome
is
disease
treatment
another kind of biologically active substance
for
a kind of process
No TPTP formula. May not be expressible in strict first order.
Economy.kif 2128-2137
If
a geopolitical area
is
electricity
consumption in period
a physical quantity
for
a kind of time interval
and
a kind of time interval
is a
subclass
of
year
or
the kind of time interval
is a
subclass
of the
fiscal
year of
the geopolitical area
,
then there exists
a time position
such that
the time position
is an
instance
of
the kind of time interval
and
the physical quantity
is an
annual
electricity consumption of
the geopolitical area
holds
during
the time position
No TPTP formula. May not be expressible in strict first order.
Economy.kif 2172-2181
If
a geopolitical area
is
electricity
export in period
a physical quantity
for
a kind of time interval
and
a kind of time interval
is a
subclass
of
year
or
the kind of time interval
is a
subclass
of the
fiscal
year of
the geopolitical area
,
then there exists
a time position
such that
the time position
is an
instance
of
the kind of time interval
and
the physical quantity
is an
annual
electricity export of
the geopolitical area
holds
during
the time position
No TPTP formula. May not be expressible in strict first order.
Economy.kif 2218-2227
If
a geopolitical area
is
electricity
import in period
a physical quantity
for
a kind of time interval
and
a kind of time interval
is a
subclass
of
year
or
the kind of time interval
is a
subclass
of the
fiscal
year of
the geopolitical area
,
then there exists
a time position
such that
the time position
is an
instance
of
the kind of time interval
and
the physical quantity
is an
annual
electricity import of
the geopolitical area
holds
during
the time position
No TPTP formula. May not be expressible in strict first order.
Economy.kif 1996-2005
If
a geopolitical area
is
electricity
production in period
a physical quantity
for
a kind of time interval
and
a kind of time interval
is a
subclass
of
year
or
the kind of time interval
is a
subclass
of the
fiscal
year of
the geopolitical area
,
then there exists
a time position
such that
the time position
is an
instance
of
the kind of time interval
and
the physical quantity
is an
annual
electricity production of
the geopolitical area
holds
during
the time position
No TPTP formula. May not be expressible in strict first order.
Media.kif 195-200
If
a kind of getting
is
equal
to
receiving
a
a kind of object
and
another kind of getting
is
equal
to
receiving
a
another kind of object
and
a kind of object
is a
subclass
of
another kind of object
,
then
a kind of getting
is a
subclass
of
another kind of getting
No TPTP formula. May not be expressible in strict first order.
Mid-level-ontology.kif 18234-18239
If
an organization
is
equal
to
another organization
is
preventing
a kind of physical
and
a kind of physical
is a
subclass
of
process
and
the organization
is a part of the organization
the other organization
,
then
the organization
inhibit
s
the kind of physical
No TPTP formula. May not be expressible in strict first order.
Economy.kif 2293-2302
If
a geopolitical area
export
total in period
a currency measure
for
a kind of time interval
and
a kind of time interval
is a
subclass
of
year
or
the kind of time interval
is a
subclass
of the
fiscal
year of
the geopolitical area
,
then there exists
a time position
such that
the time position
is an
instance
of
the kind of time interval
and
the currency measure
is an
annual
export total of
the geopolitical area
holds
during
the time position
No TPTP formula. May not be expressible in strict first order.
Hotel.kif 346-361
If use of
a kind of physical
is free for
a kind of hotel unit
and
a kind of physical
is a
subclass
of
object
and
a temporary residence
is an
instance
of
a kind of hotel unit
and
a human
stays
at
the temporary residence
and
the temporary residence
is an
element
of
belongings
of
an agent
and
an object
is an
instance
of
the kind of physical
and
the object
is
located
at
the temporary residence
and
a process
is an
instance
of
process
and
the human
is an
agent
of
the process
and
the object
is a
patient
of
the process
or
the object
is an
instrument
for
the process
or
the object
is a
resource
for
the process
,
then
the object
is
price
0
united states dollar
(s) for
the human
No TPTP formula. May not be expressible in strict first order.
Hotel.kif 364-378
If use of
a kind of physical
is free for
a kind of hotel unit
and
a kind of physical
is a
subclass
of
process
and
a temporary residence
is an
instance
of
a kind of hotel unit
and
a human
stays
at
the temporary residence
and
the temporary residence
is an
element
of
belongings
of
an agent
and
the human
is a
patient
of
a process
and
the process
is an
instance
of
the kind of physical
or
another process
is an
instance
of
the kind of physical
and
the process
is a
subprocess
of
the other process
and
the process
is
located
at
the temporary residence
,
then
the process
is
price
0.0
united states dollar
(s) for
the human
No TPTP formula. May not be expressible in strict first order.
Hotel.kif 811-832
If use of
a kind of physical
is free for
a kind of hotel function room
and
an entity
is an
instance
of
a kind of hotel function room
and
the entity
is an
element
of
belongings
of
an agent
and
a process
is an
instance
of
renting
and
the entity
is a
patient
of
the process
and
the agent
is an
agent
of
the process
and
the process
end
s up at
another entity
and
a kind of physical
is a
subclass
of
object
,
then the statement there exist
a third entity
and
a fourth entity
such that
the third entity
is an
instance
of
the kind of physical
and
the fourth entity
is an
instance
of
process
and
the third entity
is a
resource
for
the fourth entity
or
the third entity
is an
instrument
for
the fourth entity
or
the third entity
is a
patient
of
the fourth entity
and
the other entity
is an
agent
of
the fourth entity
or
the other entity
experience
s
the fourth entity
has the
modal
force
of
possibility
No TPTP formula. May not be expressible in strict first order.
Hotel.kif 294-313
If
a human
is a
guest
at
an agent
and
the human
stays
at
a temporary residence
and
the temporary residence
is an
element
of
belongings
of
the agent
and
the temporary residence
is an
instance
of
the temporary residence
OOM and
a kind of physical
is an
amenity
in
the temporary residence
OOM and
a kind of physical
is a
subclass
of
object
,
then there exists
another physical
such that
the other physical
is an
instance
of
the kind of physical
and
the other physical
is
located
at
the temporary residence
and
the agent
allow
s
the human
to perform task of the type there exists
an entity
such that
the human
is an
agent
of
the entity
and
the other physical
is an
instrument
for
the entity
or
the other physical
is a
patient
of
the entity
or
the other physical
is a
resource
for
the entity
No TPTP formula. May not be expressible in strict first order.
Media.kif 1900-1904
If
an entity
publishe
s
a class
holds
during
a time position
and
the class
is a
subclass
of
book
,
then
book publishers
is an
attribute
of
the entity
holds
during
the time position
No TPTP formula. May not be expressible in strict first order.
Media.kif 1888-1892
If
an entity
publishe
s
a class
holds
during
a time position
and
the class
is a
subclass
of
musical composition
,
then
music publishers
is an
attribute
of
the entity
holds
during
the time position
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.
Mid-level-ontology.kif 31492-31499
If
an object
can be an argument to
a relation
and
the object
is an
instance
of
the object
C and the number 1 argument of
the relation
is an
instance
of
another class
,
then
the object
C is
equal
to
the other class
or
the object
C is a
subclass
of
the other class
No TPTP formula. May not be expressible in strict first order.
Hotel.kif 1478-1491
If
duty free
is an
attribute
of
an object
and
the object
is an
instance
of
store
,
then there exist
a geopolitical area
,
an entity
,, ,
another kind of object
and
a process
such that
the geopolitical area
is an
instance
of
geopolitical area
and
the object
is
located
at
the geopolitical area
and
another kind of object
is a
subclass
of
object
and
the other kind of object
is an
import
commodity type of
the geopolitical area
and
the entity
is an
instance
of
the other kind of object
and
the process
is an
instance
of
selling
and
the entity
is a
patient
of
the process
and
the process
is
located
at
the object
No TPTP formula. May not be expressible in strict first order.
Mid-level-ontology.kif 24312-24322
If
a day
is a
birthdate
of
a human
and
the day
is an
instance
of the
day
a positive integer
,
then there exist
another kind of day
and
an integer
such that
the human
's
birthday
is
another kind of day
and
the other kind of day
is a
subclass
of
day
and
the integer
is an
instance
of
integer
and
the other kind of day
is
equal
to the
day
the positive integer
and
the integer
is
greater
than
another integer
No TPTP formula. May not be expressible in strict first order.
Merge.kif 221-227
If the number
a positive integer
argument of
a relation
is an
instance
of
a class
and the number
the positive integer
argument of
the relation
is an
instance
of
another class
,
then
the class
is a
subclass
of
the other class
or
the other class
is a
subclass
of
the class
No TPTP formula. May not be expressible in strict first order.
Merge.kif 2992-2997
If the number
a positive integer
argument of
a relation
is a
subclass
of
a class
and
the relation
is an
instance
of
predicate
and
the relation
@ROW,
then
the positive integer
th
element
of (@ROW) is a
subclass
of
the class
No TPTP formula. May not be expressible in strict first order.
Merge.kif 244-250
If the number
a positive integer
argument of
a relation
is a
subclass
of
a class
and the number
the positive integer
argument of
the relation
is a
subclass
of
another class
,
then
the class
is a
subclass
of
the other class
or
the other class
is a
subclass
of
the class
No TPTP formula. May not be expressible in strict first order.
Media.kif 195-200
If
a kind of getting
is
equal
to
receiving
a
a kind of object
and
another kind of getting
is
equal
to
receiving
a
another kind of object
and
a kind of object
is a
subclass
of
another kind of object
,
then
a kind of getting
is a
subclass
of
another kind of getting
No TPTP formula. May not be expressible in strict first order.
Merge.kif 1767-1775
If
a kind of object
is
equal
to the
attr
of
another kind of object
and
an attribute
and
a third object
is an
instance
of
a kind of object
,
then
the third object
is an
instance
of
another kind of object
and
the kind of object
is a
subclass
of
the other kind of object
and
the attribute
is an
attribute
of
the third object
No TPTP formula. May not be expressible in strict first order.
Cars.kif 3447-3476
If
a wearable item
is an
instance
of
hearing protection
and
an animal
is an
instance
of
human
and
the animal
wear
s
the wearable item
,
then
the wearable item
has the purpose there exist
an entity
,
another entity
and
a third entity
such that
the entity
is an
instance
of
process
and
the other entity
is a
subclass
of the
class
described by
the third entity
and
the entity
prevent
s the occurrence of
the other entity
and
the wearable item
is an
instrument
for
the entity
No TPTP formula. May not be expressible in strict first order.
Dining.kif 219-223
If
a catalog
is an
instance
of
cocktail menu
and
a kind of entity
is in
the catalog
,
then
a kind of entity
is a
subclass
of
alcoholic beverage
No TPTP formula. May not be expressible in strict first order.
Dining.kif 208-212
If
a catalog
is an
instance
of
drinks menu
and
a kind of entity
is in
the catalog
,
then
a kind of entity
is a
subclass
of
beverage
No TPTP formula. May not be expressible in strict first order.
Dining.kif 178-182
If
a catalog
is an
instance
of
menu
and
a kind of entity
is in
the catalog
,
then
a kind of entity
is a
subclass
of
food
for
human
No TPTP formula. May not be expressible in strict first order.
Dining.kif 229-233
If
a catalog
is an
instance
of
wine list
and
a kind of entity
is in
the catalog
,
then
a kind of entity
is a
subclass
of
wine list
No TPTP formula. May not be expressible in strict first order.
Mid-level-ontology.kif 9513-9526
If
an object
is an
instance
of
plant
and
another object
is a
part
of
the object
,
then there exist
a process
,
an entity
and
another kind of process
such that
the process
is an
instance
of
another kind of process
and
the other kind of process
is a
subclass
of
keeping
and
the entity
is an
instance
of
water
and
the entity
is a
patient
of
the process
and
the other object
is
capable
of doing
the other kind of process
as a
instrument
and
the other object
is an
instance
of
plant leaf
or
the other object
is an
instance
of
plant stem
No TPTP formula. May not be expressible in strict first order.
Mid-level-ontology.kif 16775-16779
If
a relation
is an
instance
of
economic relation
and the number 1 argument of
the relation
is an
instance
of
a class
,
then
the class
is a
subclass
of
geopolitical area
No TPTP formula. May not be expressible in strict first order.
Merge.kif 3379-3383
If
a function
is an
instance
of
sequence function
and the
range
of
the function
is an instance of
a class
,
then
the class
is a
subclass
of
integer
No TPTP formula. May not be expressible in strict first order.
Cars.kif 3389-3417
If
a wearable item
is an
instance
of
safety harness
and
an animal
is an
instance
of
animal
and
the animal
wear
s
the wearable item
,
then
the wearable item
has the purpose there exist
an entity
,
another entity
and
a third entity
such that
the entity
is an
instance
of
process
and
the wearable item
is an
instrument
for
the entity
and
the animal
is a
patient
of
the entity
and
the other entity
is a
subclass
of the
class
described by
the third entity
and
the entity
prevent
s the occurrence of
the other entity
No TPTP formula. May not be expressible in strict first order.
Sports.kif 1039-1046
If
a corpuscular object
is an
instance
of
ski
and
the corpuscular object
is
made
of
a kind of substance
,
then
a kind of substance
is a
subclass
of
metal
or
the kind of substance
is a
subclass
of
wood
or
the kind of substance
is a
subclass
of
plastic
No TPTP formula. May not be expressible in strict first order.
Economy.kif 4665-4673
If
an object
is an
instance
of
Balsa wood
and
the object
is a
part
of
another object
,
then there exists
a kind of OrganicObjecct
such that
the other object
is an
instance
of a
dead
a kind of OrganicObjecct
and
the kind of OrganicObjecct
is a
subclass
of
PlatnStem
and every
the kind of OrganicObjecct
is
initially
part
of a
Balsa tree
No TPTP formula. May not be expressible in strict first order.
Economy.kif 4678-4686
If
an object
is an
instance
of
Beech wood
and
the object
is a
part
of
another object
,
then there exists
a kind of OrganicObjecct
such that
the other object
is an
instance
of a
dead
a kind of OrganicObjecct
and
the kind of OrganicObjecct
is a
subclass
of
PlatnStem
and every
the kind of OrganicObjecct
is
initially
part
of a
Beech
No TPTP formula. May not be expressible in strict first order.
Economy.kif 4691-4699
If
an object
is an
instance
of
Birch wood
and
the object
is a
part
of
another object
,
then there exists
a kind of OrganicObjecct
such that
the other object
is an
instance
of a
dead
a kind of OrganicObjecct
and
the kind of OrganicObjecct
is a
subclass
of
PlatnStem
and every
the kind of OrganicObjecct
is
initially
part
of a
Birch
No TPTP formula. May not be expressible in strict first order.
Economy.kif 4824-4832
If
an object
is an
instance
of
Cedar wood
and
the object
is a
part
of
another object
,
then there exists
a kind of OrganicObjecct
such that
the other object
is an
instance
of a
dead
a kind of OrganicObjecct
and
the kind of OrganicObjecct
is a
subclass
of
PlatnStem
and every
the kind of OrganicObjecct
is
initially
part
of a
Cedar
No TPTP formula. May not be expressible in strict first order.
Economy.kif 4704-4713
If
an object
is an
instance
of
cherry wood
and
the object
is a
part
of
another object
,
then the statement there exists
an entity
such that
the other object
is an
instance
of a
dead
the entity
and
the entity
is a
subclass
of
PlatnStem
and every
the entity
is
initially
part
of a
black cherry tree
has the
modal
force
of
likely
No TPTP formula. May not be expressible in strict first order.
Economy.kif 4837-4846
If
an object
is an
instance
of
fir wood
and
the object
is a
part
of
another object
,
then the statement there exists
an entity
such that
the other object
is an
instance
of a
dead
the entity
and
the entity
is a
subclass
of
PlatnStem
and every
the entity
is
initially
part
of a
Douglas Fir
has the
modal
force
of
likely
No TPTP formula. May not be expressible in strict first order.
Economy.kif 4651-4660
If
an object
is an
instance
of
hardwood
and
the object
is a
part
of
another object
,
then the statement there exists
an entity
such that
the other object
is an
instance
of a
dead
the entity
and
the entity
is a
subclass
of
plant stem
and every
the entity
is
initially
part
of a
deciduous tree
has the
modal
force
of
likely
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 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.
Cars.kif 5109-5112
There exists
a kind of object
such that
a kind of object
is a
subclass
of
tool box
and the maker of
the kind of object
is
Sortimo Corporation
appearance as argument number 0
No TPTP formula. May not be expressible in strict first order.
MilitaryDevices.kif 1170-1170
Air-to-air missile
is a
subclass
of
air attack missile
No TPTP formula. May not be expressible in strict first order.
MilitaryDevices.kif 1169-1169
Air-to-air missile
is a
subclass
of
air launch missile
No TPTP formula. May not be expressible in strict first order.
MilitaryDevices.kif 1171-1171
Air-to-air missile
is a
subclass
of
guided missile
No TPTP formula. May not be expressible in strict first order.
MilitaryDevices.kif 1647-1647
Amphibious Assault Vehicle
is a
subclass
of
amphibious vehicle
No TPTP formula. May not be expressible in strict first order.
MilitaryDevices.kif 1646-1646
Amphibious Assault Vehicle
is a
subclass
of
military vehicle
No TPTP formula. May not be expressible in strict first order.
MilitaryDevices.kif 1648-1648
Amphibious Assault Vehicle
is a
subclass
of
passenger vehicle
No TPTP formula. May not be expressible in strict first order.
MilitaryDevices.kif 1649-1649
Amphibious Assault Vehicle
is a
subclass
of
powered vehicle
No TPTP formula. May not be expressible in strict first order.
Mid-level-ontology.kif 26453-26453
Ac power source
is a
subclass
of
power source
No TPTP formula. May not be expressible in strict first order.
MilitaryDevices.kif 1123-1123
AG m
is a
subclass
of
air launch missile
No TPTP formula. May not be expressible in strict first order.
MilitaryDevices.kif 1124-1124
AG m
is a
subclass
of
ground attack missile
No TPTP formula. May not be expressible in strict first order.
MilitaryDevices.kif 1203-1203
AG m114
is a
subclass
of
AG m
No TPTP formula. May not be expressible in strict first order.
MilitaryDevices.kif 1205-1205
AG m114
is a
subclass
of
anti armor weapon
No TPTP formula. May not be expressible in strict first order.
MilitaryDevices.kif 1204-1204
AG m114
is a
subclass
of
beam ridingG missile
No TPTP formula. May not be expressible in strict first order.
MilitaryDevices.kif 1136-1136
AG m65
is a
subclass
of
AG m
No TPTP formula. May not be expressible in strict first order.
MilitaryDevices.kif 1138-1138
AG m65
is a
subclass
of
anti armor weapon
No TPTP formula. May not be expressible in strict first order.
MilitaryDevices.kif 1137-1137
AG m65
is a
subclass
of
infra redG missile
No TPTP formula. May not be expressible in strict first order.
MilitaryDevices.kif 1889-1889
A h1
is a
subclass
of
helicopter
No TPTP formula. May not be expressible in strict first order.
MilitaryDevices.kif 1890-1890
A h1
is a
subclass
of
military vehicle
No TPTP formula. May not be expressible in strict first order.
MilitaryDevices.kif 1177-1177
AI m9
is a
subclass
of
air-to-air missile
No TPTP formula. May not be expressible in strict first order.
MilitaryDevices.kif 1178-1178
AI m9
is a
subclass
of
infra redG missile
No TPTP formula. May not be expressible in strict first order.
Mid-level-ontology.kif 25631-25631
Am / fm alarm clock
is a
subclass
of
alarm clock
No TPTP formula. May not be expressible in strict first order.
Mid-level-ontology.kif 25632-25632
Am / fm alarm clock
is a
subclass
of
radio receiver
No TPTP formula. May not be expressible in strict first order.
Communications.kif 293-293
AM radio station
is a
subclass
of
radio station
No TPTP formula. May not be expressible in strict first order.
Communications.kif 236-236
AM radio system
is a
subclass
of
radio system
No TPTP formula. May not be expressible in strict first order.
Transportation.kif 3169-3169
AOC number
is a
subclass
of
symbolic string
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
subclass