equal
(<=>
(
stringConcatenation
?S1 ?S2 ?S3)
(
equal
?S3
(
StringConcatenateFn
?S1 ?S2)))
Mid-level-ontology.kif 24496-24498
The
concatenation
of
a symbolic string
and
another symbolic string
is
a third symbolic string
if and only if
the third symbolic string
is
equal
to the
concatenation
of
the symbolic string
and
the other symbolic string
(<=>
(
stringLength
?INT ?STRING)
(
equal
?INT
(
StringLengthFn
?STRING)))
Mid-level-ontology.kif 24466-24468
A symbolic string
is
a nonnegative integer
characters
long
if and only if
the nonnegative integer
is
equal
to the
length
of
the symbolic string
(=>
(<=>
(
element
?ELEMENT ?SET1)
(
element
?ELEMENT ?SET2))
(
equal
?SET1 ?SET2))
Merge.kif 5421-5425
If
an entity
is an
element
of
a set
if and only if
the entity
is an
element
of
another set
,
then
the set
is
equal
to
the other set
(=>
(
and
(
amount
?S ?CO
(
MeasureFn
?N ?U))
(
instance
?SI ?S)
(
measure
?SI
(
MeasureFn
?N2 ?U))
(
part
?SI ?CO))
(
exists
(?L)
(
and
(
inList
(
MeasureFn
?N2 ?U) ?L)
(
equal
?L
(
AmountsFn
?S ?CO ?U))
(
equal
?N
(
ListSumFn
?L)))))
Merge.kif 7596-7611
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
(=>
(
and
(
applicableRelation
?O ?R)
(
instance
?O ?OC)
(
domain
?R 1 ?DC))
(
or
(
equal
?OC ?DC)
(
subclass
?OC ?DC)))
Mid-level-ontology.kif 31387-31394
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
(=>
(
and
(
approximateDiameter
?O
(
MeasureFn
?L ?LM))
(
sphereRadius
?S
(
MeasureFn
(
DivisionFn
?L 2.0) ?LM))
(
measure
?S
(
MeasureFn
?V1 ?VM))
(
measure
?O
(
MeasureFn
?V2 ?VM))
(
instance
?LM
UnitOfLength
)
(
instance
?VM
UnitOfVolume
))
(
equal
?V1 ?V2))
Mid-level-ontology.kif 17948-17959
If the
approximate
diameter
of
a self connected object
is
a real number
the real number
M(s) and the
radius
of
an object
is
the real number
and 2.0
the real number
M(s) and the
measure
of
the object
is
another real number
another unit of measure
(s) and the
measure
of
the self connected object
is
a third real number
the other unit of measure
(s) and
the real number
M is an
instance
of
unit of length
and
the other unit of measure
is an
instance
of
unit of volume
,
then
the other real number
is
equal
to
the third real number
(=>
(
and
(
attribute
?A
AppraisalAsJustTreatment
)
(
instance
?AJT
AppraisalProcess
)
(
agent
?AJT ?A))
(
exists
(?P ?A2)
(
and
(
instance
?P
Process
)
(
refers
?AJT ?P)
(
agent
?P ?A2)
(
not
(
equal
?A ?A2))
(
patient
?P ?A)
(
wants
?A ?P))))
emotion.kif 374-387
If
appraisal as just treatment
is an
attribute
of
a cognitive agent
and
the cognitive agent
JT is an
instance
of
appraisal process
and
the cognitive agent
is an
agent
of
the cognitive agent
JT,
then there exist
another process
and
the cognitive agent
2 such that
the other process
is an
instance
of
process
and
the cognitive agent
JT includes a
reference
to
the other process
and
the cognitive agent
2 is an
agent
of
the other process
and
the cognitive agent
is not
equal
to
the cognitive agent
2 and
the cognitive agent
is a
patient
of
the other process
and
the cognitive agent
want
s
the other process
(=>
(
and
(
attribute
?A
AppraisalAsUnjustTreatment
)
(
instance
?AUJ
AppraisalProcess
)
(
agent
?AUJ ?A))
(
exists
(?P ?A2)
(
and
(
instance
?P
Process
)
(
refers
?AUJ ?P)
(
agent
?P ?A2)
(
not
(
equal
?A ?A2))
(
patient
?P ?A)
(
not
(
wants
?A ?P)))))
emotion.kif 349-363
If
appraisal as unjust treatment
is an
attribute
of
a cognitive agent
and
the cognitive agent
UJ is an
instance
of
appraisal process
and
the cognitive agent
is an
agent
of
the cognitive agent
UJ,
then there exist
another process
and
the cognitive agent
2 such that
the other process
is an
instance
of
process
and
the cognitive agent
UJ includes a
reference
to
the other process
and
the cognitive agent
2 is an
agent
of
the other process
and
the cognitive agent
is not
equal
to
the cognitive agent
2 and
the cognitive agent
is a
patient
of
the other process
and
the cognitive agent
doesn't
want
the other process
(=>
(
and
(
attribute
?C
Collectible
)
(
hasPurpose
?C ?P))
(
exists
(?H ?P2)
(
and
(
instance
?H
Human
)
(
wants
?H ?C)
(
desires
?H ?P2)
(
entails
?P2
(
possesses
?H ?C))
(
not
(
equal
?P ?P2)))))
Mid-level-ontology.kif 29507-29519
If
Collectible
is an
attribute
of
an object
and
the object
has the purpose
a formula
,
then there exist
a cognitive agent
and
the formula
2 such that
the cognitive agent
is an
instance
of
human
and
the cognitive agent
want
s
the object
and
the cognitive agent
desire
s
the formula
2 and
the formula
2
entail
s
the cognitive agent
possess
es
the object
and
the formula
is not
equal
to
the formula
2
(=>
(
and
(
attribute
?M
MashupRecording
)
(
instance
?M
Recording
))
(
exists
(?M1 ?M2 ?S1 ?S2)
(
and
(
musicInterpretation
?M1 ?S1)
(
musicInterpretation
?M2 ?S2)
(
not
(
equal
?S1 ?S2))
(
part
?M1 ?M)
(
part
?M2 ?M))))
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
(=>
(
and
(
attribute
?M
RemixRecording
)
(
instance
?M
MusicRecording
))
(
exists
(?O ?A)
(
equal
?M
(
RemixFn
?O ?A))))
Music.kif 444-449
If
remix recording
is an
attribute
of
a music recording
and
the music recording
is an
instance
of
music recording
,
then there exist
another music recording
and
a cognitive agent
such that
the music recording
is
equal
to the
remix
of
the other music recording
by
the cognitive agent
(=>
(
and
(
attribute
?MR
CoverRecording
)
(
instance
?MR
MusicRecording
)
(
songArtist
?MR ?A)
(
musicInterpretation
?MR ?M)
(
record
?MR ?MM))
(
exists
(?ORIG ?ARTIST ?MUSIC)
(
and
(
musicInterpretation
?ORIG ?M)
(
songArtist
?ORIG ?ARTIST)
(
not
(
equal
?A ?ARTIST))
(
record
?ORIG ?MUSIC)
(
before
(
WhenFn
?MUSIC)
(
WhenFn
?MM)))))
Music.kif 457-470
If
cover recording
is an
attribute
of
a music recording
and
the music recording
is an
instance
of
music recording
and
a cognitive agent
is the
performer
in
the music recording
and
the music recording
is a
recording
of
a music
and
the music recording
is a
record
of
the music
M,
then there exist
another music recording
,
the cognitive agent
RTIST and
the music
USIC such that
the other music recording
is a
recording
of
the music
and
the cognitive agent
RTIST is the
performer
in
the other music recording
and
the cognitive agent
is not
equal
to
the cognitive agent
RTIST and
the other music recording
is a
record
of
the music
USIC and the
time
of existence of
the music
USIC happens
before
the
time
of existence of
the music
M
(=>
(
and
(
attribute
?ORG
UnicameralLegislature
)
(
legislativeBranch
?ORG ?AREA)
(
instance
?CHAMBER1
LegislativeChamber
)
(
subOrganization
?CHAMBER1
(
GovernmentFn
?AREA))
(
instance
?CHAMBER2
LegislativeChamber
)
(
subOrganization
?CHAMBER2
(
GovernmentFn
?AREA)))
(
equal
?CHAMBER1 ?CHAMBER2))
Government.kif 1977-1985
If
unicameral legislature
is an
attribute
of
an organization
and
a geopolitical area
is a
legislative
branch of
the organization
and
another organization
is an
instance
of
legislative chamber
and
the other organization
is a part of the organization the
government
of
the geopolitical area
and
a third organization
is an
instance
of
legislative chamber
and
the third organization
is a part of the organization the
government
of
the geopolitical area
,
then
the other organization
is
equal
to
the third organization
(=>
(
and
(
attribute
?Order
FOKOrder
)
(
agreementPeriod
?Order ?Period))
(
or
(
exists
(?Fill ?Time1)
(
and
(
instance
?Fill
FillingAnOrder
)
(
patient
?Fill ?Order)
(
equal
(
WhenFn
?Fill) ?Time1)
(
starts
?Time1 ?Period)))
(
exists
(?Kill ?Time2)
(
and
(
instance
?Kill
CancellingAnOrder
)
(
patient
?Kill ?Order)
(
equal
(
WhenFn
?Kill) ?Time2)
(
starts
?Time2 ?Period)))))
FinancialOntology.kif 2881-2897
If
FOK order
is an
attribute
of
an agreement
and
a time interval
is an
agreement
period of
the agreement
,
then there exist
a process
and
another time interval
such that
the process
is an
instance
of
filling an order
and
the agreement
is a
patient
of
the process
and the
time
of existence of
the process
is
equal
to
the other time interval
and
the other time interval
start
s
the time interval
or there exist
another process
and
a third time interval
such that
the other process
is an
instance
of
cancelling an order
and
the agreement
is a
patient
of
the other process
and the
time
of existence of
the other process
is
equal
to
the third time interval
and
the third time interval
start
s
the time interval
(=>
(
and
(
attribute
?Order
GTCOrder
)
(
agreementPeriod
?Order ?Period))
(
or
(
exists
(?Execute ?Time)
(
and
(
instance
?Execute
FillingAnOrder
)
(
patient
?Execute ?Order)
(
equal
(
WhenFn
?Execute) ?Time)
(
overlapsTemporally
?Time ?Period)))
(
exists
(?Cancel ?End)
(
and
(
instance
?Cancel
CancellingAnOrder
)
(
patient
?Cancel ?Order)
(
equal
(
WhenFn
?Cancel) ?End)
(
finishes
?End ?Period)))))
FinancialOntology.kif 2917-2933
If
GTC order
is an
attribute
of
an agreement
and
a time interval
is an
agreement
period of
the agreement
,
then there exist
a process
and
another time interval
such that
the process
is an
instance
of
filling an order
and
the agreement
is a
patient
of
the process
and the
time
of existence of
the process
is
equal
to
the other time interval
and
the time interval
overlap
s
the other time interval
or there exist
another process
and
a third time interval
such that
the other process
is an
instance
of
cancelling an order
and
the agreement
is a
patient
of
the other process
and the
time
of existence of
the other process
is
equal
to
the third time interval
and
the third time interval
finish
es
the time interval
(=>
(
and
(
attribute
?Order
IOCOrder
)
(
agreementPeriod
?Order ?Period))
(
or
(
exists
(?Fill ?Time1)
(
and
(
instance
?Fill
FillingAnOrder
)
(
patient
?Fill ?Order)
(
equal
(
WhenFn
?Fill) ?Time1)
(
starts
?Time1 ?Period)))
(
exists
(?Kill ?Time2)
(
and
(
instance
?Kill
CancellingAnOrder
)
(
patient
?Kill ?Order)
(
equal
(
WhenFn
?Kill) ?Time2)
(
starts
?Time2 ?Period)))))
FinancialOntology.kif 2854-2870
If
IOC order
is an
attribute
of
an agreement
and
a time interval
is an
agreement
period of
the agreement
,
then there exist
a process
and
another time interval
such that
the process
is an
instance
of
filling an order
and
the agreement
is a
patient
of
the process
and the
time
of existence of
the process
is
equal
to
the other time interval
and
the other time interval
start
s
the time interval
or there exist
another process
and
a third time interval
such that
the other process
is an
instance
of
cancelling an order
and
the agreement
is a
patient
of
the other process
and the
time
of existence of
the other process
is
equal
to
the third time interval
and
the third time interval
start
s
the time interval
(=>
(
and
(
attribute
?Order
LimitOrder
)
(
partyToAgreement
?Order ?Broker)
(
attribute
?Broker
Broker
)
(
orderFor
?Order
Buying
?Object)
(
measure
?Object ?Quantity)
(
limitPrice
?Order
(
MeasureFn
?LimitPrice ?U))
(
instance
?U
UnitOfCurrency
)
(
askPrice
?Object
(
MeasureFn
?Price ?U) ?Time)
(
lessThanOrEqualTo
?Price ?LimitPrice))
(
holdsObligation
(
KappaFn
?Buy
(
and
(
instance
?Buy
Buying
)
(
patient
?Buy ?Object)
(
measure
?Object ?Quantity)
(
equal
(
WhenFn
?Buy) ?BuyingTime)
(
overlapsTemporally
?Time ?BuyingTime))) ?Broker))
FinancialOntology.kif 2008-2029
If
limit order
is an
attribute
of
a financial transaction
and
an agreement
is a
party
to agreement of
the financial transaction
and
broker
is an
attribute
of
the agreement
and
the financial transaction
is
order
for
buying
for
a security
and the
measure
of
the security
is
a physical quantity
and
a real number
an unit of measure
(s) is a
limit
price of
the financial transaction
and
the unit of measure
is an
instance
of
unit of currency
and
an agent
asks
for
another real number
the unit of measure
(s) for
the security
and
the other real number
is
less
than or equal to
the real number
,
then
the agreement
is
obliged
to perform tasks of type the
class
described by
a symbolic string
(=>
(
and
(
attribute
?Order
LimitOrder
)
(
partyToAgreement
?Order ?Broker)
(
attribute
?Broker
Broker
)
(
orderFor
?Order
Selling
?Object)
(
measure
?Object ?Quantity)
(
limitPrice
?Order
(
MeasureFn
?LimitPrice ?U))
(
bidPrice
?Object
(
MeasureFn
?Price ?U) ?Time)
(
instance
?U
UnitOfCurrency
)
(
greaterThanOrEqualTo
?Price ?LimitPrice))
(
holdsObligation
(
KappaFn
?Sell
(
and
(
instance
?Sell
Selling
)
(
patient
?Sell ?Object)
(
measure
?Object ?Quantity)
(
equal
(
WhenFn
?Sell) ?SellingTime)
(
overlapsTemporally
?SellingTime ?Time))) ?Broker))
FinancialOntology.kif 2031-2052
If
limit order
is an
attribute
of
a financial transaction
and
an agreement
is a
party
to agreement of
the financial transaction
and
broker
is an
attribute
of
the agreement
and
the financial transaction
is
order
for
selling
for
a security
and the
measure
of
the security
is
a physical quantity
and
a real number
an unit of measure
(s) is a
limit
price of
the financial transaction
and
an agent
bids
another real number
the unit of measure
(s) for
the security
and
the unit of measure
is an
instance
of
unit of currency
and
the other real number
is
greater
than or equal to
the real number
,
then
the agreement
is
obliged
to perform tasks of type the
class
described by
a symbolic string
(=>
(
and
(
attribute
?SYLLABLE
Stressed
)
(
instance
?WORD
Word
)
(
part
?SYLLABLE ?WORD))
(
not
(
exists
(?SYLLABLE2)
(
and
(
instance
?SYLLABLE2
Syllable
)
(
part
?SYLLABLE2 ?WORD)
(
attribute
?SYLLABLE2
Stressed
)
(
not
(
equal
?SYLLABLE2 ?SYLLABLE))))))
Mid-level-ontology.kif 19443-19453
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
(=>
(
and
(
attribute
?X
CommunalAttribute
)
(
instance
?X
Table
)
(
instance
?E1
Eating
)
(
agent
?E1 ?GRP1)
(
instance
?GRP1
GroupOfPeople
)
(
eventLocated
?E1 ?X))
(
modalAttribute
(
exists
(?GRP2 ?E2 ?X2)
(
and
(
instance
?E2
Eating
)
(
agent
?E2 ?GRP2)
(
not
(
equal
?GRP1 ?GRP2))
(
instance
?GRP2
GroupOfPeople
)
(
eventLocated
?E2 ?X2)
(
meetsTemporally
(
WhenFn
?E1)
(
WhenFn
?E2))
(
equal
?X ?X2)))
Possibility
))
Dining.kif 1207-1224
If
communal
is an
attribute
of
an object
and
the object
is an
instance
of
table
and
a process
is an
instance
of
eating
and
an agent
is an
agent
of
the process
and
the agent
is an
instance
of
group of people
and
the process
is
located
at
the object
,
then the statement there exist
an entity
,
another entity
and
the object
2 such that
the other entity
is an
instance
of
eating
and
the entity
is an
agent
of
the other entity
and
the agent
is not
equal
to
the entity
and
the entity
is an
instance
of
group of people
and
the other entity
is
located
at
the object
2 and the
time
of existence of
the process
meet
s the
time
of existence of
the other entity
and
the object
is
equal
to
the object
2 has the
modal
force
of
possibility
(=>
(
and
(
attribute
?X
Multilingual
)
(
instance
?SPEAK
Speaking
)
(
agent
?SPEAK ?X))
(
modalAttribute
(
exists
(?LANG1 ?LANG2)
(
and
(
instance
?LANG1
SpokenHumanLanguage
)
(
instance
?LANG2
SpokenHumanLanguage
)
(
not
(
equal
?LANG1 ?LANG2))
(
or
(
patient
?SPEAK ?LANG1)
(
patient
?SPEAK ?LANG2))))
Possibility
))
Mid-level-ontology.kif 25748-25761
If
multilingual
is an
attribute
of
an agent
and
a process
is an
instance
of
speaking
and
the agent
is an
agent
of
the process
,
then the statement there exist
an entity
and
another entity
such that
the entity
is an
instance
of
spoken human language
and
the other entity
is an
instance
of
spoken human language
and
the entity
is not
equal
to
the other entity
and
the entity
is a
patient
of
the process
or
the other entity
is a
patient
of
the process
has the
modal
force
of
possibility
(=>
(
and
(
attribute
?X
Suite
)
(
instance
?X
HotelUnit
))
(
exists
(?R1 ?R2)
(
and
(
instance
?R1
HotelRoom
)
(
instance
?R2
HotelRoom
)
(
orientation
?R1 ?X
Inside
)
(
orientation
?R2 ?X
Inside
)
(
not
(
equal
?R1 ?R2)))))
Hotel.kif 1003-1014
If
suite
is an
attribute
of
an object
and
the object
is an
instance
of
hotel unit
,
then there exist
another object
and
a third object
such that
the other object
is an
instance
of
hotel room
and
the third object
is an
instance
of
hotel room
and
the other object
is
inside
to
the object
and
the third object
is
inside
to
the object
and
the other object
is not
equal
to
the third object
(=>
(
and
(
birthdate
?A ?DAY)
(
instance
?DAY
(
DayFn
?D
(
MonthFn
?M
(
YearFn
?Y)))))
(
exists
(?CLASS ?FUTURE)
(
and
(
birthday
?A ?CLASS)
(
subclass
?CLASS
Day
)
(
instance
?FUTURE
Integer
)
(
equal
?CLASS
(
DayFn
?D
(
MonthFn
?M
(
YearFn
?FUTURE))))
(
greaterThan
?FUTURE ?Y))))
Mid-level-ontology.kif 24236-24246
If
a day
is a
birthdate
of
a human
and
the day
is an
instance
of the
day
a positive integer
,
then there exist
another kind of day
and
an integer
such that
the human
's
birthday
is
another kind of day
and
the other kind of day
is a
subclass
of
day
and
the integer
is an
instance
of
integer
and
the other kind of day
is
equal
to the
day
the positive integer
and
the integer
is
greater
than
another integer
(=>
(
and
(
chromosomeSetCount
?SUB ?COLL ?I)
(
subCollection
?SUB ?COLL))
(
equal
?I
(
CardinalityFn
(
KappaFn
?I
(
subCollection
?SUB ?COLL)))))
VirusProteinAndCellPart.kif 829-836
If There are
an integer
number of
a monoploid chromosome set
MonoploidChromosomeSet in
Collection
a collection
. and
the monoploid chromosome set
is a proper
sub
-collection of
the collection
,
then
the integer
is
equal
to the number of
instances
in the
class
described by
the integer
(=>
(
and
(
connectedBodyPartTypes
?P1 ?P2 ?O)
(
instance
?OC ?O)
(
not
(
attribute
?H
DiseaseOrSyndrome
)))
(
exists
(?PC1 ?PC2)
(
and
(
instance
?PC1 ?P1)
(
instance
?PC2 ?P2)
(
not
(
equal
?PC1 ?PC2))
(
part
?PC1 ?OC)
(
part
?PC2 ?OC)
(
connected
?PC1 ?PC2))))
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
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