Browsing Interface
: Welcome guest :
log in
[
Home
|
Graph
| ]
KB:
SUMO
Language:
ChineseLanguage
ChinesePinyinWriting
ChineseSimplifiedWriting
ChineseTraditionalLanguage
EnglishLanguage
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
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 928-932
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 925-925
The number 1 argument of
part
is an
instance
of
object
No TPTP formula. May not be expressible in strict first order.
Merge.kif 926-926
The number 2 argument of
part
is an
instance
of
object
No TPTP formula. May not be expressible in strict first order.
Merge.kif 924-924
part
is an
instance
of
binary predicate
No TPTP formula. May not be expressible in strict first order.
Merge.kif 923-923
part
is an
instance
of
partial ordering relation
No TPTP formula. May not be expressible in strict first order.
Merge.kif 922-922
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 1028-1028
contains
and
part
are
disjoint
No TPTP formula. May not be expressible in strict first order.
chinese_format.kif 161-161
contains
and
part
are
disjoint
No TPTP formula. May not be expressible in strict first order.
english_format.kif 162-162
contains
and
part
are
disjoint
No TPTP formula. May not be expressible in strict first order.
french_format.kif 100-100
contains
and
part
are
disjoint
No TPTP formula. May not be expressible in strict first order.
relations-it.txt 210-210
contains
and
part
are
disjoint
No TPTP formula. May not be expressible in strict first order.
japanese_format.kif 1929-1929
contains
and
part
are
disjoint
No TPTP formula. May not be expressible in strict first order.
portuguese_format.kif 52-52
contains
and
part
are
disjoint
No TPTP formula. May not be expressible in strict first order.
relations-cz.txt 64-64
contains
and
part
are
disjoint
No TPTP formula. May not be expressible in strict first order.
relations-de.txt 197-197
contains
and
part
are
disjoint
No TPTP formula. May not be expressible in strict first order.
relations-hindi.txt 248-248
contains
and
part
are
disjoint
No TPTP formula. May not be expressible in strict first order.
relations-ro.kif 119-119
contains
and
part
are
disjoint
No TPTP formula. May not be expressible in strict first order.
relations-sv.txt 101-101
contains
and
part
are
disjoint
No TPTP formula. May not be expressible in strict first order.
relations-tg.txt 402-402
contains
and
part
are
disjoint
No TPTP formula. May not be expressible in strict first order.
Mid-level-ontology.kif 25343-25343
initial part
is
internally
related to
part
No TPTP formula. May not be expressible in strict first order.
Mid-level-ontology.kif 25371-25371
initially contains part
is
internally
related to
part
No TPTP formula. May not be expressible in strict first order.
Mid-level-ontology.kif 25397-25397
part types
is
internally
related to
part
No TPTP formula. May not be expressible in strict first order.
Mid-level-ontology.kif 25265-25265
typical part
is
internally
related to
part
No TPTP formula. May not be expressible in strict first order.
Mid-level-ontology.kif 25302-25302
typically contains part
is
internally
related to
part
No TPTP formula. May not be expressible in strict first order.
Merge.kif 975-975
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 14503-14503
half
is a
subrelation
of
part
No TPTP formula. May not be expressible in strict first order.
Mid-level-ontology.kif 26038-26038
in string
is a
subrelation
of
part
No TPTP formula. May not be expressible in strict first order.
Merge.kif 9828-9828
interior part
is a
subrelation
of
part
No TPTP formula. May not be expressible in strict first order.
Mid-level-ontology.kif 14552-14552
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 7777-7788
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 7806-7816
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 7647-7662
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
equal
the list
and
Amounts fn
the kind of substance
,
the corpuscular object
and
the unit of mass
and
equal
the real number
and the
sum
of
the list
No TPTP formula. May not be expressible in strict first order.
Mid-level-ontology.kif 12016-12027
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 12003-12014
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 1912-1917
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 1924-1929
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
equal
the object
E and
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
equal
the object
E and
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
equal
a third object
and the line between
the object
and
the other object
and
equal
the object
and
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
equal
a third object
and the line between
the object
and
the other object
and
equal
the object
and
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 21014-21024
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
equal
the object
2 and
the object
No TPTP formula. May not be expressible in strict first order.
Merge.kif 9853-9858
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 709-717
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
equal
the kind of substance
I and
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 684-688
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-1550
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
a circle
and
equal
the circle
and
circle
,
then the
diameter
of
the circle
is
the length measure
No TPTP formula. May not be expressible in strict first order.
Mid-level-ontology.kif 27362-27374
If
a real number
an unit of measure
(s) is the distance of the
parallelLinesInSpace
a line in space
and
another line in space
and
the unit of measure
is an
instance
of
unit of length
and
the line in space
and
the other line in space
are
parallel
and
an object
is a
part
of
the line in space
and
the object
is an
instance
of
point in space
and
another object
is a
part
of
the other line in space
and
the other object
is an
instance
of
point in space
and the
distance
between
the object
and
the other object
is
another real number
the unit of measure
(s),
then
the real number
is
less
than or equal to
the other real number
No TPTP formula. May not be expressible in strict first order.
Cars.kif 2569-2587
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 1962-1978
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
nerve firing
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
equal
an object
and 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
equal
the fourth object
and
the fifth object
and
equal
the object
2 and 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.
Mid-level-ontology.kif 27429-27441
If
equal
a plane in space
and the
PlaneInSpace
is perpendicular to the line formed by
a point in space
and the centre of the
AstronomicalBody
. and
the point in space
is a
part
of
an object
and
the object
is an
instance
of
region
and
the object
is
located
at
an astronomical body
,
then there exists
a finite line in space
such that
the finite line in space
is an
instance
of
line in space
and
the point in space
and the centre of
AstronomicalBody
the astronomical body
is are end points of
the finite line in space
and
the plane in space
is
right angle
to
the finite line in space
No TPTP formula. May not be expressible in strict first order.
VirusProteinAndCellPart.kif 800-809
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 1873-1895
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 1897-1919
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
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 12620-12627
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 7777-7788
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 7806-7816
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 13013-13020
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 1349-1359
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 428-438
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
equal
the music
and
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 21014-21024
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
equal
the object
2 and
the object
No TPTP formula. May not be expressible in strict first order.
Mid-level-ontology.kif 4521-4538
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
equal
the one dimensional figure
and
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 1215-1224
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 1946-1957
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 13298-13308
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
connected body parts
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
equal
the third object
and
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 1135-1148
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
equal
the other object
and
the third object
No TPTP formula. May not be expressible in strict first order.
ComputingBrands.kif 2636-2644
If
equal
an object
and 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
equal
the fourth object
and
the fifth object
and
equal
the object
2 and 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 5608-5617
If
equal
a kind of object
and
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 7294-7301
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 2551-2567
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 10032-10039
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 25356-25365
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 25383-25391
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 6254-6263
If
an object
is an
instance
of
body area
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 6274-6292
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 1171-1171
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