Browsing Interface
: Welcome guest :
log in
[
Home
|
Graph
| ]
KB:
SUMO
Language:
ChineseLanguage
ChinesePinyinWriting
ChineseSimplifiedWriting
ChineseTraditionalLanguage
EnglishLanguage
FrenchLanguage
GermanLanguage
HerbaceousPlant
Hindi
ItalianLanguage
JapaneseLanguage
PortugueseLanguage
SpanishLanguage
SwedishLanguage
WoodyPlant
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
part
Sigma KEE - part
part
appearance as argument number 1
No TPTP formula. May not be expressible in strict first order.
chinese_format.kif 1570-1572
No TPTP formula. May not be expressible in strict first order.
Merge.kif 920-924
No TPTP formula. May not be expressible in strict first order.
japanese_format.kif 143-146
No TPTP formula. May not be expressible in strict first order.
spanish_format.kif 168-171
No TPTP formula. May not be expressible in strict first order.
Merge.kif 917-917
The number 1 argument of
part
is an
instance
of
object
No TPTP formula. May not be expressible in strict first order.
Merge.kif 918-918
The number 2 argument of
part
is an
instance
of
object
No TPTP formula. May not be expressible in strict first order.
Merge.kif 916-916
part
is an
instance
of
binary predicate
No TPTP formula. May not be expressible in strict first order.
Merge.kif 915-915
part
is an
instance
of
partial ordering relation
No TPTP formula. May not be expressible in strict first order.
Merge.kif 914-914
part
is an
instance
of
spatial relation
appearance as argument number 2
No TPTP formula. May not be expressible in strict first order.
Merge.kif 1018-1018
contains
and
part
are
disjoint
No TPTP formula. May not be expressible in strict first order.
chinese_format.kif 161-161
No TPTP formula. May not be expressible in strict first order.
english_format.kif 162-162
No TPTP formula. May not be expressible in strict first order.
french_format.kif 100-100
No TPTP formula. May not be expressible in strict first order.
relations-it.txt 210-210
No TPTP formula. May not be expressible in strict first order.
japanese_format.kif 1929-1929
No TPTP formula. May not be expressible in strict first order.
portuguese_format.kif 52-52
No TPTP formula. May not be expressible in strict first order.
relations-cz.txt 64-64
No TPTP formula. May not be expressible in strict first order.
relations-de.txt 197-197
No TPTP formula. May not be expressible in strict first order.
relations-hindi.txt 248-248
No TPTP formula. May not be expressible in strict first order.
relations-ro.kif 119-119
No TPTP formula. May not be expressible in strict first order.
relations-sv.txt 101-101
No TPTP formula. May not be expressible in strict first order.
relations-tg.txt 402-402
No TPTP formula. May not be expressible in strict first order.
Mid-level-ontology.kif 23754-23754
initial part
is
internally
related to
part
No TPTP formula. May not be expressible in strict first order.
Mid-level-ontology.kif 23782-23782
initially contains part
is
internally
related to
part
No TPTP formula. May not be expressible in strict first order.
Mid-level-ontology.kif 23808-23808
part types
is
internally
related to
part
No TPTP formula. May not be expressible in strict first order.
Mid-level-ontology.kif 23676-23676
typical part
is
internally
related to
part
No TPTP formula. May not be expressible in strict first order.
Mid-level-ontology.kif 23713-23713
typically contains part
is
internally
related to
part
No TPTP formula. May not be expressible in strict first order.
Merge.kif 965-965
component
is a
subrelation
of
part
No TPTP formula. May not be expressible in strict first order.
VirusProteinAndCellPart.kif 34-34
genetic substrate of virus
is a
subrelation
of
part
No TPTP formula. May not be expressible in strict first order.
Mid-level-ontology.kif 13199-13199
half
is a
subrelation
of
part
No TPTP formula. May not be expressible in strict first order.
Mid-level-ontology.kif 24433-24433
in string
is a
subrelation
of
part
No TPTP formula. May not be expressible in strict first order.
Merge.kif 9728-9728
interior part
is a
subrelation
of
part
No TPTP formula. May not be expressible in strict first order.
Mid-level-ontology.kif 13242-13242
most
is a
subrelation
of
part
Display limited to 25 items.
Show next 25
Display limited to 25 items.
Show next 25
antecedent
No TPTP formula. May not be expressible in strict first order.
Geography.kif 7440-7451
An object
is an
instance
of
PM
and
a self connected object
is a
part
of
the object
and the
approximate
diameter
of
the self connected object
is
a real number
micrometer
(s) and 10.0 is
greater
than
the real number
and
the real number
is
greater
than 2.5 if and only if there exists
the object
10 such that
the object
10 is an
instance
of
PM10
and
the object
10 is a
part
of
the object
No TPTP formula. May not be expressible in strict first order.
Geography.kif 7469-7479
An object
is an
instance
of
PM
and
a self connected object
is a
part
of
the object
and the
approximate
diameter
of
the self connected object
is
a real number
micrometer
(s) and
the real number
is
greater
than or equal to 2.5 if and only if there exists
the object
25 such that
the object
25 is an
instance
of
PM2.5
and
the object
25 is a
part
of
the object
No TPTP formula. May not be expressible in strict first order.
Merge.kif 7597-7612
If
amount
a kind of substance
,
a corpuscular object
and
a real number
an unit of mass
(s) and
a kind of substance
I is an
instance
of
the kind of substance
and the
measure
of
the kind of substance
I is
the real number
2
the unit of mass
(s) and
the kind of substance
I is a
part
of
the corpuscular object
,
then there exists
a list
such that
the real number
2
the unit of mass
(s) is a
member
of
the list
and
the list
is
equal
to
Amounts fn
the kind of substance
,
the corpuscular object
and
the unit of mass
and
the real number
is
equal
to the
sum
of
the list
No TPTP formula. May not be expressible in strict first order.
Mid-level-ontology.kif 10712-10723
If
a kind of muscle
and
another kind of muscle
are
antagonist
muscles and
a motion
is an
instance
of
extension
and
a kind of muscle
C is an
instrument
for
the motion
and
another kind of muscle
C moves during
the motion
and
the kind of muscle
C is an
instance
of
the kind of muscle
and
the other kind of muscle
C is an
instance
of
the other kind of muscle
and
the kind of muscle
C is a
part
of
a third object
and
the other kind of muscle
C is a
part
of
the third object
and
the third object
is an
instance
of
animal
,
then
the other kind of muscle
C is
capable
of doing
flexion
as a
instrument
No TPTP formula. May not be expressible in strict first order.
Mid-level-ontology.kif 10699-10710
If
a kind of muscle
and
another kind of muscle
are
antagonist
muscles and
a motion
is an
instance
of
flexion
and
a kind of muscle
C is an
instrument
for
the motion
and
another kind of muscle
C moves during
the motion
and
the kind of muscle
C is an
instance
of
the kind of muscle
and
the other kind of muscle
C is an
instance
of
the other kind of muscle
and
the kind of muscle
C is a
part
of
a third object
and
the other kind of muscle
C is a
part
of
the third object
and
the third object
is an
instance
of
animal
,
then
the other kind of muscle
C is
capable
of doing
extension
as a
instrument
No TPTP formula. May not be expressible in strict first order.
Geography.kif 1754-1759
If
flat terrain
is an
attribute
of
an object
and
a land area
is a
part
of
the object
and
a nonnegative real number
is a
slope
gradient of
the land area
,
then 0.005 is
greater
than
the nonnegative real number
No TPTP formula. May not be expressible in strict first order.
Geography.kif 1766-1771
If
low terrain
is an
attribute
of
an object
and
a land area
is a
part
of
the object
and
a nonnegative real number
is a
slope
gradient of
the land area
,
then 0.03 is
greater
than
the nonnegative real number
No TPTP formula. May not be expressible in strict first order.
Medicine.kif 172-187
If
anaemia
is an
attribute
of
an object
and
another object
is an
instance
of
blood
and
the other object
is a
part
of
the object
and
female
is an
attribute
of
the object
and the
measure
of
the other object
is 0.1
liter
(s) and
the object
E is an
instance
of
hemoglobin
and
the object
E is a
part
of
the other object
and
the object
E2 is not an
instance
of
hemoglobin
and
the object
E is not
equal
to
the object
E2 and
the object
2 is a
part
of
the other object
and the
measure
of
the object
E is
a real number
gram
(s),
then
the real number
is
less
than 12
No TPTP formula. May not be expressible in strict first order.
Medicine.kif 155-170
If
anaemia
is an
attribute
of
an object
and
another object
is an
instance
of
blood
and
the other object
is a
part
of
the object
and
male
is an
attribute
of
the object
and the
measure
of
the other object
is 0.1
liter
(s) and
the object
E is an
instance
of
hemoglobin
and
the object
E is a
part
of
the other object
and
the object
E2 is not an
instance
of
hemoglobin
and
the object
E is not
equal
to
the object
E2 and
the object
2 is a
part
of
the other object
and the
measure
of
the object
E is
a real number
gram
(s),
then
the real number
is
less
than 13
No TPTP formula. May not be expressible in strict first order.
ComputingBrands.kif 2693-2704
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 2665-2676
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.
Mid-level-ontology.kif 19470-19480
If
stressed
is an
attribute
of
an object
and
another object
is an
instance
of
word
and
the object
is a
part
of
the other object
,
then there doesn't exist
the object
2 such that
the object
2 is an
instance
of
syllable
and
the object
2 is a
part
of
the other object
and
stressed
is an
attribute
of
the object
2 and
the object
2 is not
equal
to
the object
No TPTP formula. May not be expressible in strict first order.
Merge.kif 9751-9756
If the
bottom
of
a self connected object
is
another self connected object
and
an object
is a
part
of
the self connected object
and
the object
is not
connected
to
the other self connected object
,
then
the object
is
above
to
the other self connected object
No TPTP formula. May not be expressible in strict first order.
VirusProteinAndCellPart.kif 702-710
If There are
an integer
number of
Chromosomes
in MonoploidChromosomeSet
an eukaryotic cell
. and
an object
is a
part
of
the eukaryotic cell
and
the object
is an
instance
of
cell nucleus
and
the eukaryotic cell
OLL is an
instance
of
collection
and
the eukaryotic cell
OLL is
located
at
the object
and
Chromosome
is a
member
type of
the eukaryotic cell
OLL,
then
the integer
is a
member
count of
the eukaryotic cell
OLL
No TPTP formula. May not be expressible in strict first order.
Medicine.kif 234-249
If the
concentration
of
a kind of substance
in
a mixture
is
a real number
an unit of measure
(s) per
another real number
the unit of measure
2(s) and
a kind of substance
I is an
instance
of
the kind of substance
and
the kind of substance
I is a
part
of
the mixture
and the
measure
of
the kind of substance
I is
a third real number
the unit of measure
3(s) and
the kind of substance
I is a
part
of
the mixture
and
the kind of substance
I2 is not an
instance
of
the kind of substance
and
the kind of substance
I is not
equal
to
the kind of substance
IE2 and
the kind of substance
I2 is a
part
of
the mixture
and the
measure
of
the mixture
is
the other real number
the unit of measure
2(s),
then the approximate value of
the real number
is
the third real number
No TPTP formula. May not be expressible in strict first order.
Geography.kif 514-518
If
an object
is
connected
to
another object
and
the other object
is a
part
of
a third object
,
then
the object
is
connected
to
the third object
No TPTP formula. May not be expressible in strict first order.
Cars.kif 1541-1549
If the bore of
a hole
is
a length measure
and
the hole
is an
instance
of
hole
and
the hole
is
cylinder
and
an object
is a
part
of
the hole
and
the object
is an
instance
of
region
and
the object
is
circle
,
then the
diameter
of
the object
is
the length measure
No TPTP formula. May not be expressible in strict first order.
Cars.kif 2568-2586
If the idle speed of
an internal combustion engine
is the rotation of
a real number
miles per hour
(s) during
a time duration
and
an object
is an
instance
of
automobile
and
a process
is an
instance
of
gas pedal
and
the process
is an
instance
of
pushing
and
the process
end
s up at
another object
and
the internal combustion engine
is a
part
of
the object
and
the other object
is a
part
of
the object
and
a third object
is an
instance
of
crankshaft
and
the third object
is a
part
of
the internal combustion engine
and the
measure
of
the third object
is the rotation of
an entity
miles per hour
(s) during
the time duration
holds
during
the
time
of existence of
the process
,
then the statement
the entity
is
greater
than
the real number
has the
modal
force
of
likely
No TPTP formula. May not be expressible in strict first order.
Anatomy.kif 1923-1939
If
ennervates
a kind of nerve
and
a kind of muscle
and
an object
is an
instance
of
a kind of nerve
and
another object
is an
instance
of
a kind of muscle
and
the object
is a
part
of
a third object
and
the other object
is a
part
of
the third object
and
healthy
is an
attribute
of
the third object
and
the third object
is an
instance
of
human
,
then
the object
has the purpose there exist
the object
F and
another entity
such that
the object
F is an
instance
of
NerveFiring
and
the object
is an
instrument
for
the object
F and
the kind of muscle
is an
instance
of
MuscleContraction
and
the other object
is an
instrument
for
the other object
V and
the object
F
cause
s
the kind of muscle
No TPTP formula. May not be expressible in strict first order.
ComputingBrands.kif 2636-2644
If
an object
is
equal
to the line between
another object
and
a third object
and
a fourth object
is a
part
of
the object
and
a fifth object
is a
part
of
the object
and
the fourth object
is not
equal
to
the fifth object
and
the object
2 is
equal
to the line between
the fourth object
and
the fifth object
,
then
the object
2 is a
part
of
the object
No TPTP formula. May not be expressible in strict first order.
VirusProteinAndCellPart.kif 793-802
If There are
an integer
number of
Chromosomes
in a
Gamete
cell
a gamete
. and
the gamete
is an
instance
of
gamete
and
an object
is a
part
of
the gamete
and
the object
is an
instance
of
cell nucleus
and
a collection
is an
instance
of
collection
and
the collection
is
located
at
the object
and
Chromosome
is a
member
type of
the collection
,
then
the integer
is a
member
count of
the collection
No TPTP formula. May not be expressible in strict first order.
Anatomy.kif 1838-1860
If
lateral recumbant
is an
attribute
of
an object
and
the object
is
on
to
another object
holds
during
a time position
and
a third object
is an
instance
of
left arm
and
the third object
is a
part
of
the object
and
a fourth object
is an
instance
of
right arm
and
the fourth object
is a
part
of
the object
and
a fifth object
is an
instance
of
left leg
and
the fifth object
is a
part
of
the object
and
a sixth object
is an
instance
of
right leg
and
the sixth object
is a
part
of
the object
and
the third object
meet
s
the other object
or
the fifth object
meet
s
the other object
,
then
the fourth object
doesn't
meet
the other object
and
the sixth object
doesn't
meet
the other object
holds
during
the time position
No TPTP formula. May not be expressible in strict first order.
Anatomy.kif 1862-1884
If
lateral recumbant
is an
attribute
of
an object
and
the object
is
on
to
another object
holds
during
a time position
and
a third object
is an
instance
of
left arm
and
the third object
is a
part
of
the object
and
a fourth object
is an
instance
of
right arm
and
the fourth object
is a
part
of
the object
and
a fifth object
is an
instance
of
left leg
and
the fifth object
is a
part
of
the object
and
a sixth object
is an
instance
of
right leg
and
the sixth object
is a
part
of
the object
and
the fourth object
meet
s
the other object
or
the sixth object
meet
s
the other object
,
then
the third object
doesn't
meet
the other object
and
the fifth object
doesn't
meet
the other object
holds
during
the time position
No TPTP formula. May not be expressible in strict first order.
Anatomy.kif 1799-1807
If
prone
is an
attribute
of
an object
and
the object
is
on
to
another object
holds
during
a time position
and
a third object
is an
instance
of
chest
and
the third object
is a
part
of
the object
,
then
the third object
meet
s
the other object
No TPTP formula. May not be expressible in strict first order.
Merge.kif 18325-18333
If
dead or missing body part fn
a class
is an
attribute
of
an object
holds
during
a time position
and
the class
I is an
instance
of
the class
and
the class
I is a
part
of
the object
and
the class
I has the purpose
a formula
,
then
the formula
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 12512-12519
A process
is an
instance
of
combining
and
an object
is a
resource
for
the process
and
an entity
is a
result
of
the process
if and only if
the object
is not a
part
of
the entity
holds
during
the
beginning
of the
time
of existence of
the process
and
the object
is a
part
of
the entity
holds
during
the
end
of the
time
of existence of
the process
No TPTP formula. May not be expressible in strict first order.
Geography.kif 7440-7451
An object
is an
instance
of
PM
and
a self connected object
is a
part
of
the object
and the
approximate
diameter
of
the self connected object
is
a real number
micrometer
(s) and 10.0 is
greater
than
the real number
and
the real number
is
greater
than 2.5 if and only if there exists
the object
10 such that
the object
10 is an
instance
of
PM10
and
the object
10 is a
part
of
the object
No TPTP formula. May not be expressible in strict first order.
Geography.kif 7469-7479
An object
is an
instance
of
PM
and
a self connected object
is a
part
of
the object
and the
approximate
diameter
of
the self connected object
is
a real number
micrometer
(s) and
the real number
is
greater
than or equal to 2.5 if and only if there exists
the object
25 such that
the object
25 is an
instance
of
PM2.5
and
the object
25 is a
part
of
the object
No TPTP formula. May not be expressible in strict first order.
Mid-level-ontology.kif 11709-11716
An object
is an
instance
of
bone
if and only if there exists
another object
such that
the other object
is an
instance
of
skeleton
or
the other object
is an
instance
of
exoskeleton
and
the object
is a
part
of
the other object
No TPTP formula. May not be expressible in strict first order.
Transportation.kif 1277-1287
A geographic area
is
total
facility type in area the
class
corresponding to
airport with paved runway
for
a nonnegative integer
if and only if there exist
a symbolic string
and
an entity
such that
the nonnegative integer
is a
cardinality
of the
class
described by
the symbolic string
No TPTP formula. May not be expressible in strict first order.
UXExperimentalTerms.kif 632-640
If
an user account
is an
account
at
a web site
,
then there exist
an object
and
the web site
_OWNER such that
the object
is an
instance
of
database
and
the web site
_OWNER is an
instance
of
agent
and
the web site
_OWNER
possess
es
the web site
and
the web site
_OWNER
possess
es
the object
and
the user account
is a
part
of
the object
No TPTP formula. May not be expressible in strict first order.
Music.kif 316-322
If
an image
is the
image
on
an album
and
an object
is an
instance
of the
set
of copies on
a kind of data storage device
of
the album
and
a self connected object
contain
s
the object
,
then the statement
the image
is a
part
of the
front
of
the self connected object
has the
modal
force
of
likely
No TPTP formula. May not be expressible in strict first order.
Music.kif 426-436
If
mashup
is an
attribute
of
an object
and
the object
is an
instance
of
recording
,
then there exist
the object
1,
the object
2,, ,
a music
and
another music
such that
the object
1 is a
recording
of
the music
and
the object
2 is a
recording
of
the other music
and
the music
is not
equal
to
the other music
and
the object
1 is a
part
of
the object
and
the object
2 is a
part
of
the object
No TPTP formula. May not be expressible in strict first order.
Mid-level-ontology.kif 19470-19480
If
stressed
is an
attribute
of
an object
and
another object
is an
instance
of
word
and
the object
is a
part
of
the other object
,
then there doesn't exist
the object
2 such that
the object
2 is an
instance
of
syllable
and
the object
2 is a
part
of
the other object
and
stressed
is an
attribute
of
the object
2 and
the object
2 is not
equal
to
the object
No TPTP formula. May not be expressible in strict first order.
Mid-level-ontology.kif 4071-4088
If
a geometric figure
is an
attribute
of
an object
and
the object
is an
instance
of
four-poster bed
and
the geometric figure
is an
instance
of
quadrilateral
and the
size
of
the geometric figure
is
an one dimensional figure
and the
size
of
the geometric figure
is
another one dimensional figure
and
the one dimensional figure
is not
equal
to
the other one dimensional figure
,
then there exist
another object
,
a third object
,, ,
a geometric point
and
a fourth object
such that
the other object
is a
part
of
the object
and
the third object
is an
instance
of
floor
and
the object
is
on
to
the third object
and
the other object
is
vertical
to
the third object
and
the one dimensional figure
is
point
of intersection
the other one dimensional figure
for
the geometric point
and
the geometric point
is an
attribute
of
the fourth object
and
the fourth object
meet
s
the other object
No TPTP formula. May not be expressible in strict first order.
Hotel.kif 1207-1216
If
an attribute
is an
attribute
of
an object
and
the attribute
is an
instance
of
hotel level attribute
,
then
the object
is an
instance
of
building level
and there exists
another object
such that
the other object
is an
instance
of
hotel
and
the object
is a
part
of
the other object
No TPTP formula. May not be expressible in strict first order.
Hotel.kif 1935-1946
If
traveler accommodation
is an
attribute
of
an agent
and
the agent
is
capable
of doing
service
as a
agent
,
then there exist
a cognitive agent
and
an object
such that
the agent
employ
s
the cognitive agent
and
maid
is an
attribute
of
the cognitive agent
and
the object
is an
instance
of
hotel unit
and
the object
is a
part
of
belongings
of
the agent
and
the object
is
capable
of doing
service
as a
patient
and
the cognitive agent
is
capable
of doing
service
as a
service provider
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.
Mid-level-ontology.kif 11994-12004
If a
a kind of body part
is
connected
to a
another kind of body part
and
healthy
is an
attribute
of
an object
,
then there exist
a kind of body part
I and
another kind of body part
I such that
the kind of body part
I is an
instance
of
the kind of body part
and
the other kind of body part
I is an
instance
of
the other kind of body part
and
the kind of body part
I is a
part
of
the object
and
the other kind of body part
I is a
part
of
the object
and
the kind of body part
I is
connected
to
the other kind of body part
I
No TPTP formula. May not be expressible in strict first order.
Anatomy.kif 32-46
If
connectedBodyPartTypes
a kind of body part
,
another kind of body part
and
a kind of organism
and
a kind of organism
C is an
instance
of
the kind of organism
and
disease or syndrome
is not an
attribute
of
another object
,
then there exist
a third object
and
a fourth object
such that
the third object
is an
instance
of
a kind of body part
and
the fourth object
is an
instance
of
another kind of body part
and
the third object
is not
equal
to
the fourth object
and
the third object
is a
part
of
the kind of organism
C and
the fourth object
is a
part
of
the kind of organism
C and
the third object
is
connected
to
the fourth object
No TPTP formula. May not be expressible in strict first order.
Hotel.kif 1127-1140
If
an object
is an
element
of
belongings
of
an organization
and
annex room
is an
attribute
of
the object
and
the object
is an
instance
of
hotel room
,
then there exist
another object
,
a third object
and
another organization
such that
the other organization
is a part of the organization
the organization
and
the other organization
is an
instance
of
front desk
and
the other organization
is
located
at
the other object
and
the other object
is an
element
of
belongings
of
the organization
and
the third object
is an
element
of
belongings
of
the organization
and
the object
is a
part
of
the third object
and
the other object
is not
equal
to
the third object
No TPTP formula. May not be expressible in strict first order.
ComputingBrands.kif 2636-2644
If
an object
is
equal
to the line between
another object
and
a third object
and
a fourth object
is a
part
of
the object
and
a fifth object
is a
part
of
the object
and
the fourth object
is not
equal
to
the fifth object
and
the object
2 is
equal
to the line between
the fourth object
and
the fifth object
,
then
the object
2 is a
part
of
the object
No TPTP formula. May not be expressible in strict first order.
Economy.kif 5267-5276
If
a kind of object
is
equal
to
Object
made from
a kind of organic object
and
a kind of object
is a
subclass
of
object
,
then there exist
another object
and
a third object
such that
the other object
is an
instance
of a
dead
a kind of organic object
and
the other object
is a
part
of
the third object
and
the third object
is an
instance
of
the kind of organic object
No TPTP formula. May not be expressible in strict first order.
Mid-level-ontology.kif 6351-6358
If
an agent
experience
s
a process
and
the agent
is an
instance
of
pain
in the
a body part
,
then there exists
the body part
ART such that
the body part
ART is a
part
of
the process
and
the body part
ART is
located
at
the body part
No TPTP formula. May not be expressible in strict first order.
Cars.kif 2550-2566
If the
measure
of
an object
is
a function quantity
holds
during
a time position
and the idle speed of
an internal combustion engine
is
the function quantity
and
another object
is an
instance
of
automobile
and
the internal combustion engine
is a
part
of
the other object
and
the object
is a
part
of
the internal combustion engine
,
then the statement there don't exist
an entity
and
another entity
such that
the entity
takes place
during
the time position
and
the entity
is an
instance
of
pushing
and
the entity
end
s up at
the other entity
and
the other entity
is a
part
of
the other object
has the
modal
force
of
likely
No TPTP formula. May not be expressible in strict first order.
Merge.kif 9930-9937
If
a hole
is a
hole
in
a self connected object
and
another hole
is a
hole
in
the self connected object
,
then for all
a third hole
if
the third hole
is a
part
of the
union
of the parts of
the hole
and
the other hole
,
then
the third hole
is a
hole
in
the self connected object
No TPTP formula. May not be expressible in strict first order.
Mid-level-ontology.kif 23767-23776
If every
a kind of object
is
initially
part
of a
another kind of object
and
a physical
is an
instance
of
a kind of object
,
then there exists
an entity
such that
the entity
is an
instance
of
another kind of object
and
the physical
is a
part
of
the entity
holds
during
the
beginning
of the
time
of existence of
the physical
No TPTP formula. May not be expressible in strict first order.
Mid-level-ontology.kif 23794-23802
If instance of
a kind of object
are always
initially
part
of instances of
another kind of object
and
a physical
is an
instance
of
another kind of object
,
then there exists
an entity
such that
the entity
is an
instance
of
a kind of object
and
the entity
is a
part
of
the physical
holds
during
the
beginning
of the
time
of existence of
the physical
No TPTP formula. May not be expressible in strict first order.
Medicine.kif 6237-6246
If
an object
is an
instance
of
BodyAreaFn
a kind of body part
and
another object
is an
instance
of
animal
and
the object
is a
part
of
the other object
,
then there exists
a third object
such that
the third object
is an
instance
of
a kind of body part
and
the object
is
near
to
the third object
and
the third object
is a
part
of
the other object
No TPTP formula. May not be expressible in strict first order.
Medicine.kif 6257-6275
If
a process
is an
instance
of
amputation
and
an entity
is a
patient
of
the process
and
an object
is an
instance
of
limb
,
then there exist
another object
and
a third object
such that
the other object
is a
part
of
the object
and
the third object
is a
part
of
the other object
and
the third object
is an
instance
of
bone
and
the other object
is a
part
of
the entity
holds
during
immediately
before
the
time
of existence of
the process
and
the other object
is not a
part
of
the entity
holds
during
immediately
before
the
time
of existence of
the process
Display limited to 25 items.
Show next 25
Display limited to 25 items.
Show next 25
appearance as argument number 0
No TPTP formula. May not be expressible in strict first order.
VirusProteinAndCellPart.kif 1164-1164
The
viral
part of
a virus
and
a kind of virus part
is a
part
of
the virus
No TPTP formula. May not be expressible in strict first order.
CountriesAndRegions.kif 711-711
Atlanta georgia
is a
part
of
georgia
No TPTP formula. May not be expressible in strict first order.
CountriesAndRegions.kif 662-662
Australia
is a
part
of
oceania
No TPTP formula. May not be expressible in strict first order.
CountriesAndRegions.kif 714-714
Baltimore maryland
is a
part
of
maryland
No TPTP formula. May not be expressible in strict first order.
CountriesAndRegions.kif 724-724
Boston, Massachusetts
is a
part
of
massachusetts
No TPTP formula. May not be expressible in strict first order.
CountriesAndRegions.kif 1611-1611
Chicago united states
is a
part
of
illinois
No TPTP formula. May not be expressible in strict first order.
CountriesAndRegions.kif 854-854
Cleveland ohio
is a
part
of
ohio
No TPTP formula. May not be expressible in strict first order.
CountriesAndRegions.kif 915-915
Connecticut
is a
part
of
new england
No TPTP formula. May not be expressible in strict first order.
CountriesAndRegions.kif 851-851
Dallas texas
is a
part
of
texas
No TPTP formula. May not be expressible in strict first order.
CountriesAndRegions.kif 841-841
Detroit michigan
is a
part
of
michigan
No TPTP formula. May not be expressible in strict first order.
CountriesAndRegions.kif 835-835
Fargo north dakota
is a
part
of
north dakota
No TPTP formula. May not be expressible in strict first order.
CountriesAndRegions.kif 1242-1242
Germany
is a
part
of
europe
No TPTP formula. May not be expressible in strict first order.
CountriesAndRegions.kif 1245-1245
Greece
is a
part
of
europe
No TPTP formula. May not be expressible in strict first order.
CountriesAndRegions.kif 828-828
Houston texas
is a
part
of
texas
No TPTP formula. May not be expressible in strict first order.
CountriesAndRegions.kif 832-832
Hudson river
is a
part
of
new york state
No TPTP formula. May not be expressible in strict first order.
CountriesAndRegions.kif 728-728
Kansas city missouri
is a
part
of
missouri
No TPTP formula. May not be expressible in strict first order.
CountriesAndRegions.kif 820-820
Korean peninsula
is a
part
of
asia
No TPTP formula. May not be expressible in strict first order.
CountriesAndRegions.kif 805-805
Long island
is a
part
of
new york state
No TPTP formula. May not be expressible in strict first order.
CountriesAndRegions.kif 810-810
Los angeles california
is a
part
of
california
No TPTP formula. May not be expressible in strict first order.
CountriesAndRegions.kif 731-731
Manchester new hampshire
is a
part
of
new hampshire
No TPTP formula. May not be expressible in strict first order.
CountriesAndRegions.kif 989-989
Massachusetts
is a
part
of
new england
No TPTP formula. May not be expressible in strict first order.
CountriesAndRegions.kif 733-733
Memphis tennessee
is a
part
of
tennessee
No TPTP formula. May not be expressible in strict first order.
CountriesAndRegions.kif 737-737
Minneapolis minnesota
is a
part
of
minnesota
No TPTP formula. May not be expressible in strict first order.
CountriesAndRegions.kif 740-740
Mississippi river
is a
part
of
united states
No TPTP formula. May not be expressible in strict first order.
CountriesAndRegions.kif 746-746
Montreal canada
is a
part
of
canada
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
part