forall
(=>
(
coilCount
?WC ?N)
(
exists
(?C)
(
and
(
instance
?C
Collection
)
(
memberCount
?C ?N)
(
forall
(?M)
(=>
(
member
?M ?C)
(
and
(
attribute
?M
ClosedTwoDimensionalFigure
)
(
part
?M ?WC)
(
not
(
exists
(?M2)
(
and
(
overlapsSpatially
?M2 ?M)
(
member
?M2 ?C))))))))))
Cars.kif 3117-3133
If the number of coils in
a wire coil
is
an integer
,
then there exists
a collection
such that
the collection
is an
instance
of
collection
and
the integer
is a
member
count of
the collection
and for all
an object
if
the object
is a
member
of
the collection
,
then
closed two dimensional figure
is an
attribute
of
the object
and
the object
is a
part
of
the wire coil
and there doesn't exist
the object
2 such that
the object
2 and
the object
overlapsSpatially
and
the object
2 is a
member
of
the collection
(=>
(
completelyFills
?OBJ1 ?HOLE)
(
forall
(?OBJ2)
(=>
(
connected
?OBJ2 ?HOLE)
(
connected
?OBJ2 ?OBJ1))))
Merge.kif 10039-10044
If
an object
completely
fill
s
a hole
,
then for all
another object
if
the other object
is
connected
to
the hole
,
then
the other object
is
connected
to
the object
(=>
(
copy
?OBJ1 ?OBJ2)
(
forall
(?ATTR)
(=>
(
attribute
?OBJ1 ?ATTR)
(
attribute
?OBJ2 ?ATTR))))
Merge.kif 3855-3860
If
an object
is a
copy
of
another object
,
then for all
an attribute
if
the attribute
is an
attribute
of
the object
,
then
the attribute
is an
attribute
of
the other object
(=>
(
discography
?A ?D)
(
forall
(?X)
(=>
(
member
?X ?D)
(
exists
(?I)
(
musician
?X ?A ?I)))))
Music.kif 243-249
If
a human
has
discography
a discography
,
then for all
a music recording
if
the music recording
is a
member
of
the discography
,
then there exists
a kind of making music
such that
the human
performed
the music recording
(=>
(
disjointDecomposition
?CLASS @ROW)
(
forall
(?ITEM)
(=>
(
inList
?ITEM
(
ListFn
@ROW))
(
subclass
?ITEM ?CLASS))))
Merge.kif 2950-2955
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
(=>
(
disjointDecomposition
?CLASS @ROW)
(
forall
(?ITEM1 ?ITEM2)
(=>
(
and
(
inList
?ITEM1
(
ListFn
@ROW))
(
inList
?ITEM2
(
ListFn
@ROW))
(
not
(
equal
?ITEM1 ?ITEM2)))
(
disjoint
?ITEM1 ?ITEM2))))
Merge.kif 2957-2966
If
a class
is
disjointly
decomposed
into @ROW,
then for all
a third class
and
a fourth class
if
the third class
is a
member
of (@ROW) and
the fourth class
is a
member
of (@ROW) and
the third class
is not
equal
to
the fourth class
,
then
the third class
is
disjoint
from
the fourth class
(=>
(
dressCode
?CODE ?AGENT)
(
modalAttribute
(
exists
(?OUTFIT ?T)
(
and
(
instance
?OUTFIT
Outfit
)
(
subjectiveAttribute
?OUTFIT ?CODE ?AGENT)
(
holdsDuring
?T
(
forall
(?CUST ?ITEM)
(
and
(
customer
?CUST ?AGENT)
(
locatedAtTime
?CUST ?T ?AGENT)
(
member
?ITEM ?OUTFIT)
(
wears
?CUST ?ITEM))))))
Obligation
))
Dining.kif 492-505
If
an agent
requires customers to wear
an ambience
,
then the statement there exist
an entity
and
another entity
such that
the entity
is an
instance
of
outfit
and
the agent
believes
the entity
is
the ambience
and for all
a third entity
and
a fourth entity
the agent
is a
customer
of
the third entity
and
the third entity
located
at time
the other entity
for
the agent
and
the fourth entity
is a
member
of
the entity
and
the third entity
wear
s
the fourth entity
holds
during
the other entity
has the
modal
force
of
obligation
(=>
(
equal
(
BeginFn
?INTERVAL) ?POINT)
(
forall
(?OTHERPOINT)
(=>
(
and
(
temporalPart
?OTHERPOINT ?INTERVAL)
(
not
(
equal
?OTHERPOINT ?POINT)))
(
before
?POINT ?OTHERPOINT))))
Merge.kif 7998-8005
If the
beginning
of
a time interval
is
equal
to
a time point
,
then for all
another time point
if
the other time point
is a
part
of
the time interval
and
the other time point
is not
equal
to
the time point
,
then
the time point
happens
before
the other time point
(=>
(
equal
(
EndFn
?INTERVAL) ?POINT)
(
forall
(?OTHERPOINT)
(=>
(
and
(
temporalPart
?OTHERPOINT ?INTERVAL)
(
not
(
equal
?OTHERPOINT ?POINT)))
(
before
?OTHERPOINT ?POINT))))
Merge.kif 8016-8023
If the
end
of
a time interval
is
equal
to
a time point
,
then for all
another time point
if
the other time point
is a
part
of
the time interval
and
the other time point
is not
equal
to
the time point
,
then
the other time point
happens
before
the time point
(=>
(
equal
(
ImmediateFamilyFn
?P) ?FAMILY)
(
forall
(?MEMBER)
(=>
(
member
?MEMBER ?FAMILY)
(
exists
(?OTHER)
(
or
(
parent
?MEMBER ?OTHER)
(
parent
?OTHER ?MEMBER))))))
Merge.kif 16291-16299
If the
immediate
family of
a human
is
equal
to
a family group
,
then for all
an organism
if
the organism
is a
member
of
the family group
,
then there exists
another organism
such that
the other organism
is a
parent
of
the organism
or
the organism
is a
parent
of
the other organism
(=>
(
equal
(
MinimalCutSetFn
?GRAPH) ?PATHCLASS)
(
exists
(?NUMBER)
(
forall
(?PATH)
(=>
(
instance
?PATH ?PATHCLASS)
(
pathLength
?PATH ?NUMBER)))))
Merge.kif 6091-6097
If the
set
of minimal paths that partition
a graph
into two separate graphs is
equal
to
a kind of graph path
,
then there exists
a positive integer
such that for all
another graph path
if
the other graph path
is an
instance
of
a kind of graph path
,
then the
length
of
the other graph path
is
the positive integer
(=>
(
equal
(
TemporalCompositionFn
?INTERVAL ?INTERVALTYPE) ?CLASS)
(
forall
(?TIME)
(=>
(
and
(
instance
?TIME
TimePoint
)
(
temporalPart
?TIME ?INTERVAL))
(
exists
(?INSTANCE)
(
and
(
instance
?INSTANCE ?CLASS)
(
temporalPart
?TIME ?INSTANCE))))))
Merge.kif 9447-9457
If
decomposition
of
a time interval
into
the time interval
TYPEs is
equal
to
another kind of time interval
,
then for all
a time position
if
the time position
is an
instance
of
time point
and
the time position
is a
part
of
the time interval
,
then there exists
another time position
such that
the other time position
is an
instance
of
another kind of time interval
and
the time position
is a
part
of
the other time position
(=>
(
equal
(
TemporalCompositionFn
?INTERVAL ?INTERVALTYPE) ?CLASS)
(
forall
(?TIME1 ?TIME2)
(=>
(
and
(
instance
?TIME1 ?CLASS)
(
instance
?TIME2 ?CLASS)
(
not
(
equal
?TIME1 ?TIME2)))
(
or
(
meetsTemporally
?TIME1 ?TIME2)
(
meetsTemporally
?TIME2 ?TIME1)
(
earlier
?TIME1 ?TIME2)
(
earlier
?TIME2 ?TIME1)))))
Merge.kif 9395-9407
If
decomposition
of
a time interval
into
the time interval
TYPEs is
equal
to
another kind of time interval
,
then for all
a third time interval
and
a fourth time interval
if
the third time interval
is an
instance
of
another kind of time interval
and
the fourth time interval
is an
instance
of
the other kind of time interval
and
the third time interval
is not
equal
to
the fourth time interval
,
then
the third time interval
meet
s
the fourth time interval
or
the fourth time interval
meet
s
the third time interval
or
the third time interval
happens
earlier
than
the fourth time interval
or
the fourth time interval
happens
earlier
than
the third time interval
(=>
(
equal
(
TemporalCompositionFn
?INTERVAL ?INTERVALTYPE) ?CLASS)
(
forall
(?TIME1 ?TIME2)
(=>
(
and
(
instance
?TIME1 ?INTERVALTYPE)
(
instance
?TIME2 ?CLASS))
(
exists
(?DURATION)
(
and
(
duration
?TIME1 ?DURATION)
(
duration
?TIME2 ?DURATION))))))
Merge.kif 9383-9393
If
decomposition
of
a time interval
into
the time interval
TYPEs is
equal
to
another kind of time interval
,
then for all
a third time interval
and
a fourth time interval
if
the third time interval
is an
instance
of
the time interval
TYPE and
the fourth time interval
is an
instance
of
another kind of time interval
,
then there exists
a time duration
such that
duration
of
the third time interval
is
the time duration
and
duration
of
the fourth time interval
is
the time duration
(=>
(
equal
(
TemporalCompositionFn
?INTERVAL ?INTERVALTYPE) ?CLASS)
(
forall
(?TIME1)
(=>
(
and
(
instance
?TIME1 ?CLASS)
(
not
(
finishes
?TIME1 ?INTERVAL)))
(
exists
(?TIME2)
(
and
(
instance
?TIME2 ?CLASS)
(
meetsTemporally
?TIME1 ?TIME2))))))
Merge.kif 9423-9433
If
decomposition
of
a time interval
into
the time interval
TYPEs is
equal
to
another kind of time interval
,
then for all
a third time interval
if
the third time interval
is an
instance
of
another kind of time interval
and
the third time interval
doesn't
finish
the time interval
,
then there exists
a fourth time interval
such that
the fourth time interval
is an
instance
of
the other kind of time interval
and
the third time interval
meet
s
the fourth time interval
(=>
(
equal
(
TemporalCompositionFn
?INTERVAL ?INTERVALTYPE) ?CLASS)
(
forall
(?TIME1)
(=>
(
and
(
instance
?TIME1 ?CLASS)
(
not
(
starts
?TIME1 ?INTERVAL)))
(
exists
(?TIME2)
(
and
(
instance
?TIME2 ?CLASS)
(
meetsTemporally
?TIME2 ?TIME1))))))
Merge.kif 9435-9445
If
decomposition
of
a time interval
into
the time interval
TYPEs is
equal
to
another kind of time interval
,
then for all
a third time interval
if
the third time interval
is an
instance
of
another kind of time interval
and
the third time interval
doesn't
start
the time interval
,
then there exists
a fourth time interval
such that
the fourth time interval
is an
instance
of
the other kind of time interval
and
the fourth time interval
meet
s
the third time interval
(=>
(
equal
?ATTR1 ?ATTR2)
(
forall
(?THING)
(<=>
(
property
?THING ?ATTR1)
(
property
?THING ?ATTR2))))
Merge.kif 267-272
If
an attribute
is
equal
to
another attribute
,
then for all
an entity
the entity
the
attribute
the attribute
if and only if
the entity
the
attribute
the other attribute
(=>
(
equal
?CLASS1 ?CLASS2)
(
forall
(?THING)
(<=>
(
instance
?THING ?CLASS1)
(
instance
?THING ?CLASS2))))
Merge.kif 281-286
If
a class
is
equal
to
another class
,
then for all
an entity
the entity
is an
instance
of
the class
if and only if
the entity
is an
instance
of
the other class
(=>
(
equal
?OBJ3
(
MereologicalDifferenceFn
?OBJ1 ?OBJ2))
(
forall
(?PART)
(<=>
(
properPart
?PART ?OBJ3)
(
and
(
properPart
?PART ?OBJ1)
(
not
(
properPart
?PART ?OBJ2))))))
Merge.kif 9837-9846
If
an object
is
equal
to the
difference
between the parts of
another object
and
a third object
,
then for all
a fourth object
the fourth object
is a
proper
part
of
the object
if and only if
the fourth object
is a
proper
part
of
the other object
and
the fourth object
is not a
proper
part
of
the third object
(=>
(
equal
?OBJ3
(
MereologicalProductFn
?OBJ1 ?OBJ2))
(
forall
(?PART)
(<=>
(
part
?PART ?OBJ3)
(
and
(
part
?PART ?OBJ1)
(
part
?PART ?OBJ2)))))
Merge.kif 9817-9824
If
an object
is
equal
to the
intersection
of the parts of
another object
and
a third object
,
then for all
a fourth object
the fourth object
is a
part
of
the object
if and only if
the fourth object
is a
part
of
the other object
and
the fourth object
is a
part
of
the third object
(=>
(
equal
?OBJ3
(
MereologicalSumFn
?OBJ1 ?OBJ2))
(
forall
(?PART)
(<=>
(
part
?PART ?OBJ3)
(
or
(
part
?PART ?OBJ1)
(
part
?PART ?OBJ2)))))
Merge.kif 9796-9803
If
an object
is
equal
to the
union
of the parts of
another object
and
a third object
,
then for all
a fourth object
the fourth object
is a
part
of
the object
if and only if
the fourth object
is a
part
of
the other object
or
the fourth object
is a
part
of
the third object
(=>
(
equal
?THING1 ?THING2)
(
forall
(?ATTR)
(<=>
(
property
?THING1 ?ATTR)
(
property
?THING2 ?ATTR))))
Merge.kif 260-265
If
an entity
is
equal
to
another entity
,
then for all
an attribute
the entity
the
attribute
the attribute
if and only if
the other entity
the
attribute
the attribute
(=>
(
equal
?THING1 ?THING2)
(
forall
(?CLASS)
(<=>
(
instance
?THING1 ?CLASS)
(
instance
?THING2 ?CLASS))))
Merge.kif 274-279
If
an entity
is
equal
to
another entity
,
then for all
a class
the entity
is an
instance
of
the class
if and only if
the other entity
is an
instance
of
the class
(=>
(
eventLocated
?PROCESS ?OBJ)
(
forall
(?SUB)
(=>
(
subProcess
?SUB ?PROCESS)
(
eventLocated
?SUB ?OBJ))))
Merge.kif 4127-4132
If
a process
is
located
at
an object
,
then for all
another process
if
the other process
is a
subprocess
of
the process
,
then
the other process
is
located
at
the object
(=>
(
exhaustiveAttribute
?CLASS @ROW)
(
forall
(?ATTR1)
(=>
(
instance
?ATTR1 ?CLASS)
(
exists
(?ATTR2)
(
and
(
inList
?ATTR2
(
ListFn
@ROW))
(
equal
?ATTR1 ?ATTR2))))))
Merge.kif 509-517
If @ROW are all the
attributes
of
another kind of attribute
,
then for all
an entity
if
the entity
is an
instance
of
another kind of attribute
,
then there exists
another entity
such that
the other entity
is a
member
of (@ROW) and
the entity
is
equal
to
the other entity
Display limited to 25 items.
Show next 25
Display limited to 25 items.
Show next 25
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