and
No TPTP formula. May not be expressible in strict first order.
Mid-level-ontology.kif 24763-24768
A postal place
is
located
at
a city
and
the postal place
is an
instance
of
postal place
and
the city
is an
instance
of
city
if and only if
the postal place
is in
the city
No TPTP formula. May not be expressible in strict first order.
Mid-level-ontology.kif 24676-24681
A postal place
is
located
at
a neighborhood
and
the postal place
is an
instance
of
postal place
and
the neighborhood
is an
instance
of
neighborhood
if and only if
the postal place
is in
the neighborhood
No TPTP formula. May not be expressible in strict first order.
Mid-level-ontology.kif 24747-24752
A postal place
is
located
at
a state or province
and
the postal place
is an
instance
of
postal place
and
the state or province
is an
instance
of
state or province
if and only if
the postal place
is in
the state or province
No TPTP formula. May not be expressible in strict first order.
Mid-level-ontology.kif 24713-24720
A postal place
is
located
at
a geopolitical area
and
the postal place
is an
instance
of
postal place
and
the geopolitical area
is an
instance
of
nation
or
the geopolitical area
is an
instance
of
dependency or special sovereignty area
if and only if
the postal place
is in
the geopolitical area
No TPTP formula. May not be expressible in strict first order.
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
No TPTP formula. May not be expressible in strict first order.
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
No TPTP formula. May not be expressible in strict first order.
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
No TPTP formula. May not be expressible in strict first order.
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
No TPTP formula. May not be expressible in strict first order.
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
No TPTP formula. May not be expressible in strict first order.
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
No TPTP formula. May not be expressible in strict first order.
Merge.kif 17254-17262
An entity
is an
instance
of
human
and for all
another entity
the other entity
doesn't
employ
the entity
holds
during
a time position
if and only if
unemployed person
is an
attribute
of
the entity
holds
during
the time position
No TPTP formula. May not be expressible in strict first order.
Mid-level-ontology.kif 23252-23258
If
a case role
a process
and
an object
and
the case role
is an
instance
of
case role
and
the process
is an
instance
of
process
and
the object
is an
instance
of
object
,
then
the object
plays
role in event
the case role
for
the process
No TPTP formula. May not be expressible in strict first order.
Media.kif 3165-3169
If
a symbolic string
is the
short
title
of
an entity
-TYPE in
a language
and
another entity
is an
instance
of
the entity
-TYPE,
then
the symbolic string
is an
abbreviation
of
the other entity
No TPTP formula. May not be expressible in strict first order.
UXExperimentalTerms.kif 881-885
If
an user account
is an
account
at
a web site
and
an agent
has
account
the user account
,
then
the agent
is a
registered
user
of
the web site
No TPTP formula. May not be expressible in strict first order.
FinancialOntology.kif 3621-3625
If
a cognitive agent
holds
account
a financial account
and
the financial account
is
held
by
a financial organization
,
then
the financial organization
is a
customer
of
the cognitive agent
No TPTP formula. May not be expressible in strict first order.
Media.kif 3041-3045
If
a symbolic string
is an
acronym
for
an entity
and
a character
is
part
of
the symbolic string
,
then
the character
is an
instance
of
alphabetic character
No TPTP formula. May not be expressible in strict first order.
Mid-level-ontology.kif 20760-20767
If
a human
&actedIn
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
No TPTP formula. May not be expressible in strict first order.
Mid-level-ontology.kif 18837-18843
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
No TPTP formula. May not be expressible in strict first order.
FinancialOntology.kif 487-499
If
an agent
is an
agent
of
a process
and
the process
originate
s at
an object
and
a physical
is a
patient
of
the process
and
value
of
the physical
is
a currency measure
,
then there exists
a financial transaction
such that
the financial transaction
is a
subprocess
of
the process
and
the financial transaction
is an
instance
of
payment
and
the currency measure
is a
transaction
amount of
the financial transaction
and
the financial transaction
originate
s at
the agent
and
the financial transaction
end
s up at
the object
No TPTP formula. May not be expressible in strict first order.
Mid-level-ontology.kif 14079-14089
If
a cognitive agent
has the responsibility to make
a proposition
a deontic attribute
in
an agreement
and
the deontic attribute
is
equal
to
obligation
or
the deontic attribute
is
equal
to
promise
,
then the statement there exists
an entity
such that
the entity
express
es the content of
the proposition
and
the cognitive agent
is an
agent
of
the entity
has the
modal
force
of
likely
No TPTP formula. May not be expressible in strict first order.
Government.kif 714-719
If
a time point
is an
agreement
effective date of
an agreement
and
the agreement
obligate
s
a cognitive agent
to perform task of the type
a formula
and
a time position
is an
instance
of
the time point
,
then
the cognitive agent
is
obliged
to perform tasks of type
the formula
holds
during
immediately
after
the time position
No TPTP formula. May not be expressible in strict first order.
Government.kif 721-726
If
a time point
is an
agreement
effective date of
an agreement
and
the agreement
allow
s
a cognitive agent
to perform task of the type
a formula
and
a time position
is an
instance
of
the time point
,
then
the cognitive agent
has the
right
to perform
the formula
holds
during
immediately
after
the time position
No TPTP formula. May not be expressible in strict first order.
FinancialOntology.kif 722-726
If
a time point
is an
agreement
effective date of
a financial account
and
the financial account
current
account balance
the time point
for
a currency measure
,
then
the currency measure
is an
original
balance of
the financial account
No TPTP formula. May not be expressible in strict first order.
Government.kif 766-772
If
a kind of time position
is an
agreement
effective during of
a proposition
and
another time position
is an
instance
of
a kind of time position
and
a formula
is an
instance
of
formula
and
the formula
contain
s information
the proposition
,
then
the formula
holds
during
the other time position
No TPTP formula. May not be expressible in strict first order.
Mid-level-ontology.kif 14016-14021
If
a time interval
is an
agreement
period of
an agreement
and
a time point
is an
agreement
effective date of
the agreement
,
then
the agreement
the
attribute
active agreement
holds
during
a
time
that starts at
the time point
and lasts for
the time interval
Display limited to 25 items.
Show next 25
Display limited to 25 items.
Show next 25
Sigma web home
Suggested Upper Merged Ontology (SUMO) web home
Sigma version 3.0 is
open source software
produced by
Articulate Software
and its partners
