Browsing Interface
: Welcome guest :
log in
[
Home
| 
Graph
|  ]
KB:
SUMO
Language:
ChineseLanguage
ChinesePinyinWriting
ChineseSimplifiedWriting
ChineseTraditionalLanguage
EnglishLanguage
FrenchLanguage
GermanLanguage
HerbaceousPlant
Hindi
ItalianLanguage
JapaneseLanguage
PortugueseLanguage
SpanishLanguage
SwedishLanguage
WoodyPlant
cb
cz
de
hi
ro
sv
tg
Formal Language:
OWL
SUO-KIF
TPTP
traditionalLogic
KB Term:
Term intersection
English Word:
Any
Noun
Verb
Adjective
Adverb
exists
Sigma KEE - exists
exists
appearance as argument number 2
(
termFormat
EnglishLanguage
exists
"exists")
domainEnglishFormat.kif 65827-65827
antecedent
(<=>
(
and
(
instance
?Withdrawal
Withdrawal
)
(
instance
?Account
FinancialAccount
)
(
origin
?Withdrawal
(
CurrencyFn
?Account))
(
not
(
exists
(?Penalty)
(
and
(
instance
?Penalty
Penalty
)
(
destination
?Penalty
(
CurrencyFn
?Account))
(
causes
?Withdrawal ?Penalty)))))
(
liquidity
?Account
HighLiquidity
))
FinancialOntology.kif 1818-1828
A process
is an
instance
of
withdrawal
and
a financial account
is an
instance
of
financial account
and
the process
originate
s at the
currency
of
the financial account
and there doesn't exist
another process
such that
the other process
is an
instance
of
penalty
and
the other process
end
s up at the
currency
of
the financial account
and
the process
cause
s
the other process
if and only if the
liqudity
of
the financial account
is
high liquidity
(<=>
(
exists
(?Period)
(
and
(
instance
?Loan
Loan
)
(
agreementPeriod
?Loan ?Period)
(
interestEarned
?Loan ?Amount ?Period)))
(
loanInterest
?Loan ?Amount))
FinancialOntology.kif 3920-3926
There exists
a time interval
such that
a loan
is an
instance
of
loan
and
the time interval
is an
agreement
period of
the loan
and
the loan
is
interest
earned
an interest
for
the time interval
if and only if
the interest
is a
loan
interest of
the loan
(<=>
(
exists
(?Process)
(
programRunning
?Process ?Program))
(
property
?Program
Executable
))
QoSontology.kif 989-992
There exists
a computer process
such that
a computer program
is a
program
running of
the computer process
if and only if
the computer program
the
attribute
executable
(<=>
(
exists
(?Rate)
(
fixedInterestRate
?Account ?Rate))
(
instance
?Account
FixedRateAccount
))
FinancialOntology.kif 981-984
There exists
a number
such that
the number
is a
fixed
interest rate of
a financial account
if and only if
the financial account
is an
instance
of
fixed rate account
(<=>
(
exists
(?Stock ?StockPrice ?StrikePrice)
(
and
(
instance
?Option
CallOption
)
(
underlier
?Option ?Stock)
(
price
?Stock
(
MeasureFn
?StockPrice ?U) ?Time)
(
instance
?U
UnitOfCurrency
)
(
strikePrice
?Option
(
MeasureFn
?StrikePrice ?U))
(
lessThan
?StockPrice ?StrikePrice)))
(
outOfTheMoney
?Option ?Time))
FinancialOntology.kif 3051-3062
There exist
a financial instrument
,
the financial instrument
Price and
another real number
such that
an agreement
is an
instance
of
call option
and
the financial instrument
is an
underlier
of
the agreement
and
the financial instrument
is
price
the financial instrument
Price
an unit of measure
(s) for
an agent
and
the unit of measure
is an
instance
of
unit of currency
and
the other real number
the unit of measure
(s) is a
strike
price of
the agreement
and
the financial instrument
Price is
less
than
the other real number
if and only if
the agent
is an
out
of the money of
the agreement
(<=>
(
exists
(?Stock ?StockPrice ?StrikePrice)
(
and
(
instance
?Option
CallOption
)
(
underlier
?Option ?Stock)
(
price
?Stock
(
MeasureFn
?StockPrice ?U) ?Time)
(
instance
?U
UnitOfCurrency
)
(
strikePrice
?Option
(
MeasureFn
?StrikePrice ?U))
(
lessThan
?StrikePrice ?StockPrice)))
(
inTheMoney
?Option ?Time))
FinancialOntology.kif 3002-3013
There exist
a financial instrument
,
the financial instrument
Price and
another real number
such that
an agreement
is an
instance
of
call option
and
the financial instrument
is an
underlier
of
the agreement
and
the financial instrument
is
price
the financial instrument
Price
an unit of measure
(s) for
an agent
and
the unit of measure
is an
instance
of
unit of currency
and
the other real number
the unit of measure
(s) is a
strike
price of
the agreement
and
the other real number
is
less
than
the financial instrument
Price if and only if
the agent
is an
in
the money of
the agreement
(<=>
(
exists
(?Stock ?StockPrice ?StrikePrice)
(
and
(
instance
?Option
Option
)
(
underlier
?Option ?Stock)
(
price
?Stock ?StockPrice ?Time)
(
strikePrice
?Option ?StrikePrice)
(
equal
?StockPrice ?StrikePrice)))
(
atTheMoney
?Option ?Time))
FinancialOntology.kif 3034-3042
There exist
a financial instrument
,
the financial instrument
Price and
another currency measure
such that
an agreement
is an
instance
of
option
and
the financial instrument
is an
underlier
of
the agreement
and
the financial instrument
is
price
the financial instrument
Price for
an agent
and
the other currency measure
is a
strike
price of
the agreement
and
the financial instrument
Price is
equal
to
the other currency measure
if and only if
the agent
is an
at
the money of
the agreement
(<=>
(
exists
(?Stock ?StockPrice ?StrikePrice)
(
and
(
instance
?Option
PutOption
)
(
underlier
?Option ?Stock)
(
price
?Stock
(
MeasureFn
?StockPrice ?U) ?Time)
(
instance
?U
UnitOfCurrency
)
(
strikePrice
?Option
(
MeasureFn
?StrikePrice ?U))
(
lessThan
?StockPrice ?StrikePrice)))
(
inTheMoney
?Option ?Time))
FinancialOntology.kif 3015-3026
There exist
a financial instrument
,
the financial instrument
Price and
another real number
such that
an agreement
is an
instance
of
put option
and
the financial instrument
is an
underlier
of
the agreement
and
the financial instrument
is
price
the financial instrument
Price
an unit of measure
(s) for
an agent
and
the unit of measure
is an
instance
of
unit of currency
and
the other real number
the unit of measure
(s) is a
strike
price of
the agreement
and
the financial instrument
Price is
less
than
the other real number
if and only if
the agent
is an
in
the money of
the agreement
(<=>
(
exists
(?Stock ?StockPrice ?StrikePrice)
(
and
(
instance
?Option
PutOption
)
(
underlier
?Option ?Stock)
(
price
?Stock
(
MeasureFn
?StockPrice ?U) ?Time)
(
instance
?U
UnitOfCurrency
)
(
strikePrice
?Option
(
MeasureFn
?StrikePrice ?U))
(
lessThan
?StrikePrice ?StockPrice)))
(
outOfTheMoney
?Option ?Time))
FinancialOntology.kif 3064-3075
There exist
a financial instrument
,
the financial instrument
Price and
another real number
such that
an agreement
is an
instance
of
put option
and
the financial instrument
is an
underlier
of
the agreement
and
the financial instrument
is
price
the financial instrument
Price
an unit of measure
(s) for
an agent
and
the unit of measure
is an
instance
of
unit of currency
and
the other real number
the unit of measure
(s) is a
strike
price of
the agreement
and
the other real number
is
less
than
the financial instrument
Price if and only if
the agent
is an
out
of the money of
the agreement
(=>
(
and
(
breathingRate
?H ?T ?R)
(
instance
?T
Minute
)
(
not
(
exists
(?R)
(
and
(
instance
?R
RecreationOrExercise
)
(
agent
?R ?H)
(
during
?T
(
WhenFn
?R)))))
(
holdsDuring
?T
(
attribute
?H
HumanAdult
))
(
or
(
greaterThan
?R 16)
(
lessThan
?R 12)))
(
holdsDuring
?T
(
not
(
attribute
?H
Healthy
))))
Medicine.kif 367-385
If
an agent
breathes
at a rate of
an integer
breaths per
a time interval
and
the time interval
is an
instance
of
minute
and there doesn't exist
the integer
such that
the integer
is an
instance
of
recreation or exercise
and
the agent
is an
agent
of
the integer
and
the time interval
takes place
during
the
time
of existence of
the integer
and
human adult
is an
attribute
of
the agent
holds
during
the time interval
and
the integer
is
greater
than 16 or
the integer
is
less
than 12,
then
healthy
is not an
attribute
of
the agent
holds
during
the time interval
(=>
(
and
(
customer
?CUST ?AGENT)
(
corkageFee
?AMT ?ITEM ?AGENT)
(
instance
?X ?ITEM)
(
not
(
exists
(?B)
(
and
(
instance
?B
Buying
)
(
patient
?B ?X)
(
destination
?B ?CUST)
(
origin
?B ?AGENT))))
(
instance
?D
Drinking
)
(
agent
?D ?CUST)
(
resource
?D ?X))
(
exists
(?C)
(
and
(
instance
?C
Corkage
)
(
agent
?C ?CUST)
(
refers
?C ?X)
(
destination
?C ?AGENT))))
Dining.kif 130-150
If
an agent
is a
customer
of
a cognitive agent
and
the agent
charges
a currency measure
in
corkage
for
a kind of object
and
another object
is an
instance
of
a kind of object
and there doesn't exist
a process
such that
the process
is an
instance
of
buying
and
the other object
is a
patient
of
the process
and
the process
end
s up at
the cognitive agent
and
the process
originate
s at
the agent
and
another process
is an
instance
of
drinking
and
the cognitive agent
is an
agent
of
the other process
and
the other object
is a
resource
for
the other process
,
then there exists
a third process
such that
the third process
is an
instance
of
corkage
and
the cognitive agent
is an
agent
of
the third process
and
the third process
includes a
reference
to
the other object
and
the third process
end
s up at
the agent
(=>
(
and
(
facility
?AGENT ?OBJ)
(
customer
?CUST ?AGENT)
(
instance
?X ?OBJ)
(
desires
?CUST
(
exists
(?PROC)
(
and
(
instance
?PROC
IntentionalProcess
)
(
patient
?PROC ?X)
(
agent
?PROC ?CUST)))))
(
modalAttribute
(
confersRight
(
uses
?X ?CUST) ?AGENT ?CUST)
Possibility
))
Dining.kif 336-350
If
an agent
provides
an object
and
the agent
is a
customer
of
a cognitive agent
and
an entity
is an
instance
of
the object
and
the cognitive agent
desire
s there exists
another entity
such that
the other entity
is an
instance
of
intentional process
and
the entity
is a
patient
of
the other entity
and
the cognitive agent
is an
agent
of
the other entity
,
then the statement
the agent
allow
s
the cognitive agent
to perform task of the type
the cognitive agent
use
s
the entity
has the
modal
force
of
possibility
(=>
(
and
(
instance
?A1
Automobile
)
(
instance
?A2
Automobile
)
(
instance
?S1
AutomobileShock
)
(
part
?S1 ?A1)
(
not
(
exists
(?S2)
(
and
(
instance
?S2
AutomobileShock
)
(
part
?S2 ?A2))))
(
dampingRatio
?A1 ?R1)
(
dampingRatio
?A2 ?R2))
(
greaterThan
?R2 ?R1))
Cars.kif 853-866
If
a physical system
is an
instance
of
automobile
and
another physical system
is an
instance
of
automobile
and
an object
is an
instance
of
shock
and
the object
is a
part
of
the physical system
and there doesn't exist
another object
such that
the other object
is an
instance
of
shock
and
the other object
is a
part
of
the other physical system
and the damping ratio of
the physical system
is
a real number
and the damping ratio of
the other physical system
is
another real number
,
then
the other real number
is
greater
than
the real number
(=>
(
and
(
instance
?AGENT
AutonomousAgent
)
(
potentialCustomer
?CUST ?AGENT)
(
modalAttribute
(
and
(
instance
?R
Reserving
)
(
destination
?R ?AGENT))
Necessity
)
(
conditionalProbability
(
exists
(?RES1)
(
and
(
instance
?RES1
Reservation
)
(
reservingEntity
?CUST ?RES1)
(
fulfillingEntity
?AGENT ?RES1)))
(
customer
?CUST ?AGENT) ?NUM1)
(
conditionalProbability
(
not
(
exists
(?RES2)
(
and
(
instance
?RES2
Reservation
)
(
reservingEntity
?CUST ?RES2)
(
fulfillingEntity
?AGENT ?RES2))))
(
customer
?CUST ?AGENT) ?NUM2))
(
lessThan
?NUM2 ?NUM1))
Dining.kif 772-795
If
an agent
is an
instance
of
agent
and
a cognitive agent
is a
potential
customer
for
the agent
and the statement
an entity
is an
instance
of
reserving
and
the entity
end
s up at
the agent
has the
modal
force
of
necessity
and
probability
of there exists
the entity
ES1 such that
the entity
ES1 is an
instance
of
reservation
and
the cognitive agent
reserves
the entity
ES1 and
the agent
fulfills
the entity
ES1 provided that
the agent
is a
customer
of
the cognitive agent
holds is
a real number
and
probability
of there doesn't exist
the entity
ES2 such that
the entity
ES2 is an
instance
of
reservation
and
the cognitive agent
reserves
the entity
ES2 and
the agent
fulfills
the entity
ES2 provided that
the agent
is a
customer
of
the cognitive agent
holds is
another real number
,
then
the other real number
is
less
than
the real number
(=>
(
and
(
instance
?Account
LiabilityAccount
)
(
minimumPayment
?Account
(
MeasureFn
?MinPayment ?U)
MonthDuration
)
(
instance
?U
UnitOfCurrency
)
(
exists
(?Payment ?Month)
(
and
(
instance
?Month
Month
)
(
destination
?Payment
(
CurrencyFn
?Account))
(
paymentsPerPeriod
?Account
(
MeasureFn
?Amount ?U) ?Month)
(
lessThan
?Amount ?MinPayment))))
(
exists
(?Penalty)
(
and
(
instance
?Penalty
Penalty
)
(
destination
?Penalty
(
CurrencyFn
?Account)))))
FinancialOntology.kif 759-775
If
a liability account
is an
instance
of
liability account
and
the liability account
is
minimum
payment
a real number
an unit of measure
(s) for
month duration
and
the unit of measure
is an
instance
of
unit of currency
and there exist
a process
and
a time interval
such that
the time interval
is an
instance
of
month
and
the process
end
s up at the
currency
of
the liability account
and
the liability account
payments
per period
another real number
the unit of measure
(s) for
the time interval
and
the other real number
is
less
than
the real number
,
then there exists
another process
such that
the other process
is an
instance
of
penalty
and
the other process
end
s up at the
currency
of
the liability account
(=>
(
and
(
instance
?B
Bubble
)
(
not
(
exists
(?X ?S)
(
and
(
attribute
?X ?S)
(
not
(
equal
?X
Gas
))
(
meetsSpatially
?X ?B)))))
(
attribute
?B
ConvexRoundShape
))
Mid-level-ontology.kif 5010-5019
If
an object
is an
instance
of
bubble
and there don't exist
another object
and
an attribute
such that
the attribute
is an
attribute
of
the other object
and
the other object
is not
equal
to
gas
and
the other object
meet
s
the object
,
then
convex round shape
is an
attribute
of
the object
(=>
(
and
(
instance
?BUYINGS
Collection
)
(
instance
?GMB
CurrencyMeasure
)
(
instance
?TOTAL
RealNumber
)
(
equal
?GMB
(
GMBFn
?BUYINGS))
(
equal
?TOTAL
(
CardinalityFn
(
KappaFn
?ITEM
(
and
(
instance
?ITEM
Object
)
(
exists
(?BUYING)
(
and
(
member
?BUYING ?BUYINGS)
(
patient
?BUYING ?ITEM))))))))
(
equal
(
ABPFn
?BUYINGS)
(
DivisionFn
?GMB ?TOTAL)))
UXExperimentalTerms.kif 3239-3259
If
a collection
is an
instance
of
collection
and
a real number
is an
instance
of
currency measure
and
an integer
is an
instance
of
real number
and
the real number
is
equal
to the
value
of
the collection
and
the integer
is
equal
to the number of
instances
in the
class
described by
a symbolic string
,
then the
average
price
of
the collection
is
equal
to
the real number
and
the integer
(=>
(
and
(
instance
?C
CateringService
)
(
agent
?C ?AGENT)
(
destination
?C ?CUST)
(
located
?AGENT ?LOC1)
(
customer
?CUST ?AGENT)
(
exists
(?S ?FOOD ?E)
(
and
(
instance
?S
Cooking
)
(
agent
?S ?AGENT)
(
result
?S ?FOOD)
(
patient
?C ?FOOD)
(
instance
?E
Eating
)
(
agent
?E ?CUST)
(
eventLocated
?E ?LOC2))))
(
not
(
equal
?LOC1 ?LOC2)))
Dining.kif 586-602
If
a process
is an
instance
of
catering
and
an agent
is an
agent
of
the process
and
the process
end
s up at
the process
UST and
the agent
is
located
at
an object
and
the agent
is a
customer
of
the process
UST and there exist
another process
,
an entity
and
a third process
such that
the other process
is an
instance
of
cooking
and
the agent
is an
agent
of
the other process
and
the entity
is a
result
of
the other process
and
the entity
is a
patient
of
the process
and
the third process
is an
instance
of
eating
and
the process
UST is an
agent
of
the third process
and
the third process
is
located
at
another object
,
then
the object
is not
equal
to
the other object
(=>
(
and
(
instance
?CS1 ?CLASS)
(
subclass
?CLASS
CompoundSubstance
)
(
not
(
exists
(?CS2)
(
and
(
instance
?CS2 ?CLASS)
(
part
?CS2 ?CS1))))
(
molecularRatio
?ECLASS ?N ?CLASS)
(
instance
?G
Group
)
(
member
?E ?G)
(
part
?E ?CS1)
(
instance
?E ?ECLASS))
(
memberCount
?G ?N))
Mid-level-ontology.kif 21766-21780
If
an object
is an
instance
of
a kind of compound substance
and
a kind of compound substance
is a
subclass
of
compound substance
and there doesn't exist
another object
such that
the other object
is an
instance
of
the kind of compound substance
and
the other object
is a
part
of
the object
and the number of molecules of
a kind of elemental substance
in a molecule of
the kind of compound substance
is
an integer
and
a collection
is an
instance
of
group
and
a third object
is a
member
of
the collection
and
the third object
is a
part
of
the object
and
the third object
is an
instance
of
a kind of elemental substance
,
then
the integer
is a
member
count of
the collection
(=>
(
and
(
instance
?EM
Electromagnet
)
(
not
(
holdsDuring
?T1
(
exists
(?T ?E)
(
and
(
instance
?T
Transfer
)
(
instance
?E
Electricity
)
(
objectTransferred
?T ?E)
(
path
?T ?EM))))))
(
not
(
holdsDuring
?T1
(
exists
(?M)
(
and
(
instance
?M
Magnetism
)
(
instrument
?M ?EM))))))
Cars.kif 3890-3906
If
an entity
is an
instance
of
electromagnet
and there exist
another entity
and
a third entity
such that
the other entity
is an
instance
of
transfer
and
the third entity
is an
instance
of
electricity
and the object transferred in
the other entity
is
the third entity
and
the entity
is
path
along which
the other entity
occurs doesn't hold
during
the other entity
1,
then there exists
a fourth entity
such that
the fourth entity
is an
instance
of
magnetism
and
the entity
is an
instrument
for
the fourth entity
doesn't hold
during
the other entity
1
(=>
(
and
(
instance
?GUN
Gun
)
(
instance
?U
UnitOfLength
)
(
effectiveRange
?GUN
(
MeasureFn
?LM ?U))
(
distance
?GUN ?O
(
MeasureFn
?LM1 ?U))
(
instance
?O
Organism
)
(
not
(
exists
(?O2)
(
between
?O ?O2 ?GUN)))
(
lessThanOrEqualTo
?LM1 ?LM))
(
exists
(?KILLING)
(
capability
(
KappaFn
?KILLING
(
and
(
instance
?KILLING
Killing
)
(
patient
?KILLING ?O)))
instrument
?GUN)))
Mid-level-ontology.kif 1410-1429
If
a device
is an
instance
of
gun
and
an unit of measure
is an
instance
of
unit of length
and
a real number
the unit of measure
(s) is an
effective
range of
the device
and the
distance
between
the device
and
an object
is
the real number
1
the unit of measure
(s) and
the object
is an
instance
of
organism
and there doesn't exist
the object
2 such that
the object
2 is
between
the object
and
the device
and
the real number
1 is
less
than or equal to
the real number
,
then there exists
a symbolic string
such that
the device
is
capable
of doing the
class
described by
the symbolic string
as a
instrument
(=>
(
and
(
instance
?GUN
Gun
)
(
instance
?U
UnitOfLength
)
(
effectiveRange
?GUN
(
MeasureFn
?LM ?U))
(
distance
?GUN ?O
(
MeasureFn
?LM1 ?U))
(
not
(
exists
(?O2)
(
between
?O ?O2 ?GUN)))
(
lessThanOrEqualTo
?LM1 ?LM))
(
exists
(?DAMAGING)
(
capability
(
KappaFn
?DAMAGING
(
and
(
instance
?DAMAGING
Damaging
)
(
patient
?DAMAGING ?O)))
instrument
?GUN)))
Mid-level-ontology.kif 1388-1406
If
a device
is an
instance
of
gun
and
an unit of measure
is an
instance
of
unit of length
and
a real number
the unit of measure
(s) is an
effective
range of
the device
and the
distance
between
the device
and
an object
is
the real number
1
the unit of measure
(s) and there doesn't exist
the object
2 such that
the object
2 is
between
the object
and
the device
and
the real number
1 is
less
than or equal to
the real number
,
then there exists
a symbolic string
such that
the device
is
capable
of doing the
class
described by
the symbolic string
as a
instrument
(=>
(
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
?PROCESS
TakingOff
)
(
patient
?PROCESS ?DUD)
(
not
(
exists
(?EXPLOSION)
(
and
(
instance
?EXPLOSION
Explosion
)
(
patient
?EXPLOSION ?DUD)))))
(
instance
?DUD
AbsoluteDud
))
MilitaryDevices.kif 1409-1418
If
a process
is an
instance
of
taking off
and
an entity
is a
patient
of
the process
and there doesn't exist
another process
such that
the other process
is an
instance
of
explosion
and
the entity
is a
patient
of
the other process
,
then
the entity
is an
instance
of
absolute dud
(=>
(
and
(
instance
?PURCHASES
Collection
)
(
forall
(?MEMBER)
(=>
(
member
?MEMBER ?PURCHASES)
(
instance
?MEMBER
Buying
)))
(
exists
(?REGION)
(
and
(
instance
?REGION
GeopoliticalArea
)
(
forall
(?BUYER ?BUYING)
(=>
(
and
(
instance
?BUYER
AutonomousAgent
)
(
instance
?BUYING
Buying
)
(
member
?BUYING ?PURCHASES)
(
agent
?BUYING ?BUYER))
(
located
?BUYER ?REGION))))))
(
exists
(?AMOUNT ?PURCHASE ?TOTAL_PURCHASE_AMOUNT)
(
and
(
total
(
KappaFn
?AMOUNT
(
and
(
instance
?PURCHASE
Buying
)
(
member
?PURCHASE ?PURCHASES)
(
transactionAmount
?PURCHASE ?AMOUNT))) ?TOTAL_PURCHASE_AMOUNT)
(
equal
(
GMBFn
?PURCHASES) ?TOTAL_PURCHASE_AMOUNT))))
UXExperimentalTerms.kif 2956-2983
If
a collection
is an
instance
of
collection
and for all
a physical
if
the physical
is a
member
of
the collection
,
then
the physical
is an
instance
of
buying
and there exists
an object
such that
the object
is an
instance
of
geopolitical area
and for all
an agent
and
a process
if
the agent
is an
instance
of
agent
and
the process
is an
instance
of
buying
and
the process
is a
member
of
the collection
and
the agent
is an
agent
of
the process
,
then
the agent
is
located
at
the object
,
then there exist
a symbolic string
,
an entity
and
another entity
_PURCHASE_AMOUNT such that the
total
of values in the
class
described by
the symbolic string
is
the other entity
_PURCHASE_AMOUNT and the
value
of
the collection
is
equal
to
the other entity
_PURCHASE_AMOUNT
Display limited to 25 items.
Show next 25
Display limited to 25 items.
Show next 25
consequent
(<=>
(
and
(
instance
?B
BodyPart
)
(
holdsDuring
?T
(
attribute
?B
Bare
)))
(
holdsDuring
?T
(
not
(
exists
(?C)
(
and
(
instance
?C
Clothing
)
(
covers
?C ?B))))))
Mid-level-ontology.kif 30202-30212
An entity
is an
instance
of
body part
and
bare
is an
attribute
of
the entity
holds
during
a time position
if and only if there doesn't exist
another entity
such that
the other entity
is an
instance
of
clothing
and
the other entity
covers
the entity
holds
during
the time position
(<=>
(
and
(
instance
?COPY
Photocopying
)
(
patient
?COPY ?OBJ1)
(
instance
?OBJ1
VisualContentBearingObject
)
(
containsInformation
?OBJ1 ?INFO1))
(
exists
(?OBJ2 ?INFO2)
(
and
(
result
?COPY ?OBJ2)
(
instance
?OBJ2
VisualContentBearingObject
)
(
containsInformation
?OBJ2 ?INFO2)
(
equal
?INFO1 ?INFO2))))
Mid-level-ontology.kif 26362-26373
A process
is an
instance
of
photocopying
and
a content bearing physical
is a
patient
of
the process
and
the content bearing physical
is an
instance
of
visual content bearing object
and
the content bearing physical
contain
s information
a proposition
if and only if there exist
another content bearing physical
and
another proposition
such that
the other content bearing physical
is a
result
of
the process
and
the other content bearing physical
is an
instance
of
visual content bearing object
and
the other content bearing physical
contain
s information
the other proposition
and
the proposition
is
equal
to
the other proposition
(<=>
(
and
(
instance
?PM
ParticulateMatter
)
(
part
?P ?PM)
(
approximateDiameter
?P
(
MeasureFn
?S
Micrometer
))
(
greaterThan
10.0 ?S)
(
greaterThan
?S 2.5))
(
exists
(?PM10)
(
and
(
instance
?PM10
CoarseParticulateMatter
)
(
part
?PM10 ?PM))))
Geography.kif 7440-7451
An object
is an
instance
of
PM
and
a self connected object
is a
part
of
the object
and the
approximate
diameter
of
the self connected object
is
a real number
micrometer
(s) and 10.0 is
greater
than
the real number
and
the real number
is
greater
than 2.5 if and only if there exists
the object
10 such that
the object
10 is an
instance
of
PM10
and
the object
10 is a
part
of
the object
(<=>
(
and
(
instance
?PM
ParticulateMatter
)
(
part
?P ?PM)
(
approximateDiameter
?P
(
MeasureFn
?S
Micrometer
))
(
greaterThanOrEqualTo
?S 2.5))
(
exists
(?PM25)
(
and
(
instance
?PM25
FineParticulateMatter
)
(
part
?PM25 ?PM))))
Geography.kif 7469-7479
An object
is an
instance
of
PM
and
a self connected object
is a
part
of
the object
and the
approximate
diameter
of
the self connected object
is
a real number
micrometer
(s) and
the real number
is
greater
than or equal to 2.5 if and only if there exists
the object
25 such that
the object
25 is an
instance
of
PM2.5
and
the object
25 is a
part
of
the object
(<=>
(
and
(
instance
?Y
(
YearFn
?YEAR))
(
equal
(
MaleLifeExpectancyAtBirthFn
?AREA ?Y) ?REALNUMBER))
(
exists
(?LIST ?COUNT ?LIFEEXPECTANCYAGE ?BIRTH ?INDIVIDUAL ?DEATH)
(
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) ?Y)
(
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 357-390
A year
is an
instance
of the
year
the year
EAR and the
male
life expectancy at birth of
a geopolitical area
and
the year
is
equal
to
a real number
if and only if there exist
a list
,
another integer
,, ,
a symbolic string
,, ,
an entity
,, ,
another entity
and
a third entity
such that
the list
is an
instance
of
list
and
length
of
the list
is an
instance
of
the other 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
the symbolic string
and there doesn't exist
a fifth entity
such that
the fifth entity
is an
instance
of
the symbolic string
and
the fifth 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
(<=>
(
and
(
instance
?YEAR
(
YearFn
?Y))
(
equal
(
FemaleLifeExpectancyAtBirthFn
?AREA ?YEAR) ?REALNUMBER))
(
exists
(?LIST ?COUNT ?LIFEEXPECTANCYAGE ?BIRTH ?INDIVIDUAL ?DEATH)
(
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) ?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 403-436
A year
is an
instance
of the
year
an integer
and the
female
life expectancy at birth of
a geopolitical area
and
the year
is
equal
to
a real number
if and only if there exist
a list
,
another integer
,, ,
a symbolic string
,, ,
an entity
,, ,
another entity
and
a third entity
such that
the list
is an
instance
of
list
and
length
of
the list
is an
instance
of
the other 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
the symbolic string
and there doesn't exist
a fifth entity
such that
the fifth entity
is an
instance
of
the symbolic string
and
the fifth 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
(<=>
(
and
(
instance
?YEAR
(
YearFn
?Y))
(
equal
(
LifeExpectancyAtBirthFn
?AREA ?YEAR) ?REALNUMBER))
(
exists
(?LIST ?COUNT ?LIFEEXPECTANCYAGE ?BIRTH ?INDIVIDUAL ?DEATH)
(
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) ?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 310-342
A year
is an
instance
of the
year
an integer
and the
life
expectancy at birth of
a geopolitical area
and
the year
is
equal
to
a real number
if and only if there exist
a list
,
another integer
,, ,
a symbolic string
,, ,
an entity
,, ,
another entity
and
a third entity
such that
the list
is an
instance
of
list
and
length
of
the list
is an
instance
of
the other 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
the symbolic string
and there doesn't exist
a fifth entity
such that
the fifth entity
is an
instance
of
the symbolic string
and
the fifth 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
(<=>
(
annualExpendituresOfAreaInPeriod
?AREA ?AMOUNT ?PERIOD)
(
exists
(?TIME)
(
and
(
instance
?TIME ?PERIOD)
(
holdsDuring
?TIME
(
annualExpendituresOfArea
?AREA ?AMOUNT)))))
Economy.kif 1517-1522
A geopolitical area
annual
expenditures of area in period
a currency measure
for
a kind of time interval
if and only if there exists
a time position
such that
the time position
is an
instance
of
a kind of time interval
and
the currency measure
is an
annual
expenditures of area of
the geopolitical area
holds
during
the time position
(<=>
(
annualRevenuesOfAreaInPeriod
?AREA ?AMOUNT ?PERIOD)
(
exists
(?TIME)
(
and
(
instance
?TIME ?PERIOD)
(
holdsDuring
?TIME
(
annualRevenuesOfArea
?AREA ?AMOUNT)))))
Economy.kif 1488-1493
A geopolitical area
annual
revenues of area in period
a currency measure
for
a kind of time interval
if and only if there exists
a time position
such that
the time position
is an
instance
of
a kind of time interval
and
the currency measure
is an
annual
revenues of area of
the geopolitical area
holds
during
the time position
(<=>
(
attribute
?MUSIC
PolyphonicMusic
)
(
exists
(?PART1 ?PART2)
(
and
(
instance
?MUSIC
MakingMusic
)
(
instance
?PART1
MakingMusic
)
(
instance
?PART2
MakingMusic
)
(
subProcess
?PART1 ?MUSIC)
(
subProcess
?PART2 ?MUSIC)
(
not
(
equal
?PART1 ?PART2))
(
cooccur
?PART1 ?MUSIC)
(
cooccur
?PART2 ?MUSIC))))
Mid-level-ontology.kif 744-755
Polyphonic music
is an
attribute
of
an object
if and only if there exist
a process
and
another process
such that
the object
is an
instance
of
making music
and
the process
is an
instance
of
making music
and
the other process
is an
instance
of
making music
and
the process
is a
subprocess
of
the object
and
the other process
is a
subprocess
of
the object
and
the process
is not
equal
to
the other process
and
the process
occur
s at the same time as
the object
and
the other process
occur
s at the same time as
the object
(<=>
(
attribute
?WATER
OpenSea
)
(
exists
(?LAND ?DIST)
(
and
(
instance
?WATER
SaltWaterArea
)
(
not
(
instance
?WATER
LandlockedWater
))
(
distance
?LAND ?WATER
(
MeasureFn
?DIST
NauticalMile
))
(
greaterThan
?DIST 5.0))))
Geography.kif 4711-4720
Open sea
is an
attribute
of
an object
if and only if there exist
a physical
and
a real number
such that
the object
is an
instance
of
salt water area
and
the object
is not an
instance
of
landlocked water
and the
distance
between
the physical
and
the object
is
the real number
nautical mile
(s) and
the real number
is
greater
than 5.0
(<=>
(
aunt
?A ?H)
(
exists
(?P)
(
and
(
sister
?A ?P)
(
parent
?H ?P))))
Mid-level-ontology.kif 23098-23103
A woman
is the
aunt
of
a human
if and only if there exists
another human
such that
the woman
is the
sister
of
the other human
and
the other human
is a
parent
of
the human
(<=>
(
average
?LIST1 ?AVERAGE)
(
exists
(?LIST2 ?LASTPLACE)
(
and
(
equal
(
ListLengthFn
?LIST2)
(
ListLengthFn
?LIST1))
(
equal
(
ListOrderFn
?LIST2 1)
(
ListOrderFn
?LIST1 1))
(
forall
(?ITEMFROM2)
(=>
(
inList
?ITEMFROM2 ?LIST2)
(
exists
(?POSITION ?POSITIONMINUSONE ?ITEMFROM1 ?PRIORFROM2)
(
and
(
greaterThan
?POSITION 1)
(
lessThanOrEqualTo
?POSITION
(
ListLengthFn
?LIST2))
(
equal
(
ListOrderFn
?LIST2 ?ITEMFROM2) ?POSITION)
(
inList
?ITEMFROM1 ?LIST1)
(
equal
?POSITION
(
ListOrderFn
?LIST1 ?ITEMFROM1))
(
inList
?PRIORFROM2 ?LIST2)
(
equal
?POSITIONMINUSONE
(
SubtractionFn
?POSITION 1))
(
equal
?POSITIONMINUSONE
(
ListOrderFn
?LIST2 ?PRIORFROM2))
(
equal
?ITEMFROM2
(
AdditionFn
?ITEMFROM1 ?PRIORFROM2))))))
(
equal
?LASTPLACE
(
ListLengthFn
?LIST2))
(
equal
?AVERAGE
(
DivisionFn
(
ListOrderFn
?LIST2 ?LASTPLACE) ?LASTPLACE)))))
People.kif 272-293
A real number
is an
average
of
a list
if and only if there exist
another list
and
a positive integer
such that
length
of
the other list
is
equal
to
length
of
the list
and 1th
element
of
the other list
is
equal
to 1th
element
of
the list
and for all
another positive integer
if
the other positive integer
is a
member
of
the other list
,
then there exist
another real number
,
the other real number
MINUSONE,, ,
a third positive integer
and
a fourth positive integer
such that
the other real number
is
greater
than 1 and
the other real number
is
less
than or equal to
length
of
the other list
and
the other positive integer
th
element
of
the other list
is
equal
to
the other real number
and
the third positive integer
is a
member
of
the list
and
the other real number
is
equal
to
the third positive integer
th
element
of
the list
and
the fourth positive integer
is a
member
of
the other list
and
the other real number
MINUSONE is
equal
to (
the other real number
and 1) and
the other real number
MINUSONE is
equal
to
the fourth positive integer
th
element
of
the other list
and
the other positive integer
is
equal
to (
the third positive integer
and
the fourth positive integer
)
and
the positive integer
is
equal
to
length
of
the other list
and
the real number
is
equal
to
the positive integer
th
element
of
the other list
and
the positive integer
(<=>
(
bankAccount
?AccountType ?Bank)
(
exists
(?Account)
(
and
(
instance
?Account ?AccountType)
(
accountAt
?Account ?Bank))))
FinancialOntology.kif 3943-3948
A BankFinancialOrganization
is a
bank
account of
a kind of financial account
if and only if there exists
another financial account
such that
the other financial account
is an
instance
of
a kind of financial account
and
the other financial account
is
held
by
the BankFinancialOrganization
(<=>
(
beliefGroupPercentInRegion
?BG ?N ?R)
(
exists
(?G1 ?G2 ?P ?P2 ?N1 ?N2)
(
and
(
located
?P ?R)
(
member
?P ?BG)
(
member
?P ?G1)
(
memberCount
?G1 ?N1)
(
located
?P2 ?R)
(
member
?P2 ?G2)
(
memberCount
?G2 ?N2)
(
equal
(
DivisionFn
?N 100)
(
DivisionFn
?N1 ?N2)))))
People.kif 1528-1539
A real number
percent of people in
a geographic area
believe
in
a belief group
if and only if there exist
a collection
,
another collection
,, ,
a physical
,, ,
the physical
2,, ,
the real number
1 and
the real number
2 such that
the physical
is
located
at
the geographic area
and
the physical
is a
member
of
the belief group
and
the physical
is a
member
of
the collection
and
the real number
1 is a
member
count of
the collection
and
the physical
2 is
located
at
the geographic area
and
the physical
2 is a
member
of
the other collection
and
the real number
2 is a
member
count of
the other collection
and
the real number
and 100 is
equal
to
the real number
1 and
the real number
2
(<=>
(
capitalExpendituresOfAreaInPeriod
?AREA ?CAPAMOUNT ?PERIOD)
(
exists
(?TIME)
(
and
(
instance
?TIME ?PERIOD)
(
holdsDuring
?TIME
(
capitalExpendituresOfArea
?AREA ?CAPAMOUNT)))))
Economy.kif 1565-1570
A geopolitical area
capital
expenditures of area in period
a currency measure
for
a kind of time interval
if and only if there exists
a time position
such that
the time position
is an
instance
of
a kind of time interval
and
the currency measure
is a
capital
expenditures of area of
the geopolitical area
holds
during
the time position
(<=>
(
cousin
?P1 ?P2)
(
and
(
exists
(?G1 ?G2)
(
and
(
grandmother
?P1 ?G1)
(
grandfather
?P1 ?G2)
(
grandmother
?P2 ?G1)
(
grandfather
?P2 ?G2)))
(
not
(
exists
(?M ?F)
(
and
(
mother
?P1 ?M)
(
father
?P1 ?F)
(
mother
?P2 ?M)
(
father
?P2 ?F))))))
Mid-level-ontology.kif 23113-23128
A human
and
another human
are
cousins
if and only if there exist
a woman
and
a man
such that the
grandmother
of
the human
is
the woman
and the
grandfather
of
the human
is
the man
and the
grandmother
of
the other human
is
the woman
and the
grandfather
of
the other human
is
the man
and there don't exist
an organism
and
another organism
such that
the organism
is a
mother
of
the human
and
the other organism
is a
father
of
the human
and
the organism
is a
mother
of
the other human
and
the other organism
is a
father
of
the other human
(<=>
(
currencyExchangePerUSDollar
?AMOUNT ?PERIOD)
(
exists
(?TIME)
(
and
(
instance
?TIME ?PERIOD)
(
holdsDuring
?TIME
(
currencyExchangeRate
UnitedStatesDollar
?AMOUNT)))))
Economy.kif 3661-3666
A kind of time interval
is a
currency
exchange per US dollar of
a currency measure
if and only if there exists
a time position
such that
the time position
is an
instance
of
a kind of time interval
and
the currency measure
is a
currency
exchange rate of
united states dollar
holds
during
the time position
(<=>
(
currencyExchangeRateInPeriod
?UNIT ?AMOUNT ?PERIOD)
(
exists
(?TIME)
(
and
(
instance
?TIME ?PERIOD)
(
holdsDuring
?TIME
(
currencyExchangeRate
?UNIT ?AMOUNT)))))
Economy.kif 3668-3673
An unit of currency
currency
exchange rate in period
a currency measure
for
a kind of time interval
if and only if there exists
a time position
such that
the time position
is an
instance
of
a kind of time interval
and
the currency measure
is a
currency
exchange rate of
the unit of currency
holds
during
the time position
(<=>
(
customer
?AGENT1 ?AGENT2)
(
exists
(?SERVICE)
(
and
(
instance
?SERVICE
FinancialTransaction
)
(
agent
?SERVICE ?AGENT2)
(
destination
?SERVICE ?AGENT1))))
Mid-level-ontology.kif 7754-7760
An agent
is a
customer
of
a cognitive agent
if and only if there exists
a process
such that
the process
is an
instance
of
financial transaction
and
the agent
is an
agent
of
the process
and
the process
end
s up at
the cognitive agent
(<=>
(
customerRepresentative
?Person1 ?Person2 ?Org)
(
exists
(?Service)
(
and
(
instance
?Service
FinancialTransaction
)
(
employs
?Org ?Person1)
(
agent
?Service ?Person1)
(
destination
?Service ?Person2))))
FinancialOntology.kif 3635-3642
A cognitive agent
customer
representative
another cognitive agent
for
an organization
if and only if there exists
a process
such that
the process
is an
instance
of
financial transaction
and
the organization
employ
s
the cognitive agent
and
the cognitive agent
is an
agent
of
the process
and
the process
end
s up at
the other cognitive agent
(<=>
(
earthAltitude
?OBJ ?ALT)
(
exists
(?SEA)
(
and
(
altitude
?OBJ ?SEA ?ALT)
(
surface
?SEA
PlanetEarth
))))
Geography.kif 2781-2786
An object
is
a length measure
above
the ground if and only if there exists
a self connected object
such that the
altitude
of
the object
is
the self connected object
and
the self connected object
is a
surface
of
planet earth
(<=>
(
economicAidDonatedInPeriod
?COUNTRY ?AMOUNT ?PERIOD)
(
exists
(?TIME)
(
and
(
instance
?TIME ?PERIOD)
(
holdsDuring
?TIME
(
economicAidDonated
?COUNTRY ?AMOUNT)))))
Economy.kif 2819-2824
A geopolitical area
is
economic
aid donated in period
a currency measure
for
a kind of time interval
if and only if there exists
a time position
such that
the time position
is an
instance
of
a kind of time interval
and
the currency measure
is an
economic
aid donated of
the geopolitical area
holds
during
the time position
(<=>
(
economicAidReceivedNetInPeriod
?COUNTRY ?AMOUNT ?PERIOD)
(
exists
(?TIME)
(
and
(
instance
?TIME ?PERIOD)
(
holdsDuring
?TIME
(
economicAidReceivedNet
?COUNTRY ?AMOUNT)))))
Economy.kif 2859-2864
A geopolitical area
is
economic
aid received net in period
a currency measure
for
a kind of time interval
if and only if there exists
a time position
such that
the time position
is an
instance
of
a kind of time interval
and
the currency measure
is an
economic
aid received net of
the geopolitical area
holds
during
the time position
(<=>
(
electricityFractionFromSourceInPeriod
?AREA ?SOURCE ?FRACTION ?PERIOD)
(
exists
(?TIME)
(
and
(
instance
?TIME ?PERIOD)
(
holdsDuring
?TIME
(
electricityFractionFromSource
?AREA ?SOURCE ?FRACTION)))))
Economy.kif 2056-2061
A geopolitical area
is
electricity
fraction from source in period
a kind of power generation
for
a real number
with
a kind of time interval
if and only if there exists
a time position
such that
the time position
is an
instance
of
a kind of time interval
and
the geopolitical area
is
electricity
fraction from source
a kind of power generation
for
the real number
holds
during
the time position
Display limited to 25 items.
Show next 25
Display limited to 25 items.
Show next 25
statement
(
containsInformation
(
forall
(?POLITY ?VOTER ?ELECTION ?VOTINGAGE ?AGE)
(=>
(
and
(
citizen
?VOTER ?POLITY)
(
suffrageAgeMinimum
?POLITY
(
MeasureFn
?VOTINGAGE
YearDuration
))
(
age
?VOTER
(
MeasureFn
?AGE
YearDuration
))
(
greaterThanOrEqualTo
?AGE ?VOTINGAGE)
(
instance
?ELECTION
(
ElectionFn
?POLITY)))
(
exists
(?VOTING)
(
and
(
instance
?VOTING
(
VotingFn
?ELECTION))
(
agent
?VOTING ?VOTER)))))
CompulsorySuffrageLaw
)
Government.kif 1124-1138
For all ?POLITY, ?VOTER,, , ?ELECTION,, , ?VOTINGAGE and ?AGE
if ?VOTER is a
citizen
of ?POLITY and ?VOTINGAGE
year duration
(s) is a
suffrage
age minimum of ?POLITY and the
age
of ?VOTER is ?AGE
year duration
(s) and ?AGE is
greater
than or equal to ?VOTINGAGE and ?ELECTION is an
instance
of the
election
of ?POLITY,
then there exists ?VOTING such that ?VOTING is an
instance
of the
voting
of ?ELECTION and ?VOTER is an
agent
of ?VOTING
contain
s information
compulsory suffrage law
(
decreasesLikelihood
(
exists
(?X ?CUT ?PAPER ?CBO ?INFO)
(
and
(
instance
?X
PaperShredder
)
(
instance
?CUT
Cutting
)
(
instrument
?CUT ?X)
(
instance
?PAPER
Paper
)
(
patient
?CUT ?PAPER)
(
located
?CBO ?PAPER)
(
instance
?CBO
VisualContentBearingObject
)
(
containsInformation
?CBO ?INFO)))
(
exists
(?READ)
(
and
(
instance
?READ
Interpreting
)
(
patient
?READ ?INFO)
(
earlier
(
WhenFn
?CUT)
(
WhenFn
?READ)))))
Mid-level-ontology.kif 18229-18246
There exist ?X, ?CUT,, , ?PAPER,, , ?CBO and ?INFO such that ?X is an
instance
of
paper shredder
and ?CUT is an
instance
of
cutting
and ?X is an
instrument
for ?CUT and ?PAPER is an
instance
of
paper
and ?PAPER is a
patient
of ?CUT and ?CBO is
located
at ?PAPER and ?CBO is an
instance
of
visual content bearing object
and ?CBO
contain
s information ?INFO
decrease
s likelihood of there exists ?READ such that ?READ is an
instance
of
interpreting
and ?INFO is a
patient
of ?READ and the
time
of existence of ?CUT happens
earlier
than the
time
of existence of ?READ
(
hasPurpose
IBookstore
(
exists
(?D)
(
and
(
instance
?D
DownloadingOverNetwork
)
(
instrument
?D
IBookstore
)
(
instance
?T
Text
)
(
objectTransferred
?D ?T))))
ComputingBrands.kif 3309-3315
IBookstore
has the purpose there exists ?D such that ?D is an
instance
of
downloading
and
iBookstore
is an
instrument
for ?D and ?T is an
instance
of
text
and the object transferred in ?D is ?T
(
not
(
exists
(?PATH1 ?PATH2)
(
and
(
instance
?PATH1
(
CutSetFn
?GRAPH))
(
instance
?PATH2
(
MinimalCutSetFn
?GRAPH))
(
pathLength
?PATH1 ?NUMBER1)
(
pathLength
?PATH2 ?NUMBER2)
(
lessThan
?NUMBER1 ?NUMBER2))))
Merge.kif 6100-6107
There don't exist
a graph path
and
another graph path
such that
the graph path
is an
instance
of the
set
of paths that partition
a graph
into two separate graphs and
the other graph path
is an
instance
of the
set
of minimal paths that partition
the graph
into two separate graphs and the
length
of
the graph path
is
a positive integer
and the
length
of
the other graph path
is
another positive integer
and
the positive integer
is
less
than
the other positive integer
appearance as argument number 0
(
exists
(?D ?M)
(
and
(
instance
?D
Disseminating
)
(
agent
?D
Netflix
)
(
patient
?D ?M)
(
instance
?M
MotionPicture
)))
Medicine.kif 4559-4564
There exist
a process
and
an entity
such that
the process
is an
instance
of
disseminating
and
Netflix Corp.
is an
agent
of
the process
and
the entity
is a
patient
of
the process
and
the entity
is an
instance
of
motion picture
(
exists
(?FM)
(
and
(
instance
?FM
FilmMaking
)
(
agent
?FM
Netflix
)))
Medicine.kif 4566-4569
There exists
a process
such that
the process
is an
instance
of
film making
and
Netflix Corp.
is an
agent
of
the process
(
exists
(?H)
(
and
(
attribute
?H
NewReporter
)
(
employs
ProPublica
?H)))
Medicine.kif 4590-4593
There exists
a cognitive agent
such that
NewReporter
is an
attribute
of
the cognitive agent
and
Pro Publica Inc.
employ
s
the cognitive agent
(
exists
(?MEAL ?REGION)
(
attribute
?MEAL
(
MealAttributeFn
?MEAL ?REGION)))
Food.kif 1902-1903
There exist
a meal
and
a region
such that the appropriate
meal
for
the meal
in
the region
is an
attribute
of
the meal
(
exists
(?T)
(
and
(
instance
?T
(
YearFn
1976))
(
holdsDuring
?T
(
coworker
SteveJobsOfApple
SteveWozniakOfApple
))))
ComputingBrands.kif 2453-2457
There exists
a time position
such that
the time position
is an
instance
of the
year
1976 and
Steve Wozniak
is a
coworker
of
Steve Jobs
holds
during
the time position
(
exists
(?T)
(
and
(
instance
?T
(
YearFn
2002))
(
holdsDuring
?T
(
coworker
SteveJobsOfApple
TimCookOfApple
))))
ComputingBrands.kif 2441-2445
There exists
a time position
such that
the time position
is an
instance
of the
year
2002 and
Tim Cook
is a
coworker
of
Steve Jobs
holds
during
the time position
(
exists
(?T)
(
and
(
subclass
?T
HandToolBox
)
(
manufacturer
?T
SortimoCorp
)))
Cars.kif 5094-5097
There exists
a kind of object
such that
a kind of object
is a
subclass
of
tool box
and the maker of
the kind of object
is
Sortimo Corporation
(
exists
(?THING)
(
instance
?THING
Entity
))
Merge.kif 825-826
There exists
an entity
such that
the entity
is an
instance
of
entity
(
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 1970-1978
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
Jesus of Nazareth
and
the time interval
start
s the
time
of existence of
Twelve apostles
and for all
an entity
if
the entity
is a
member
of
Twelve apostles
holds
during
the time interval
,
then
Jesus of Nazareth
is a
friend
of
the entity
holds
during
the time interval
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