BeginFn
(=>
(
and
(
instance
?PROCESS ?PROCESS_CLASS)
(
subclass
?PROCESS_CLASS
Process
)
(
instance
?ACCESSING
AccessingWebPage
)
(
instance
?AGENT
AutonomousAgent
)
(
agent
?PROCESS ?AGENT)
(
agent
?ACCESSING ?AGENT)
(
during
?PROCESS ?ACCESSING)
(
instance
?TIMETOFIRST
TimeInterval
)
(
not
(
exists
(?PROCESS2)
(
and
(
instance
?PROCESS2 ?PROCESS_CLASS)
(
agent
?PROCESS2 ?AGENT)
(
during
?PROCESS2 ?ACCESSING)
(
before
(
BeginFn
(
WhenFn
?PROCESS2))
(
BeginFn
(
WhenFn
?PROCESS))))))
(
equal
(
BeginFn
(
WhenFn
?ACCESSING))
(
BeginFn
(
WhenFn
?TIMETOFIRST)))
(
equal
(
BeginFn
(
WhenFn
?PROCESS))
(
EndFn
(
WhenFn
?TIMETOFIRST))))
(
equal
(
TTFxFn
?PROCESS_CLASS ?ACCESSING) ?TIMETOFIRST))
UXExperimentalTerms.kif 1496-1518
If
a time interval
is an
instance
of
the time interval
_CLASS and
the time interval
_CLASS is a
subclass
of
process
and
an accessing web page
is an
instance
of
accessing web page
and
an agent
is an
instance
of
agent
and
the agent
is an
agent
of
the time interval
and
the agent
is an
agent
of
the accessing web page
and
the time interval
takes place
during
the accessing web page
and
a physical
is an
instance
of
time interval
and there doesn't exist
the time interval
2 such that
the time interval
2 is an
instance
of
the time interval
_CLASS and
the agent
is an
agent
of
the time interval
2 and
the time interval
2 takes place
during
the accessing web page
and the
beginning
of the
time
of existence of
the time interval
2 happens
before
the
beginning
of the
time
of existence of
the time interval
and the
beginning
of the
time
of existence of
the accessing web page
is
equal
to the
beginning
of the
time
of existence of
the physical
and the
beginning
of the
time
of existence of
the time interval
is
equal
to the
end
of the
time
of existence of
the physical
,
then the
time
of
the accessing web page
in the class
the time interval
_CLASS is
equal
to
the physical
(=>
(
and
(
instance
?R
ChemicalReduction
)
(
patient
?R ?S)
(
holdsDuring
(
BeginFn
(
WhenFn
?R))
(
electronNumber
?S ?L)))
(
exists
(?G)
(
and
(
greaterThan
?G ?L)
(
holdsDuring
(
EndFn
(
WhenFn
?R))
(
electronNumber
?S ?G)))))
Mid-level-ontology.kif 19565-19577
If
a process
is an
instance
of
chemical reduction
and
an entity
is a
patient
of
the process
and
a real number
is an
electron
number of
the entity
holds
during
the
beginning
of the
time
of existence of
the process
,
then there exists
another real number
such that
the other real number
is
greater
than
the real number
and
the other real number
is an
electron
number of
the entity
holds
during
the
end
of the
time
of existence of
the process
(=>
(
and
(
instance
?REVERSE
Reversing
)
(
patient
?REVERSE ?OBJ)
(
holdsDuring
(
BeginFn
(
WhenFn
?REVERSE))
(
and
(
top
?TOP ?OBJ)
(
bottom
?BOTTOM ?OBJ))))
(
holdsDuring
(
EndFn
(
WhenFn
?REVERSE))
(
and
(
top
?BOTTOM ?OBJ)
(
bottom
?TOP ?OBJ))))
Mid-level-ontology.kif 17517-17522
If
a process
is an
instance
of
reversing
and
an entity
is a
patient
of
the process
and the
top
of
the entity
is
another entity
and the
bottom
of
the entity
is
a third entity
holds
during
the
beginning
of the
time
of existence of
the process
,
then the
top
of
the entity
is
the third entity
and the
bottom
of
the entity
is
the other entity
holds
during
the
end
of the
time
of existence of
the process
(=>
(
and
(
instance
?TI
TimeInterval
)
(
equal
?S
(
BeginFn
?TI))
(
equal
?E
(
EndFn
?TI)))
(
before
?S ?E))
Merge.kif 8262-8267
If
a time interval
is an
instance
of
time interval
and
a time point
is
equal
to the
beginning
of
the time interval
and
another time point
is
equal
to the
end
of
the time interval
,
then
the time point
happens
before
the other time point
(=>
(
and
(
instance
?TI1
TimeInterval
)
(
instance
?TI2
TimeInterval
)
(
beforeOrEqual
(
BeginFn
?TI2)
(
BeginFn
?TI1))
(
before
(
BeginFn
?TI1)
(
EndFn
?TI2)))
(
overlapsTemporally
?TI2 ?TI1))
Merge.kif 8269-8279
If
a time interval
is an
instance
of
time interval
and
another time interval
is an
instance
of
time interval
and the
beginning
of
the other time interval
happen
s before or at the
beginning
of
the time interval
and the
beginning
of
the time interval
happens
before
the
end
of
the other time interval
,
then
the time interval
overlap
s
the other time interval
(=>
(
and
(
instance
?Y1
(
YearFn
?N1))
(
instance
?Y2
(
YearFn
?N2))
(
equal
?T1
(
BeginFn
?Y1))
(
equal
?T2
(
BeginFn
?Y2))
(
greaterThan
?N2 ?N1))
(
before
?T1 ?T2))
Merge.kif 8690-8697
If
a time interval
is an
instance
of the
year
an integer
and
another time interval
is an
instance
of the
year
another integer
and
a time point
is
equal
to the
beginning
of
the time interval
and
another time point
is
equal
to the
beginning
of
the other time interval
and
the other integer
is
greater
than
the integer
,
then
the time point
happens
before
the other time point
(=>
(
and
(
muscleInsertion
?MC ?BPC)
(
instance
?H
Human
)
(
holdsDuring
?T
(
attribute
?H
StandardAnatomicalPosition
))
(
attribute
?H
Healthy
)
(
instance
?C
MuscularContraction
)
(
during
(
WhenFn
?C) ?T)
(
instance
?M ?MC)
(
part
?M ?H)
(
instrument
?C ?M)
(
physicalEnd
?E ?M)
(
meetsSpatially
?E ?BP)
(
holdsDuring
(
BeginFn
?C)
(
located
?E ?L)))
(
holdsDuring
(
EndFn
?C)
(
not
(
located
?E ?L))))
Anatomy.kif 1758-1780
If the
insertion
point of
a kind of muscle
is
a kind of body part
and
an object
is an
instance
of
human
and
standard anatomical position
is an
attribute
of
the object
holds
during
a time interval
and
healthy
is an
attribute
of
the object
and
another time interval
is an
instance
of
muscular contraction
and the
time
of existence of
the other time interval
takes place
during
the time interval
and
another object
is an
instance
of
a kind of muscle
and
the other object
is a
part
of
the object
and
the other object
is an
instrument
for
the other time interval
and one end of
the other object
is
a third object
and
the third object
meet
s
a fourth object
and
the third object
is
located
at
an entity
holds
during
the
beginning
of
the other time interval
,
then
the third object
is not
located
at
the entity
holds
during
the
end
of
the other time interval
(=>
(
and
(
muscleOrigin
?MC ?BPC)
(
instance
?H
Human
)
(
holdsDuring
?T
(
attribute
?H
StandardAnatomicalPosition
))
(
attribute
?H
Healthy
)
(
instance
?C
MuscularContraction
)
(
during
(
WhenFn
?C) ?T)
(
instance
?M ?MC)
(
part
?M ?H)
(
instrument
?C ?M)
(
physicalEnd
?E ?M)
(
meetsSpatially
?E ?BP)
(
holdsDuring
(
BeginFn
?C)
(
located
?E ?L)))
(
holdsDuring
(
EndFn
?C)
(
located
?E ?L)))
Anatomy.kif 1708-1729
If the
origin
of
a kind of muscle
is
a kind of body part
and
an object
is an
instance
of
human
and
standard anatomical position
is an
attribute
of
the object
holds
during
a time interval
and
healthy
is an
attribute
of
the object
and
another time interval
is an
instance
of
muscular contraction
and the
time
of existence of
the other time interval
takes place
during
the time interval
and
another object
is an
instance
of
a kind of muscle
and
the other object
is a
part
of
the object
and
the other object
is an
instrument
for
the other time interval
and one end of
the other object
is
a third object
and
the third object
meet
s
a fourth object
and
the third object
is
located
at
an entity
holds
during
the
beginning
of
the other time interval
,
then
the third object
is
located
at
the entity
holds
during
the
end
of
the other time interval
(=>
(
and
(
patient
?PROCESS ?PATIENT)
(
time
?PATIENT
(
EndFn
(
WhenFn
?PROCESS)))
(
not
(
time
?PATIENT
(
BeginFn
(
WhenFn
?PROCESS)))))
(
instance
?PROCESS
Creation
))
Merge.kif 12804-12810
If
a physical
is a
patient
of
a 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
,
then
the process
is an
instance
of
creation
(=>
(
and
(
property
?Option
Option
)
(
optionHolder
?Option ?Agent)
(
strikePrice
?Option ?Price)
(
agreementExpirationDate
?Option ?ExpDate)
(
price
?Stocks ?Price ?Time)
(
instance
?Time
TimeInterval
)
(
before
(
EndFn
?Time)
(
BeginFn
?ExpDate))
(
underlier
?Option ?Stocks))
(
holdsRight
(
KappaFn
?Sell
(
and
(
instance
?Sell
Selling
)
(
patient
?Sell ?Stocks)
(
time
?Sell ?Time)
(
measure
?Stocks
(
MeasureFn
100
ShareUnit
))
(
agent
?Sell ?Agent))) ?Agent))
FinancialOntology.kif 2669-2685
If
an agreement
the
attribute
option
and
a cognitive agent
holds
the agreement
and
a currency measure
is a
strike
price of
the agreement
and
the agreement
has
expiration
a time interval
and
a financial instrument
is
price
the currency measure
for
an agent
and
the agent
is an
instance
of
time interval
and the
end
of
the agent
happens
before
the
beginning
of
the time interval
and
the financial instrument
is an
underlier
of
the agreement
,
then
the cognitive agent
has the
right
to perform the
class
described by
a symbolic string
(=>
(
and
(
property
?Option
Option
)
(
optionHolder
?Option ?Agent)
(
strikePrice
?Option ?Price)
(
agreementExpirationDate
?Option ?ExpDate)
(
underlier
?Option ?Stocks)
(
price
?Stocks ?Price ?Time)
(
instance
?Time
TimeInterval
)
(
before
(
EndFn
?Time)
(
BeginFn
?ExpDate)))
(
holdsRight
(
KappaFn
?Buy
(
and
(
instance
?Buy
Buying
)
(
patient
?Buy ?Stocks)
(
time
?Buy ?Time)
(
measure
?Stocks
(
MeasureFn
100
ShareUnit
))
(
agent
?Buy ?Agent))) ?Agent))
FinancialOntology.kif 2623-2639
If
an agreement
the
attribute
option
and
a cognitive agent
holds
the agreement
and
a currency measure
is a
strike
price of
the agreement
and
the agreement
has
expiration
a time interval
and
a financial instrument
is an
underlier
of
the agreement
and
the financial instrument
is
price
the currency measure
for
an agent
and
the agent
is an
instance
of
time interval
and the
end
of
the agent
happens
before
the
beginning
of
the time interval
,
then
the cognitive agent
has the
right
to perform the
class
described by
a symbolic string
(=>
(
and
(
property
?Option
Option
)
(
optionSeller
?Option ?Agent)
(
strikePrice
?Option ?Price)
(
agreementExpirationDate
?Option ?ExpDate)
(
price
?Stocks ?Price ?Time)
(
instance
?Time
TimeInterval
)
(
before
(
EndFn
?Time)
(
BeginFn
?ExpDate))
(
underlier
?Option ?Stocks))
(
holdsObligation
(
KappaFn
?Buy
(
and
(
instance
?Buy
Buying
)
(
patient
?Buy ?Stocks)
(
time
?Buy ?Time)
(
measure
?Stocks
(
MeasureFn
100
ShareUnit
))
(
agent
?Buy ?Agent))) ?Agent))
FinancialOntology.kif 2687-2703
If
an agreement
the
attribute
option
and
a cognitive agent
sells
the agreement
and
a currency measure
is a
strike
price of
the agreement
and
the agreement
has
expiration
a time interval
and
a financial instrument
is
price
the currency measure
for
an agent
and
the agent
is an
instance
of
time interval
and the
end
of
the agent
happens
before
the
beginning
of
the time interval
and
the financial instrument
is an
underlier
of
the agreement
,
then
the cognitive agent
is
obliged
to perform tasks of type the
class
described by
a symbolic string
(=>
(
and
(
property
?Option
Option
)
(
optionSeller
?Option ?Seller)
(
strikePrice
?Option ?Price)
(
agreementExpirationDate
?Option ?ExpDate)
(
underlier
?Option ?Stocks)
(
price
?Stocks ?Price ?Time)
(
instance
?Time
TimeInterval
)
(
before
(
EndFn
?Time)
(
BeginFn
?ExpDate)))
(
holdsObligation
(
KappaFn
?Sell
(
and
(
instance
?Sell
Selling
)
(
patient
?Sell ?Stocks)
(
time
?Sell ?Time)
(
measure
?Stocks
(
MeasureFn
100
ShareUnit
))
(
agent
?Sell ?Agent))) ?Seller))
FinancialOntology.kif 2641-2659
If
an agreement
the
attribute
option
and
a cognitive agent
sells
the agreement
and
a currency measure
is a
strike
price of
the agreement
and
the agreement
has
expiration
a time interval
and
a financial instrument
is an
underlier
of
the agreement
and
the financial instrument
is
price
the currency measure
for
an agent
and
the agent
is an
instance
of
time interval
and the
end
of
the agent
happens
before
the
beginning
of
the time interval
,
then
the cognitive agent
is
obliged
to perform tasks of type the
class
described by
a symbolic string
(=>
(
and
(
resource
?PROC ?OBJ)
(
holdsDuring
(
BeginFn
(
WhenFn
?PROC))
(
measure
?OBJ ?QUANT1))
(
holdsDuring
(
EndFn
(
WhenFn
?PROC))
(
measure
?OBJ ?QUANT2)))
(
greaterThan
?QUANT1 ?QUANT2))
Merge.kif 8025-8030
If
an object
is a
resource
for
a process
and the
measure
of
the object
is
a real number
holds
during
the
beginning
of the
time
of existence of
the process
and the
measure
of
the object
is
another real number
holds
during
the
end
of the
time
of existence of
the process
,
then
the real number
is
greater
than
the other real number
(=>
(
and
(
transactionAmount
?Payment ?Amount)
(
date
?Payment ?Date)
(
instance
?Account
FinancialAccount
)
(
destination
?Payment
(
CurrencyFn
?Account))
(
amountDue
?Account ?Amount ?DueDate)
(
before
(
EndFn
?Date)
(
BeginFn
?DueDate)))
(
instance
?Payment
Prepayment
))
FinancialOntology.kif 834-842
If
a currency measure
is a
transaction
amount of
a financial transaction
and
date
of
the financial transaction
is
a day
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
the financial account
amount
due
the currency measure
for
a time interval
and the
end
of
the day
happens
before
the
beginning
of
the time interval
,
then
the financial transaction
is an
instance
of
prepayment
(=>
(
before
(
EndFn
?INTERVAL1)
(
BeginFn
?INTERVAL2))
(
earlier
?INTERVAL1 ?INTERVAL2))
Merge.kif 8382-8384
If the
end
of
a time interval
happens
before
the
beginning
of
another time interval
,
then
the time interval
happens
earlier
than
the other time interval
(=>
(
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
?INTERVAL1)
(
BeginFn
?INTERVAL2))
(
meetsTemporally
?INTERVAL1 ?INTERVAL2))
Merge.kif 8339-8343
If the
end
of
a time interval
is
equal
to the
beginning
of
another time interval
,
then
the time interval
meet
s
the other time interval
(=>
(
exists
(?Time1 ?Time2)
(
and
(
dependencyDelay
?Program1 ?Delay)
(
dependencyType
?Program1
ShutdownBlock
)
(
hasDependency
?Program1 ?Program2)
(
instance
?Process1
ComputerProcess
)
(
programRunning
?Process1 ?Program1)
(
instance
?Process2
ComputerProcess
)
(
programRunning
?Process2 ?Program2)
(
equal
(
WhenFn
?Process2) ?Time2)
(
finishes
?Time ?Time1)
(
equal
(
WhenFn
?Process2) ?Time2)
(
equal
(
BeginFn
?Time)
(
EndFn
?Time2))))
(
duration
?Time ?Delay))
QoSontology.kif 1270-1284
If there exist
a time interval
and
another time interval
such that
a time duration
is a
dependency
delay of
a computer program
and
shutdown block
is a
dependency
type of
the computer program
and
another computer program
has a
dependency
on
the computer program
and
a computer process
is an
instance
of
computer process
and
the computer program
is a
program
running of
the computer process
and
another computer process
is an
instance
of
computer process
and
the other computer program
is a
program
running of
the other computer process
and the
time
of existence of
the other computer process
is
equal
to
the other time interval
and
a third time interval
finish
es
the time interval
and the
time
of existence of
the other computer process
is
equal
to
the other time interval
and the
beginning
of
the third time interval
is
equal
to the
end
of
the other time interval
,
then
duration
of
the third time interval
is
the time duration
(=>
(
exists
(?Time1 ?Time2)
(
and
(
dependencyDelay
?Program1 ?Delay)
(
dependencyType
?Program1
StartupBlock
)
(
hasDependency
?Program1 ?Program2)
(
instance
?Process1
ComputerProcess
)
(
programRunning
?Process1 ?Program1)
(
instance
?Process2
ComputerProcess
)
(
programRunning
?Process2 ?Program2)
(
equal
(
WhenFn
?Process2) ?Time2)
(
starts
?Time2 ?Time)
(
equal
(
WhenFn
?Process1) ?Time1)
(
equal
(
EndFn
?Time)
(
BeginFn
?Time1))))
(
duration
?Time ?Delay))
QoSontology.kif 1254-1268
If there exist
a time interval
and
another time interval
such that
a time duration
is a
dependency
delay of
a computer program
and
startup block
is a
dependency
type of
the computer program
and
another computer program
has a
dependency
on
the computer program
and
a computer process
is an
instance
of
computer process
and
the computer program
is a
program
running of
the computer process
and
another computer process
is an
instance
of
computer process
and
the other computer program
is a
program
running of
the other computer process
and the
time
of existence of
the other computer process
is
equal
to
the other time interval
and
the other time interval
start
s
a third time interval
and the
time
of existence of
the computer process
is
equal
to
the time interval
and the
end
of
the third time interval
is
equal
to the
beginning
of
the time interval
,
then
duration
of
the third time interval
is
the time duration
(=>
(
temporallyBetweenOrEqual
(
BeginFn
(
WhenFn
?PHYS)) ?TIME
(
EndFn
(
WhenFn
?PHYS)))
(
and
(
time
?PHYS ?TIME)
(
instance
?TIME
TimePoint
)))
Merge.kif 8212-8221
If
a time point
is
between
or at the
beginning
of the
time
of existence of
a physical
and the
end
of the
time
of existence of
the physical
,
then
the physical
exists
during
the time point
and
the time point
is an
instance
of
time point
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