Browsing Interface
: Welcome guest :
log in
[
Home
|
Graph
| ]
KB:
SUMO
Language:
ChineseLanguage
ChineseTraditionalLanguage
ChinesehLanguage
EnglishLanguage
FrenchLanguage
GermanLanguage
JapaneseLanguage
SpanishLanguage
SwedishLanguage
Formal Language:
OWL
SUO-KIF
TPTP
traditionalLogic
KB Term:
Term intersection
English Word:
Any
Noun
Verb
Adjective
Adverb
WhenFn
Sigma KEE - WhenFn
WhenFn
appearance as argument number 1
(
documentation
WhenFn
ChineseLanguage
"这是一个
UnaryFunction
，它把一个
Object
或
Process
联系到它存在的准确
TimeInterval
。注：在
TimeInterval
(WhenFn ?THING)以外的 每一个
TimePoint
?TIME， (time ?THING ?TIME) 并不存在")
chinese_format.kif 2736-2738
(
documentation
WhenFn
EnglishLanguage
"A
UnaryFunction
that maps an
Object
or
Process
to the exact
TimeInterval
during which it exists. Note that, for every
TimePoint
?TIME outside of the
TimeInterval
(WhenFn ?THING), (time ?THING ?TIME) does not hold.")
Merge.kif 7930-7933
(
domain
WhenFn
1
Physical
)
Merge.kif 7927-7927
The number 1 argument of
when
is an
instance
of
physical
(
instance
WhenFn
TemporalRelation
)
Merge.kif 7924-7924
When
is an
instance
of
temporal relation
(
instance
WhenFn
TotalValuedRelation
)
Merge.kif 7926-7926
When
is an
instance
of
total valued relation
(
instance
WhenFn
UnaryFunction
)
Merge.kif 7925-7925
When
is an
instance
of
unary function
(
range
WhenFn
TimeInterval
)
Merge.kif 7928-7928
The
range
of
when
is an instance of
time interval
appearance as argument number 2
(
format
ChineseLanguage
WhenFn
"%1 出现 的
time
")
chinese_format.kif 455-455
(
format
EnglishLanguage
WhenFn
"the
time
of existence of %1")
english_format.kif 464-464
(
relatedInternalConcept
WhereFn
WhenFn
)
Merge.kif 4073-4073
Where
is
internally
related to
when
(
termFormat
ChineseLanguage
WhenFn
"何时")
domainEnglishFormat.kif 62893-62893
(
termFormat
ChineseLanguage
WhenFn
"何时函数")
chinese_format.kif 456-456
(
termFormat
ChineseTraditionalLanguage
WhenFn
"何時")
domainEnglishFormat.kif 62892-62892
(
termFormat
EnglishLanguage
WhenFn
"when")
domainEnglishFormat.kif 62891-62891
antecedent
(<=>
(
temporalPart
?POS
(
WhenFn
?THING))
(
time
?THING ?POS))
Merge.kif 7561-7563
A time position
is a
part
of the
time
of existence of
a physical
if and only if
the physical
exists
during
the time position
(=>
(
and
(
engineIdleSpeed
?E
(
RotationFn
?N1 ?M))
(
instance
?A
Automobile
)
(
instance
?P
GasPedal
)
(
instance
?P
Pushing
)
(
destination
?P ?GP)
(
part
?E ?A)
(
part
?GP ?A)
(
instance
?C
Crankshaft
)
(
part
?C ?E)
(
holdsDuring
(
WhenFn
?P)
(
measure
?C
(
RotationFn
?N2 ?M))))
(
modalAttribute
(
greaterThan
?N2 ?N1)
Likely
))
Cars.kif 2572-2588
If the idle speed of
an internal combustion engine
is the rotation of
a rotating
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
during
the time duration
holds
during
the
time
of existence of
the process
,
then the statement
the entity
is
greater
than
the rotating
has the
modal
force
of
likely
(=>
(
and
(
equal
?PROCESS-START
(
BeginFn
(
WhenFn
?PROCESS)))
(
equal
?AGENT-END
(
EndFn
(
WhenFn
?AGENT)))
(
benefits
?PROCESS ?AGENT))
(
before
?PROCESS-START ?AGENT-END))
Mid-level-ontology.kif 20841-20846
If
a process
-START is
equal
to the
beginning
of the
time
of existence of
the process
and
an agent
-END is
equal
to the
end
of the
time
of existence of
the agent
and
the agent
is a beneficiary of
the process
,
then
the process
-START happens
before
the agent
-END
(=>
(
and
(
equal
?PROCESS-START
(
BeginFn
(
WhenFn
?PROCESS)))
(
equal
?AGENT-END
(
EndFn
(
WhenFn
?AGENT)))
(
suffers
?PROCESS ?AGENT))
(
before
?PROCESS-START ?AGENT-END))
Mid-level-ontology.kif 27795-27804
If
a process
-START is
equal
to the
beginning
of the
time
of existence of
the process
and
an agent
-END is
equal
to the
end
of the
time
of existence of
the agent
and
the agent
suffers
from
the process
,
then
the process
-START happens
before
the agent
-END
(=>
(
and
(
holdsDuring
?T
(
attribute
?X
Booting
))
(
holdsDuring
?T2
(
attribute
?X
HostReady
))
(
equal
?T2
(
ImmediateFutureFn
(
WhenFn
?T)))
(
instance
?DIS
ComputerDisplay
)
(
connectedEngineeringComponents
?DIS ?X))
(
modalAttribute
(
exists
(?HS)
(
and
(
instance
?HS
HomeScreen
)
(
displayedUpon
?HS ?DIS)))
Likely
))
ComputingBrands.kif 3217-3231
If
booting up
is an
attribute
of
an engineering component
holds
during
a physical
and
host ready
is an
attribute
of
the engineering component
holds
during
the physical
2 and
the physical
2 is
equal
to immediately
after
the
time
of existence of
the physical
and
another engineering component
is an
instance
of
ComputerDisplay
and
the other engineering component
is
connected
to
the engineering component
,
then the statement there exists
an entity
such that
the entity
is an
instance
of
home screen
and
the entity
is
displayed
on
the other engineering component
has the
modal
force
of
likely
(=>
(
and
(
holdsDuring
?T
(
desires
?M
(
attribute
?V
Dead
)))
(
instance
?MURDER
Murder
)
(
agent
?MURDER ?M)
(
patient
?MURDER ?V)
(
earlier
?T
(
WhenFn
?MURDER)))
(
attribute
?MURDER
Premeditated
))
Law.kif 524-533
If
an agent
desire
s
dead
is an
attribute
of
an entity
holds
during
a time interval
and
the agent
URDER is an
instance
of
murder
and
the agent
is an
agent
of
the agent
URDER and
the entity
is a
patient
of
the agent
URDER and
the time interval
happens
earlier
than the
time
of existence of
the agent
URDER,
then
premeditated
is an
attribute
of
the agent
URDER
(=>
(
and
(
holdsDuring
?T1
(
attribute
?H
Dieting
))
(
holdsDuring
?T2
(
not
(
attribute
?H
Dieting
)))
(
instance
?M1
Meal
)
(
instance
?E1
Eating
)
(
agent
?E1 ?H)
(
resource
?E1 ?M1)
(
during
(
WhenFn
?E1) ?T1)
(
measure
?M1
(
MeasureFn
?C1
Calorie
))
(
instance
?M2
Meal
)
(
instance
?E2
Eating
)
(
agent
?E2 ?H)
(
resource
?E2 ?M2)
(
during
(
WhenFn
?E2) ?T2)
(
measure
?M2
(
MeasureFn
?C2
Calorie
)))
(
modalAttribute
(
greaterThan
?C2 ?C1)
Likely
))
Mid-level-ontology.kif 28831-28852
If
dieting
is an
attribute
of
an agent
holds
during
a time interval
and
dieting
is not an
attribute
of
the agent
holds
during
another time interval
and
an object
is an
instance
of
meal
and
a process
is an
instance
of
eating
and
the agent
is an
agent
of
the process
and
the object
is a
resource
for
the process
and the
time
of existence of
the process
takes place
during
the time interval
and the
measure
of
the object
is
a real number
calorie
(s) and
another object
is an
instance
of
meal
and
another process
is an
instance
of
eating
and
the agent
is an
agent
of
the other process
and
the other object
is a
resource
for
the other process
and the
time
of existence of
the other process
takes place
during
the other time interval
and the
measure
of
the other object
is
another real number
calorie
(s),
then the statement
the other real number
is
greater
than
the real number
has the
modal
force
of
likely
(=>
(
and
(
holdsDuring
?TIME
(
attribute
?ORG
Embryonic
))
(
instance
?BIRTH
Birth
)
(
equal
?BW
(
WhenFn
?BIRTH))
(
experiencer
?BIRTH ?ORG))
(
not
(
overlapsTemporally
?TIME ?BW)))
Merge.kif 16891-16897
If
embryonic
is an
attribute
of
an agent
holds
during
a time interval
and
a process
is an
instance
of
birth
and
another time interval
is
equal
to the
time
of existence of
the process
and
the agent
experience
s
the process
,
then
the other time interval
doesn't
overlap
the time interval
(=>
(
and
(
holdsDuring
?TIME
(
attribute
?ORG
Larval
))
(
instance
?BIRTH
Birth
)
(
equal
?BW
(
WhenFn
?BIRTH))
(
experiencer
?BIRTH ?ORG))
(
meetsTemporally
?BW ?TIME))
Merge.kif 16862-16868
If
larval
is an
attribute
of
an agent
holds
during
a time interval
and
a process
is an
instance
of
birth
and
another time interval
is
equal
to the
time
of existence of
the process
and
the agent
experience
s
the process
,
then
the other time interval
meet
s
the time interval
(=>
(
and
(
instance
?A
Accelerating
)
(
equal
?T
(
WhenFn
?A))
(
experiencer
?A ?E))
(
not
(
exists
(?D)
(
and
(
instance
?D
Decelerating
)
(
experiencer
?D ?E)
(
equal
?T
(
WhenFn
?D))))))
Mid-level-ontology.kif 14785-14795
If
a process
is an
instance
of
accelerating
and
a time interval
is
equal
to the
time
of existence of
the process
and
an agent
experience
s
the process
,
then there doesn't exist
another process
such that
the other process
is an
instance
of
decelerating
and
the agent
experience
s
the other process
and
the time interval
is
equal
to the
time
of existence of
the other process
(=>
(
and
(
instance
?A
Ambulating
)
(
subProcess
?S1 ?A)
(
instance
?S1
Stepping
)
(
subProcess
?S2 ?A)
(
instance
?S2
Stepping
)
(
equal
?S1-START
(
BeginFn
(
WhenFn
?S1)))
(
equal
?S2-START
(
BeginFn
(
WhenFn
?S2)))
(
not
(
or
(
before
?S1-START ?S2-START)
(
before
?S2-START ?S1-START))))
(
equal
?S1 ?S2))
Mid-level-ontology.kif 675-688
If
a process
is an
instance
of
ambulating
and
another process
is a
subprocess
of
the process
and
the other process
is an
instance
of
stepping
and
a third process
is a
subprocess
of
the process
and
the third process
is an
instance
of
stepping
and
the other process
-START is
equal
to the
beginning
of the
time
of existence of
the other process
and
the third process
-START is
equal
to the
beginning
of the
time
of existence of
the third process
and
the other process
-START happens
before
the third process
-START and
the third process
-START happens
before
the other process
-START,
then
the other process
is
equal
to
the third process
(=>
(
and
(
instance
?ACCESSING
AccessingWebPage
)
(
instance
?PAGE
WebPage
)
(
instance
?TRANSFER
DataTransfer
)
(
instance
?SERVER
Server
)
(
instance
?REQUESTING
Requesting
)
(
instance
?BROWSER
WebBrowser
)
(
instance
?INTERVAL
TimeInterval
)
(
patient
?ACCESSING ?PAGE)
(
agent
?REQUESTING ?BROWSER)
(
destination
?REQUESTING ?SERVER)
(
patient
?REQUESTING ?PAGE)
(
origin
?TRANSFER ?SERVER)
(
destination
?TRANSFER ?BROWSER)
(
patient
?TRANSFER ?PAGE)
(
subProcess
?TRANSFER ?ACCESSING)
(
subProcess
?REQUESTING ?ACCESSING)
(
equal
(
EndFn
(
WhenFn
?REQUESTING))
(
BeginFn
?INTERVAL))
(
equal
(
EndFn
(
WhenFn
?TRANSFER))
(
EndFn
?INTERVAL)))
(
equal
(
SiteSpeedFn
?ACCESSING) ?INTERVAL))
UXExperimentalTerms.kif 3961-3986
If
an AccessingWebPage
is an
instance
of
AccessingWebPage
and
an entity
is an
instance
of
WebPage
and
a process
is an
instance
of
data transfer
and
an object
is an
instance
of
server
and
another process
is an
instance
of
requesting
and
an agent
is an
instance
of
web browser
and
a time interval
is an
instance
of
time interval
and
the entity
is a
patient
of
the AccessingWebPage
and
the agent
is an
agent
of
the other process
and
the other process
end
s up at
the object
and
the entity
is a
patient
of
the other process
and
the process
originate
s at
the object
and
the process
end
s up at
the agent
and
the entity
is a
patient
of
the process
and
the process
is a
subprocess
of
the AccessingWebPage
and
the other process
is a
subprocess
of
the AccessingWebPage
and the
end
of the
time
of existence of
the other process
is
equal
to the
beginning
of
the time interval
and the
end
of the
time
of existence of
the process
is
equal
to the
end
of
the time interval
,
then the time to
access
in
the AccessingWebPage
is
equal
to
the time interval
(=>
(
and
(
instance
?AMBULATE
Ambulating
)
(
equal
?DURATION
(
WhenFn
?AMBULATE)))
(
exists
(?STEP1 ?STEPN)
(
and
(
instance
?STEP1
Stepping
)
(
instance
?STEPN
Stepping
)
(
subProcess
?STEP1 ?AMBULATE)
(
subProcess
?STEPN ?AMBULATE)
(
starts
(
WhenFn
?STEP1) ?DURATION)
(
finishes
(
WhenFn
?STEPN) ?DURATION)
(
not
(
equal
?STEP1 ?STEPN)))))
Mid-level-ontology.kif 660-672
If
a process
is an
instance
of
ambulating
and
a time interval
is
equal
to the
time
of existence of
the process
,
then there exist
another process
and
a third process
such that
the other process
is an
instance
of
stepping
and
the third process
is an
instance
of
stepping
and
the other process
is a
subprocess
of
the process
and
the third process
is a
subprocess
of
the process
and the
time
of existence of
the other process
start
s
the time interval
and the
time
of existence of
the third process
finish
es
the time interval
and
the other process
is not
equal
to
the third process
(=>
(
and
(
instance
?AR
ArmedReconnaissance
)
(
agent
?AR ?AGENT)
(
patient
?AR ?HOSTILE)
(
holdsDuring
(
WhenFn
?AR)
(
enemy
?AGENT ?HOSTILE)))
(
confersRight
(
exists
(?ATTACK)
(
and
(
instance
?ATTACK
Attack
)
(
agent
?ATTACK ?AGENT)
(
patient
?ATTACK ?HOSTILE))) ?AR ?AGENT))
MilitaryProcesses.kif 89-103
If
a process
is an
instance
of
armed reconnaissance
and
a cognitive agent
is an
agent
of
the process
and
an entity
is a
patient
of
the process
and
the cognitive agent
and
the entity
are enemies of each other holds
during
the
time
of existence of
the process
,
then
the process
allow
s
the cognitive agent
to perform task of the type there exists
another entity
such that
the other entity
is an
instance
of
attack
and
the cognitive agent
is an
agent
of
the other entity
and
the entity
is a
patient
of
the other entity
(=>
(
and
(
instance
?ASO
AntiSurfaceOperation
)
(
patient
?ASO ?TARGET)
(
holdsDuring
(
WhenFn
?ASO)
(
located
?TARGET ?LOCATION)))
(
instance
?LOCATION
WaterArea
))
MilitaryProcesses.kif 665-671
If
a process
is an
instance
of
anti ace operation
and
an entity
is a
patient
of
the process
and
the entity
is
located
at
another entity
holds
during
the
time
of existence of
the process
,
then
the other entity
is an
instance
of
water area
(=>
(
and
(
instance
?BOILING
Boiling
)
(
boilingPoint
?TYPE
(
MeasureFn
?TEMP1 ?MEASURE))
(
instance
?SUBSTANCE ?TYPE)
(
patient
?BOILING ?SUBSTANCE)
(
holdsDuring
(
WhenFn
?BOILING)
(
measure
?SUBSTANCE
(
MeasureFn
?TEMP2 ?MEASURE)))
(
instance
?MEASURE
UnitOfTemperature
))
(
greaterThanOrEqualTo
?TEMP2 ?TEMP1))
Merge.kif 12817-12825
If
a process
is an
instance
of
boiling
and
a real number
an unit of measure
(s) is a
boiling
point of
a kind of pure substance
and
an entity
is an
instance
of
a kind of pure substance
and
the entity
is a
patient
of
the process
and the
measure
of
the entity
is
a quantity
the unit of measure
(s) holds
during
the
time
of existence of
the process
and
the unit of measure
is an
instance
of
UnitOfTemperature
,
then
the quantity
is
greater
than or equal to
the real number
(=>
(
and
(
instance
?CHANGE
ChangeOfPossession
)
(
patient
?CHANGE ?OBJ)
(
holdsDuring
(
BeginFn
(
WhenFn
?CHANGE))
(
possesses
?AGENT1 ?OBJ))
(
holdsDuring
(
EndFn
(
WhenFn
?CHANGE))
(
possesses
?AGENT2 ?OBJ)))
(
not
(
equal
?AGENT1 ?AGENT2)))
Merge.kif 10867-10874
If
a process
is an
instance
of
change of possession
and
an entity
is a
patient
of
the process
and
another entity
possess
es
the entity
holds
during
the
beginning
of the
time
of existence of
the process
and
a third entity
possess
es
the entity
holds
during
the
end
of the
time
of existence of
the process
,
then
the other entity
is not
equal
to
the third entity
(=>
(
and
(
instance
?COLL
Collection
)
(
instance
?SITE
WebSite
)
(
instance
?AGENT
Agent
)
(
instance
?LISTING
WebListing
)
(
instance
?TIME
TimePoint
)
(
listingSeller
?LISTING ?AGENT)
(
not
(
member
?LISTING ?COLL))
(
forall
(?ITEM)
(=>
(
and
(
instance
?ITEM
WebListing
)
(
member
?ITEM
(
SellersItemsFn
?AGENT ?SITE))
(
temporalPart
?TIME
(
WhenFn
?ITEM))
(
not
(
equal
?ITEM ?LISTING)))
(
member
?ITEM ?COLL)))
(
forall
(?MEMBER)
(=>
(
member
?MEMBER ?COLL)
(
and
(
temporalPart
?TIME
(
WhenFn
?ITEM))
(
instance
?MEMBER
WebListing
)))))
(
equal
(
SellersOtherItemsFn
?AGENT ?SITE ?LISTING ?TIME) ?COLL))
UXExperimentalTerms.kif 1226-1253
If
a collection
is an
instance
of
collection
and
a WebSite
is an
instance
of
WebSite
and
an agent
is an
instance
of
agent
and
a web listing
is an
instance
of
web listing
and
a time point
is an
instance
of
time point
and
the agent
sells
the web listing
and
the web listing
is not a
member
of
the collection
and for all
an object
if
the object
is an
instance
of
web listing
and
the object
is a
member
of items for
sale
by
the agent
at
the WebSite
and
the time point
is a
part
of the
time
of existence of
the object
and
the object
is not
equal
to
the web listing
,
then
the object
is a
member
of
the collection
and for all
another object
if
the other object
is a
member
of
the collection
,
then
the time point
is a
part
of the
time
of existence of
the object
and
the other object
is an
instance
of
web listing
,
then things for
sale
by
the agent
not listed in
the web listing
at
the WebSite
during
the time point
is
equal
to
the collection
(=>
(
and
(
instance
?CONST
(
ConstitutionFn
?COUNTRY))
(
instance
?COUNTRY
Nation
)
(
equal
?GOV
(
GovernmentFn
?COUNTRY))
(
agreementEffectiveDuring
?CONST
(
WhenFn
?GOV))
(
subProposition
?PART ?CONST)
(
containsInformation
?FORMULA ?PART))
(
holdsObligation
?FORMULA ?GOV))
Government.kif 761-769
If
a proposition
is an
instance
of the
constitution
of
a geopolitical area
and
the geopolitical area
is an
instance
of
nation
and
a government
is
equal
to
the geopolitical area
の
government
and the
time
of existence of
the government
is an
agreement
effective during of
the proposition
and
another proposition
is a
sub
-proposition of
the proposition
and
a formula
contain
s information
the other proposition
,
then
the government
is
obliged
to perform tasks of type
the formula
(=>
(
and
(
instance
?Compression
DataCompression
)
(
dataProcessed
?Compression ?Data)
(
holdsDuring
(
ImmediatePastFn
(
WhenFn
?Compression))
(
memorySize
?Data
(
MeasureFn
?Memory ?Measure)))
(
holdsDuring
(
ImmediateFutureFn
(
WhenFn
?Compression))
(
memorySize
?Data
(
MeasureFn
?NewMemory ?Measure))))
(
lessThan
?NewMemory ?Memory))
QoSontology.kif 1932-1946
If
a computer process
is an
instance
of
data compression
and
a digital data
is
processed
by
the computer process
and
the digital data
requires
a quantity
an entity
(s) holds
during
immediately
before
the
time
of existence of
the computer process
and
the digital data
requires
another quantity
the entity
(s) holds
during
immediately
after
the
time
of existence of
the computer process
,
then
the other quantity
is
less
than
the quantity
(=>
(
and
(
instance
?D
DeletingAnAccount
)
(
instance
?AC
Account
)
(
holdsDuring
(
ImmediatePastFn
(
WhenFn
?D))
(
hasAccount
?A ?AC))
(
patient
?D ?AC)
(
agent
?D ?A))
(
holdsDuring
(
ImmediateFutureFn
(
WhenFn
?D))
(
not
(
hasAccount
?A ?AC))))
ComputingBrands.kif 4486-4496
If
a process
is an
instance
of
deleting an account
and
an entity
is an
instance
of
account
and
an agent
has
account
the entity
holds
during
immediately
before
the
time
of existence of
the process
and
the entity
is a
patient
of
the process
and
the agent
is an
agent
of
the process
,
then not
the agent
has
account
the entity
holds
during
immediately
after
the
time
of existence of
the process
(=>
(
and
(
instance
?D
Dodging
)
(
agent
?D ?A)
(
equal
?DT
(
WhenFn
?D)))
(
hasPurpose
?D
(
not
(
exists
(?I)
(
and
(
or
(
meetsTemporally
?DT
(
WhenFn
?I))
(
overlapsTemporally
?DT
(
WhenFn
?I)))
(
instance
?I
Impacting
)
(
patient
?I ?A))))))
Mid-level-ontology.kif 609-622
If
a process
is an
instance
of
dodging
and
an agent
is an
agent
of
the process
and
the process
T is
equal
to the
time
of existence of
the process
,
then
the process
purpose there doesn't exist
an entity
such that
the process
T
meet
s the
time
of existence of
the entity
or the
time
of existence of
the entity
overlap
s
the process
T and
the entity
is an
instance
of
impacting
and
the agent
is a
patient
of
the entity
(=>
(
and
(
instance
?DEPOSITION
Deposition
)
(
patient
?DEPOSITION ?OBJ)
(
holdsDuring
(
ImmediatePastFn
(
WhenFn
?DEPOSITION))
(
measure
?OBJ
(
MeasureFn
?X
Joule
)))
(
holdsDuring
(
ImmediateFutureFn
(
WhenFn
?DEPOSITION))
(
measure
?OBJ
(
MeasureFn
?Y
Joule
))))
(
lessThan
?Y ?X))
Geography.kif 6354-6368
If
a process
is an
instance
of
deposition
and
an entity
is a
patient
of
the process
and the
measure
of
the entity
is
a quantity
joule
(s) holds
during
immediately
before
the
time
of existence of
the process
and the
measure
of
the entity
is
another quantity
joule
(s) holds
during
immediately
after
the
time
of existence of
the process
,
then
the other quantity
is
less
than
the quantity
(=>
(
and
(
instance
?DISCOVER
Discovering
)
(
patient
?DISCOVER ?OBJ)
(
holdsDuring
(
WhenFn
?DISCOVER)
(
located
?OBJ ?PLACE)))
(
exists
(?LEARN)
(
and
(
instance
?LEARN
Learning
)
(
subProcess
?LEARN ?DISCOVER)
(
patient
?LEARN
(
located
?OBJ ?PLACE)))))
Merge.kif 11167-11176
If
a process
is an
instance
of
discovering
and
an entity
is a
patient
of
the process
and
the entity
is
located
at
another entity
holds
during
the
time
of existence of
the process
,
then there exists
another process
such that
the other process
is an
instance
of
learning
and
the other process
is a
subprocess
of
the process
and
the entity
is
located
at
the other entity
is a
patient
of
the other process
(=>
(
and
(
instance
?Deposit
Deposit
)
(
instance
?Account
FinancialAccount
)
(
destination
?Deposit
(
CurrencyFn
?Account))
(
transactionAmount
?Deposit ?Amount)
(
currentAccountBalance
?Account
(
ImmediatePastFn
(
WhenFn
?Deposit)) ?Balance1)
(
equal
?Balance2
(
AdditionFn
?Balance1 ?Amount)))
(
currentAccountBalance
?Account
(
ImmediateFutureFn
(
FutureFn
?Deposit)) ?Balance2))
FinancialOntology.kif 428-436
If
a financial transaction
is an
instance
of
deposit
and
a financial account
is an
instance
of
financial account
and
the financial transaction
end
s up at the
currency
of
the financial account
and
a currency measure
is a
transaction
amount of
the financial transaction
and
the financial account
current
account balance immediately
before
the
time
of existence of
the financial transaction
for
another currency measure
and
a third currency measure
is
equal
to (
the other currency measure
and
the currency measure
),
then
the financial account
current
account balance immediately
after
after
the financial transaction
for
the third currency measure
Display limited to 25 items.
Show next 25
Display limited to 25 items.
Show next 25
consequent
(<=>
(
and
(
instance
?COMBINE
Combining
)
(
resource
?COMBINE ?OBJ1)
(
result
?COMBINE ?OBJ2))
(
and
(
holdsDuring
(
BeginFn
(
WhenFn
?COMBINE))
(
not
(
part
?OBJ1 ?OBJ2)))
(
holdsDuring
(
EndFn
(
WhenFn
?COMBINE))
(
part
?OBJ1 ?OBJ2))))
Merge.kif 11550-11557
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
(<=>
(
and
(
time
?PHYS ?TIME)
(
instance
?TIME
TimePoint
))
(
temporallyBetweenOrEqual
(
BeginFn
(
WhenFn
?PHYS)) ?TIME
(
EndFn
(
WhenFn
?PHYS))))
Merge.kif 7754-7758
A physical
exists
during
a time point
and
the time point
is an
instance
of
time point
if and only if
the time point
is
between
or at the
beginning
of the
time
of existence of
the physical
and the
end
of the
time
of existence of
the physical
(<=>
(
cooccur
?PHYS1 ?PHYS2)
(
equal
(
WhenFn
?PHYS1)
(
WhenFn
?PHYS2)))
Merge.kif 7861-7863
A physical
occur
s at the same time as
another physical
if and only if the
time
of existence of
the physical
is
equal
to the
time
of existence of
the other physical
(<=>
(
equal
(
BirthsPerThousandFn
?AREA
(
YearFn
?YEAR)) ?REALNUMBER)
(
and
(
equal
(
DivisionFn
(
PopulationFn
?AREA) 1000) ?THOUSANDS)
(
equal
?BIRTHCOUNT
(
CardinalityFn
(
KappaFn
?BIRTH
(
and
(
instance
?BIRTH
Birth
)
(
experiencer
?BIRTH ?INFANT)
(
instance
?INFANT
Human
)
(
during
(
WhenFn
?BIRTH)
(
YearFn
?YEAR))
(
equal
(
WhereFn
?BIRTH
(
WhenFn
?BIRTH)) ?AREA)))))
(
equal
(
DivisionFn
?BIRTHCOUNT ?THOUSANDS) ?REALNUMBER)))
People.kif 104-117
The
births
per thousand of
a geopolitical area
and the
year
an integer
is
equal
to
a real number
if and only if the
population
of
the geopolitical area
and 1000 is
equal
to
a quantity
and
another integer
is
equal
to the number of
instances
in the
class
described by
a symbolic string
and
the other integer
and
the quantity
is
equal
to
the real number
(<=>
(
equal
(
DeathsPerThousandFn
?AREA
(
YearFn
?YEAR)) ?REALNUMBER)
(
and
(
equal
(
DivisionFn
(
PopulationFn
?AREA) 1000) ?THOUSANDS)
(
equal
?DEATHCOUNT
(
CardinalityFn
(
KappaFn
?DEATH
(
and
(
instance
?DEATH
Death
)
(
experiencer
?DEATH ?PERSON)
(
instance
?PERSON
Human
)
(
during
(
WhenFn
?DEATH)
(
YearFn
?YEAR))
(
equal
(
WhereFn
?DEATH
(
WhenFn
?DEATH)) ?AREA)))))
(
equal
(
DivisionFn
?DEATHCOUNT ?THOUSANDS) ?REALNUMBER)))
People.kif 138-151
The
deaths
per thousand of
a geopolitical area
and the
year
an integer
is
equal
to
a real number
if and only if the
population
of
the geopolitical area
and 1000 is
equal
to
a quantity
and
another integer
is
equal
to the number of
instances
in the
class
described by
a symbolic string
and
the other integer
and
the quantity
is
equal
to
the real number
(<=>
(
equal
(
DeathsPerThousandLiveBirthsFn
?AREA
(
YearFn
?YEAR)) ?REALNUMBER)
(
and
(
equal
?BIRTHCOUNT
(
CardinalityFn
(
KappaFn
?BIRTH
(
and
(
instance
?BIRTH
Birth
)
(
experiencer
?BIRTH ?INFANT)
(
instance
?INFANT
Human
)
(
during
(
WhenFn
?BIRTH)
(
YearFn
?YEAR))
(
equal
(
WhereFn
?BIRTH
(
WhenFn
?BIRTH)) ?AREA)))))
(
equal
(
DivisionFn
?BIRTHCOUNT 1000) ?THOUSANDSOFBIRTHS)
(
equal
?INFANTDEATHCOUNT
(
CardinalityFn
(
KappaFn
?DEATH
(
and
(
instance
?DEATH
Death
)
(
experiencer
?DEATH ?INFANT)
(
instance
?INFANT
Human
)
(
age
?INFANT
(
MeasureFn
?AGE
YearDuration
))
(
lessThan
?AGE 1)
(
during
(
WhenFn
?DEATH)
(
YearFn
?YEAR))
(
equal
(
WhereFn
?DEATH
(
WhenFn
?DEATH)) ?AREA)))))
(
equal
(
DivisionFn
?INFANTDEATHCOUNT ?THOUSANDSOFBIRTHS) ?REALNUMBER)))
People.kif 253-277
The
deaths
per thousand live births of
a geopolitical area
and the
year
an integer
is
equal
to
a real number
if and only if
another integer
is
equal
to the number of
instances
in the
class
described by
a symbolic string
and
the other integer
and 1000 is
equal
to
a quantity
and
a third integer
is
equal
to the number of
instances
in the
class
described by
another symbolic string
and
the third integer
and
the quantity
is
equal
to
the real number
(<=>
(
equal
(
FemaleLifeExpectancyAtBirthFn
?AREA
(
YearFn
?YEAR)) ?REALNUMBER)
(
exists
(?LIST)
(
and
(
instance
?LIST
List
)
(
instance
(
ListLengthFn
?LIST) ?COUNT)
(
forall
(?LISTITEM)
(=>
(
inList
?LISTITEM ?LIST)
(
and
(
instance
?LISTITEM ?LIFEEXPECTANCYAGE)
(
not
(
exists
(?NUMBER)
(
and
(
instance
?NUMBER ?LIFEEXPECTANCYAGE)
(
not
(
inList
?NUMBER ?LIST)))))
(
equal
?COUNT
(
CardinalityFn
(
KappaFn
?LIFEEXPECTANCYAGE
(
and
(
instance
?BIRTH
Birth
)
(
experiencer
?BIRTH ?INDIVIDUAL)
(
instance
?INDIVIDUAL
Human
)
(
attribute
?INDIVIDUAL
Female
)
(
during
(
WhenFn
?BIRTH)
(
YearFn
?YEAR))
(
equal
(
WhereFn
?BIRTH
(
WhenFn
?BIRTH)) ?AREA)
(
instance
?DEATH
Death
)
(
experiencer
?DEATH ?INDIVIDUAL)
(
holdsDuring
(
WhenFn
?DEATH)
(
age
?INDIVIDUAL
(
MeasureFn
?LIFEEXPECTANCYAGE
YearDuration
))))))))))
(
average
?LIST ?REALNUMBER))))
People.kif 411-442
The
female
life expectancy at birth of
a geopolitical area
and the
year
an integer
is
equal
to
a real number
if and only if there exists
a list
such that
the list
is an
instance
of
list
and
length
of
the list
is an
instance
of
another integer
and for all
the list
ITEM
if
the list
ITEM is a
member
of
the list
,
then
the list
ITEM is an
instance
of
a symbolic string
and there doesn't exist
another entity
such that
the other entity
is an
instance
of
the symbolic string
and
the other entity
is not a
member
of
the list
and
the other integer
is
equal
to the number of
instances
in the
class
described by
the symbolic string
and
the real number
is an
average
of
the list
(<=>
(
equal
(
LifeExpectancyAtBirthFn
?AREA
(
YearFn
?YEAR)) ?REALNUMBER)
(
exists
(?LIST)
(
and
(
instance
?LIST
List
)
(
instance
(
ListLengthFn
?LIST) ?COUNT)
(
forall
(?LISTITEM)
(=>
(
inList
?LISTITEM ?LIST)
(
and
(
instance
?LISTITEM ?LIFEEXPECTANCYAGE)
(
not
(
exists
(?NUMBER)
(
and
(
instance
?NUMBER ?LIFEEXPECTANCYAGE)
(
not
(
inList
?NUMBER ?LIST)))))
(
equal
?COUNT
(
CardinalityFn
(
KappaFn
?LIFEEXPECTANCYAGE
(
and
(
instance
?BIRTH
Birth
)
(
experiencer
?BIRTH ?INDIVIDUAL)
(
instance
?INDIVIDUAL
Human
)
(
during
(
WhenFn
?BIRTH)
(
YearFn
?YEAR))
(
equal
(
WhereFn
?BIRTH
(
WhenFn
?BIRTH)) ?AREA)
(
instance
?DEATH
Death
)
(
experiencer
?DEATH ?INDIVIDUAL)
(
holdsDuring
(
WhenFn
?DEATH)
(
age
?INDIVIDUAL
(
MeasureFn
?LIFEEXPECTANCYAGE
YearDuration
))))))))))
(
average
?LIST ?REALNUMBER))))
People.kif 323-353
The
life
expectancy at birth of
a geopolitical area
and the
year
an integer
is
equal
to
a real number
if and only if there exists
a list
such that
the list
is an
instance
of
list
and
length
of
the list
is an
instance
of
another integer
and for all
the list
ITEM
if
the list
ITEM is a
member
of
the list
,
then
the list
ITEM is an
instance
of
a symbolic string
and there doesn't exist
another entity
such that
the other entity
is an
instance
of
the symbolic string
and
the other entity
is not a
member
of
the list
and
the other integer
is
equal
to the number of
instances
in the
class
described by
the symbolic string
and
the real number
is an
average
of
the list
(<=>
(
equal
(
MaleLifeExpectancyAtBirthFn
?AREA
(
YearFn
?YEAR)) ?REALNUMBER)
(
exists
(?LIST)
(
and
(
instance
?LIST
List
)
(
instance
(
ListLengthFn
?LIST) ?COUNT)
(
forall
(?LISTITEM)
(=>
(
inList
?LISTITEM ?LIST)
(
and
(
instance
?LISTITEM ?LIFEEXPECTANCYAGE)
(
not
(
exists
(?NUMBER)
(
and
(
instance
?NUMBER ?LIFEEXPECTANCYAGE)
(
not
(
inList
?NUMBER ?LIST)))))
(
equal
?COUNT
(
CardinalityFn
(
KappaFn
?LIFEEXPECTANCYAGE
(
and
(
instance
?BIRTH
Birth
)
(
experiencer
?BIRTH ?INDIVIDUAL)
(
instance
?INDIVIDUAL
Human
)
(
attribute
?INDIVIDUAL
Male
)
(
during
(
WhenFn
?BIRTH)
(
YearFn
?YEAR))
(
equal
(
WhereFn
?BIRTH
(
WhenFn
?BIRTH)) ?AREA)
(
instance
?DEATH
Death
)
(
experiencer
?DEATH ?INDIVIDUAL)
(
holdsDuring
(
WhenFn
?DEATH)
(
age
?INDIVIDUAL
(
MeasureFn
?LIFEEXPECTANCYAGE
YearDuration
))))))))))
(
average
?LIST ?REALNUMBER))))
People.kif 367-398
The
male
life expectancy at birth of
a geopolitical area
and the
year
an integer
is
equal
to
a real number
if and only if there exists
a list
such that
the list
is an
instance
of
list
and
length
of
the list
is an
instance
of
another integer
and for all
the list
ITEM
if
the list
ITEM is a
member
of
the list
,
then
the list
ITEM is an
instance
of
a symbolic string
and there doesn't exist
another entity
such that
the other entity
is an
instance
of
the symbolic string
and
the other entity
is not a
member
of
the list
and
the other integer
is
equal
to the number of
instances
in the
class
described by
the symbolic string
and
the real number
is an
average
of
the list
(<=>
(
holdsDuring
?T
(
attribute
?H
Alone
))
(
not
(
exists
(?H2 ?SI)
(
and
(
not
(
equal
?H ?H2))
(
instance
?H2
Agent
)
(
instance
?SI
SocialInteraction
)
(
during
(
WhenFn
?SI) ?T)
(
involvedInEvent
?SI ?H)
(
involvedInEvent
?SI ?H2)))))
Mid-level-ontology.kif 28405-28418
Alone
is an
attribute
of
an entity
holds
during
a time interval
if and only if there don't exist
the entity
2 and
a process
such that
the entity
is not
equal
to
the entity
2 and
the entity
2 is an
instance
of
agent
and
the process
is an
instance
of
social interaction
and the
time
of existence of
the process
takes place
during
the time interval
and
the entity
is an
involved
in event of
the process
and
the entity
2 is an
involved
in event of
the process
(<=>
(
holdsDuring
?T
(
attribute
?P
Mute
))
(
not
(
exists
(?S)
(
and
(
instance
?S
Speaking
)
(
during
(
WhenFn
?S) ?T)
(
agent
?S ?P)))))
Mid-level-ontology.kif 28451-28459
Mute
is an
attribute
of
an agent
holds
during
a time interval
if and only if there doesn't exist
a process
such that
the process
is an
instance
of
speaking
and the
time
of existence of
the process
takes place
during
the time interval
and
the agent
is an
agent
of
the process
(<=>
(
instance
?PROCESS
Creation
)
(
exists
(?PATIENT)
(
and
(
patient
?PROCESS ?PATIENT)
(
time
?PATIENT
(
EndFn
(
WhenFn
?PROCESS)))
(
not
(
time
?PATIENT
(
BeginFn
(
WhenFn
?PROCESS)))))))
Merge.kif 11867-11874
A process
is an
instance
of
creation
if and only if there exists
a physical
such that
the physical
is a
patient
of
the process
and
the physical
exists
during
the
end
of the
time
of existence of
the process
and
the physical
doesn't exist
during
the
beginning
of the
time
of existence of
the process
(<=>
(
instance
?PROCESS
Destruction
)
(
exists
(?PATIENT)
(
and
(
patient
?PROCESS ?PATIENT)
(
time
?PATIENT
(
BeginFn
(
WhenFn
?PROCESS)))
(
not
(
time
?PATIENT
(
EndFn
(
WhenFn
?PROCESS)))))))
Merge.kif 11415-11422
A process
is an
instance
of
destruction
if and only if there exists
a physical
such that
the physical
is a
patient
of
the process
and
the physical
exists
during
the
beginning
of the
time
of existence of
the process
and
the physical
doesn't exist
during
the
end
of the
time
of existence of
the process
(=>
(
almaMater
?PERSON ?SCHOOL)
(
exists
(?EV)
(
and
(
instance
?EV
EducationalProcess
)
(
destination
?EV ?PERSON)
(
eventLocated
?EV ?SCHOOL)
(
holdsDuring
(
WhenFn
?EV)
(
attribute
?PERSON
Student
)))))
Mid-level-ontology.kif 14434-14443
If
a human
's
almaMater
is
a post secondary school
,
then there exists
a process
such that
the process
is an
instance
of
educational process
and
the process
end
s up at
the human
and
the process
is
located
at
2
and
student
is an
attribute
of
the human
holds
during
the
time
of existence of
the process
(=>
(
and
(
Process
?WW
WaterWave
)
(
waveHeight
?WW ?WH))
(
exists
(?LIST ?WA)
(
and
(
inList
?WH ?LIST)
(
instance
?WA
WaterArea
)
(
eventLocated
?WW ?WA)
(
significantWaveHeight
?WA
(
WhenFn
?WW)
(
MeasureFn
?SWH ?U))
(
equal
?SWH
(
MultiplicationFn
4
(
StandardDeviationFn
?LIST))))))
Weather.kif 1131-1145
If
process
a water wave
and
water wave
and
wave height
the water wave
and
a length measure
,
then there exist
a list
and
a water area
such that
the length measure
is a
member
of
the list
and
the water area
is an
instance
of
water area
and
the water wave
is
located
at
2
and
significant wave height
the water area
, the
time
of existence of
the water wave
and
a real number
an unit of measure
(s) and
the real number
is
equal
to 4 and
standard deviation
the list
(=>
(
and
(
actedIn
?ACTOR ?O)
(
instance
?PERF
DramaticActing
)
(
patient
?PERF ?ACTOR)
(
result
?PERF ?O))
(
holdsDuring
(
WhenFn
?PERF)
(
attribute
?ACTOR
Actor
)))
Mid-level-ontology.kif 18442-18449
If
actedIn
a human
and
a content bearing physical
and
a process
is an
instance
of
dramatic acting
and
the human
is a
patient
of
the process
and
the content bearing physical
is a
result
of
the process
,
then
Actor
is an
attribute
of
the human
holds
during
the
time
of existence of
the process
(=>
(
and
(
agent
?PROCESS ?AGENT)
(
result
?PROCESS ?WORK)
(
instance
?WORK
ArtWork
))
(
holdsDuring
(
WhenFn
?PROCESS)
(
attribute
?AGENT
Artist
)))
Mid-level-ontology.kif 16535-16541
If
an agent
is an
agent
of
a process
and
an entity
is a
result
of
the process
and
the entity
is an
instance
of
art work
,
then
Artist
is an
attribute
of
the agent
holds
during
the
time
of existence of
the process
(=>
(
and
(
attribute
?AC
TwoFactorAuthentication
)
(
loggedInDuring
?A ?AC ?T))
(
exists
(?TF)
(
and
(
instance
?TF
TwoFactorLoggingIn
)
(
agent
?TF ?A)
(
accountUsed
?TF ?AC)
(
earlier
(
WhenFn
?TF) ?T))))
ComputingBrands.kif 4293-4302
If
two-factor authentication
is an
attribute
of
an user account
and
an agent
is logged-in to
the user account
during
a time interval
,
then there exists
the time interval
F such that
the time interval
F is an
instance
of
two-factor login
and
the agent
is an
agent
of
the time interval
F and the
accountUsed
in
the time interval
F is
the user account
and the
time
of existence of
the time interval
F happens
earlier
than
the time interval
(=>
(
and
(
attribute
?H
Muslim
)
(
equal
(
WealthFn
?H) ?W))
(
modalAttribute
(
exists
(?Z ?T)
(
and
(
instance
?Z
Zakat
)
(
instance
?Y
Year
)
(
during
?Y
(
WhenFn
?H))
(
holdsDuring
?Y
(
attribute
?H
FullyFormed
))
(
agent
?Z ?H)
(
patient
?Z ?T)
(
monetaryValue
?T ?C)
(
greaterThan
?C
(
MultiplicationFn
?W 0.025))))
Obligation
))
ArabicCulture.kif 193-210
If
muslim
is an
attribute
of
an agent
and
value
of belongings of
the agent
is
equal
to
a currency measure
,
then the statement there exist
an entity
and
another entity
such that
the entity
is an
instance
of
zakat
and
a third entity
is an
instance
of
year
and
the third entity
takes place
during
the
time
of existence of
the agent
and
fully formed
is an
attribute
of
the agent
holds
during
the third entity
and
the agent
is an
agent
of
the entity
and
the other entity
is a
patient
of
the entity
and
value
of
the other entity
is
a fourth entity
and
the fourth entity
is
greater
than
the currency measure
and 0.025 has the
modal
force
of
obligation
(=>
(
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 454-467
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
?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 2802-2818
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)
(
and
(
instance
?Execute
FillingAnOrder
)
(
patient
?Execute ?Order)
(
equal
(
WhenFn
?Execute) ?Time)
(
overlapsTemporally
?Time ?Period)))
(
exists
(?Cancel)
(
and
(
instance
?Cancel
CancellingAnOrder
)
(
patient
?Cancel ?Order)
(
equal
(
WhenFn
?Cancel) ?End)
(
finishes
?End ?Period)))))
FinancialOntology.kif 2838-2854
If
GTC order
is an
attribute
of
an agreement
and
a time interval
is an
agreement
period of
the agreement
,
then there exists
a process
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
another time interval
and
the time interval
overlap
s
the other time interval
or there exists
another process
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
a 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 2775-2791
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 ?LimitPrice)
(
askPrice
?Object ?Price ?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 1945-1963
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 currency measure
is a
limit
price of
the financial transaction
and
an agent
asks
for
another currency measure
for
the security
and
the other currency measure
is
less
than or equal to
the currency measure
,
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 ?LimitPrice)
(
bidPrice
?Object ?Price ?Time)
(
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 1965-1983
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 currency measure
is a
limit
price of
the financial transaction
and
an agent
bids
another currency measure
for
the security
and
the other currency measure
is
greater
than or equal to
the currency measure
,
then
the agreement
is
obliged
to perform tasks of type the
class
described by
a symbolic string
Display limited to 25 items.
Show next 25
Display limited to 25 items.
Show next 25
statement
(
exists
(?TIME)
(
and
(
instance
?TIME
TimeInterval
)
(
finishes
?TIME
(
WhenFn
JesusOfNazareth
))
(
starts
?TIME
(
WhenFn
TwelveApostles
))
(
forall
(?MEM)
(=>
(
holdsDuring
?TIME
(
member
?MEM
TwelveApostles
))
(
holdsDuring
?TIME
(
friend
?MEM
JesusOfNazareth
))))))
Media.kif 1972-1980
There exists
a time interval
such that
the time interval
is an
instance
of
time interval
and
the time interval
finish
es the
time
of existence of
JesusOfNazareth
and
the time interval
start
s the
time
of existence of
TwelveApostles
and for all
an entity
if
the entity
is a
member
of
TwelveApostles
holds
during
the time interval
,
then
JesusOfNazareth
is a
friend
of
the entity
holds
during
the time interval
(
holdsDuring
(
WhenFn
JesusOfNazareth
)
(
located
JesusOfNazareth
Palestine
))
Media.kif 1922-1922
JesusOfNazareth
is
located
at
palestine
holds
during
the
time
of existence of
JesusOfNazareth
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
