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
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.
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.
Merge.kif 5299-5299
subset
is a
subrelation
of
subclass
No TPTP formula. May not be expressible in strict first order.
domainEnglishFormat.kif 55683-55683
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 55682-55682
No TPTP formula. May not be expressible in strict first order.
domainEnglishFormat.kif 55681-55681
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
UnitOfArea
and the
measure
of
the physical
is
the real number
the unit of measure
(s) and the
measure
of
the object
is
the other real number
the unit of measure
(s) and
the real number
is an
instance
of
area measure
and
the other real number
is an
instance
of
area measure
and
the other real number
is
greater
than
the real number
No TPTP formula. May not be expressible in strict first order.
Biography.kif 500-510
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 969-973
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 617-623
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 13066-13077
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
NonCompositeUnitOfMeasure
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 13035-13046
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
NonCompositeUnitOfMeasure
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 950-954
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 956-960
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 2123-2132
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 2167-2176
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 2213-2222
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 1991-2000
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 17836-17841
If
an organization
is
equal
to
another organization
is
preventing
a kind of process
and
a kind of process
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 process
No TPTP formula. May not be expressible in strict first order.
Economy.kif 2288-2297
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 1886-1890
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 1874-1878
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 30884-30891
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.
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 2941-2946
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 1728-1736
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.
Dining.kif 215-219
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 204-208
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 225-229
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 9207-9220
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
PlantLeaf
or
the other object
is an
instance
of
PlantStem
No TPTP formula. May not be expressible in strict first order.
Mid-level-ontology.kif 16399-16403
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 3328-3332
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.
Mid-level-ontology.kif 29534-29564
If
a process
is an
instance
of
BreakingRecord
and
an agent
is an
agent
of
the process
,
then there exist
a class
,
another class
,, ,
another process
,, ,
a time point
,, ,
a case role
,, ,
an entity
and
another entity
such that
the class
is an
instance
of
set
and
the agent
is an
instance
of
the class
and
the other class
is a
subclass
of
process
and
the entity
is an
instance
of
region
and
the time point
is an
instance
of
time point
and
the other entity
is an
instance
of
quantity
and
the other process
is an
instance
of
the other class
and
the process
includes a
reference
to
the other entity
and
the other entity
includes a
reference
to
the other process
and
the agent
plays
role in event
the case role
for
the other process
and
the other process
is
located
at
2
and there don't exist
a third entity
and
a fourth entity
such that
the third entity
is an
instance
of
the class
and
the third entity
is not
equal
to
the agent
and
the fourth entity
is an
instance
of
the other class
and
the third entity
plays
role in event
the case role
for
the fourth entity
and
the fourth entity
is
located
at
2
holds
during
interval
between
the time point
and the
end
of the
time
of existence of
the process
No TPTP formula. May not be expressible in strict first order.
Merge.kif 324-330
If the
range
of
a function
is an instance of
a class
and the
range
of
the function
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 339-343
If the values returned by
a function
are
subclasses
of
a kind of class
and
the function
(@ROW) is
equal
to
another class
,
then
the other class
is a
subclass
of
a kind of class
No TPTP formula. May not be expressible in strict first order.
Merge.kif 351-357
If the values returned by
a function
are
subclasses
of
a kind of class
and the values returned by
the function
are
subclasses
of
another kind of class
,
then
a kind of class
is a
subclass
of
another kind of class
or
the other kind of class
is a
subclass
of
the kind of class
No TPTP formula. May not be expressible in strict first order.
Mid-level-ontology.kif 20440-20447
If
medical doctor
is an
attribute
of
an object
,
then there exist
a kind of process
and
another kind of process
such that
a kind of process
is a
subclass
of
diagnostic process
and
another kind of process
is a
subclass
of
therapeutic process
and
the object
is
capable
of doing
the kind of process
as a
agent
and
the object
is
capable
of doing
the other kind of process
as a
agent
No TPTP formula. May not be expressible in strict first order.
Mid-level-ontology.kif 20493-20505
If
art critic
is an
attribute
of
an object
,
then
the object
has the purpose there exist
an entity
,
another entity
and
a third entity
such that
the entity
is an
instance
of
art work
and the
time
of existence of
the object
overlap
s the
time
of existence of
the entity
and
the other entity
is an
instance
of
the third entity
and
the third entity
is a
subclass
of
article
and
the object
is the
author
of
the third entity
and
the other entity
includes a
reference
to
the entity
No TPTP formula. May not be expressible in strict first order.
Mid-level-ontology.kif 20470-20484
If
news reporter
is an
attribute
of
an object
,
then
the object
has the purpose there exist
an entity
,
another entity
and
a third entity
such that
the entity
is an
instance
of
process
and the
time
of existence of
the object
overlap
s the
time
of existence of
the entity
and
the other entity
is an
instance
of
the third entity
and
the third entity
is a
subclass
of
newspaper
or
the third entity
is a
subclass
of
Newsprogram
and
the object
is the
author
of
the third entity
and
the other entity
includes a
reference
to
the entity
No TPTP formula. May not be expressible in strict first order.
Languages.kif 14705-14709
If
a symbolic string
in
ISO-639-1
denotes
a class
,
then
the class
is an
instance
of
human language
or
the class
is a
subclass
of
human language
No TPTP formula. May not be expressible in strict first order.
WMD.kif 1279-1281
If
a disease or syndrome
is
disease
treatment
oral antibiotic
for
a kind of process
,
then
a kind of process
is a
subclass
of
ingesting
No TPTP formula. May not be expressible in strict first order.
WMD.kif 1306-1308
If
a disease or syndrome
is
disease
treatment
topical antibiotic
for
a kind of process
,
then
a kind of process
is a
subclass
of
covering
No TPTP formula. May not be expressible in strict first order.
Merge.kif 2886-2891
If
a class
is
disjointly
decomposed
into @ROW,
then for all
a third class
if
the third class
is a
member
of (@ROW),
then
the third class
is a
subclass
of
the class
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.
Cars.kif 5112-5115
There exists
an agent
such that
the agent
is a
subclass
of
tool box
and the maker of
Sortimo Corporation
is
the agent
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 25834-25834
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 25017-25017
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 25018-25018
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 3168-3168
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