Browsing Interface
: Welcome guest :
log in
[
Home
| 
Graph
|  ]
KB:
SUMO
Language:
ChineseLanguage
ChinesePinyinWriting
ChineseSimplifiedWriting
ChineseTraditionalLanguage
EnglishLanguage
FrenchLanguage
GermanLanguage
JapaneseLanguage
SpanishLanguage
SwedishLanguage
Formal Language:
OWL
SUO-KIF
TPTP
traditionalLogic
KB Term:
Term intersection
English Word:
Any
Noun
Verb
Adjective
Adverb
forall
Sigma KEE - forall
forall
antecedent
(<=>
(
holdsDuring
?T
(
and
(
instance
?PERSON
Human
)
(
forall
(?ORG)
(
not
(
employs
?ORG ?PERSON)))))
(
holdsDuring
?T
(
attribute
?PERSON
Unemployed
)))
Merge.kif 16994-17002
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
is an
attribute
of
the entity
holds
during
the time position
(=>
(
and
(
climateTypeInArea
?AREA
ColdClimateZone
)
(
forall
(?MO)
(
and
(
instance
?MO
Month
)
(
averageTemperatureForPeriod
?AREA ?MO
(
MeasureFn
?TEMP
CelsiusDegree
)))))
(
greaterThan
10.0 ?TEMP))
Geography.kif 1526-1534
If
cold climate zone
is a
climate
type in area of
a geographic area
and for all
a time interval
the time interval
is an
instance
of
month
and
the geographic area
average
temperature for period
the time interval
for
a real number
celsius degree
(s),
then 10.0 is
greater
than
the real number
(=>
(
and
(
equal
(
PathWeightFn
?PATH) ?SUM)
(
graphPart
?ARC1 ?PATH)
(
graphPart
?ARC2 ?PATH)
(
arcWeight
?ARC1 ?NUMBER1)
(
arcWeight
?ARC2 ?NUMBER2)
(
forall
(?ARC3)
(=>
(
graphPart
?ARC3 ?PATH)
(
or
(
equal
?ARC3 ?ARC1)
(
equal
?ARC3 ?ARC2)))))
(
equal
(
PathWeightFn
?PATH)
(
AdditionFn
?NUMBER1 ?NUMBER2)))
Merge.kif 5891-5904
If the
value
of
a graph path
is
equal
to
a real number
and
a graph arc
is a
part
of
the graph path
and
another graph arc
is a
part
of
the graph path
and the
value
of
the graph arc
is
another real number
and the
value
of
the other graph arc
is
a third real number
and for all
a graph element
if
the graph element
is a
part
of
the graph path
,
then
the graph element
is
equal
to
the graph arc
or
the graph element
is
equal
to
the other graph arc
,
then the
value
of
the graph path
is
equal
to (
the other real number
and
the third real number
)
(=>
(
and
(
equal
(
PathWeightFn
?PATH) ?SUM)
(
subGraph
?SUBPATH ?PATH)
(
graphPart
?ARC1 ?PATH)
(
arcWeight
?ARC1 ?NUMBER1)
(
forall
(?ARC2)
(=>
(
graphPart
?ARC2 ?PATH)
(
or
(
graphPart
?ARC2 ?SUBPATH)
(
equal
?ARC2 ?ARC1)))))
(
equal
?SUM
(
AdditionFn
(
PathWeightFn
?SUBPATH) ?NUMBER1)))
Merge.kif 5877-5889
If the
value
of
a graph path
is
equal
to
a real number
and
another graph path
is a
subgraph
of
the graph path
and
a graph arc
is a
part
of
the graph path
and the
value
of
the graph arc
is
another real number
and for all
a graph element
if
the graph element
is a
part
of
the graph path
,
then
the graph element
is a
part
of
the other graph path
or
the graph element
is
equal
to
the graph arc
,
then
the real number
is
equal
to (the
value
of
the other graph path
and
the other real number
)
(=>
(
and
(
instance
?AUCTIONS
Collection
)
(
forall
(?AUC)
(=>
(
member
?AUC ?AUCTIONS)
(
instance
?AUC
Auctioning
))))
(
and
(
total
(
KappaFn
?AMOUNT
(
and
(
instance
?AUCTION
Auctioning
)
(
member
?AUCTION ?AUCTIONS)
(
transactionAmount
?AUCTION ?AMOUNT))) ?TOTAL_PURCHASE_AMOUNT)
(
equal
(
AuctionGMBFn
?AUCTIONS) ?TOTAL_PURCHASE_AMOUNT)))
UXExperimentalTerms.kif 3409-3424
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
auction
,
then the
total
of values in the
class
described by
a symbolic string
is
an entity
_PURCHASE_AMOUNT and the
total
purchase
price
of
the collection
is
equal
to
the entity
_PURCHASE_AMOUNT
(=>
(
and
(
instance
?COLL
Collection
)
(
forall
(?MEMBER)
(=>
(
member
?MEMBER ?COLL)
(
instance
?MEMBER
FinancialTransaction
))))
(
equal
(
CardinalityFn
(
KappaFn
?ITEM
(
and
(
instance
?ITEM
Physical
)
(
instance
?BUYING
Buying
)
(
member
?BUYING ?COLL)
(
patient
?BUYING ?ITEM))))
(
BoughtItemsFn
?COLL)))
UXExperimentalTerms.kif 3096-3111
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
financial transaction
,
then the number of
instances
in the
class
described by
a symbolic string
is
equal
to number of items
purchased
in
the collection
(=>
(
and
(
instance
?COLL
Collection
)
(
forall
(?MEMBER)
(=>
(
member
?MEMBER ?COLL)
(
instance
?MEMBER
WebListing
))))
(
equal
(
CardinalityFn
(
KappaFn
?BIDDING
(
and
(
instance
?ITEM
Physical
)
(
instance
?LISTING
WebListing
)
(
instance
?BIDDING
Bidding
)
(
member
?LISTING ?COLL)
(
objectOfBid
?BIDDING ?ITEM)
(
patient
?LISTING ?ITEM))))
(
BidCountFn
?COLL)))
UXExperimentalTerms.kif 3130-3147
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
web listing
,
then the number of
instances
in the
class
described by
a symbolic string
is
equal
to number of
bids
in
the collection
(=>
(
and
(
instance
?COLL
Collection
)
(
forall
(?MEMBER)
(=>
(
member
?MEMBER ?COLL)
(
instance
?MEMBER
WebListing
))))
(
equal
(
DivisionFn
(
CardinalityFn
(
KappaFn
?LISTING
(
and
(
instance
?LISTING
WebListing
)
(
instance
?SITE
WebSite
)
(
instance
?ITEM
Physical
)
(
member
?LISTING ?COLL)
(
patient
?LISTING ?ITEM)
(
hostedOn
?LISTING ?SITE)
(
exists
(?BUYING)
(
and
(
instance
?BUYING
Buying
)
(
patient
?BUYING ?ITEM)
(
eCommerceSite
?BUYING ?SITE))))))
(
CardinalityFn
?COLL))
(
BidCountFn
?COLL)))
UXExperimentalTerms.kif 3055-3079
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
web listing
,
then the number of
instances
in the
class
described by
a symbolic string
and the number of
instances
in
the collection
is
equal
to number of
bids
in
the collection
(=>
(
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 ?MEMBER)
(
and
(=>
(
and
(
instance
?ITEM
WebListing
)
(
member
?ITEM
(
SellersItemsFn
?AGENT ?SITE))
(
temporalPart
?TIME
(
WhenFn
?ITEM))
(
not
(
equal
?ITEM ?LISTING)))
(
member
?ITEM ?COLL))
(=>
(
member
?MEMBER ?COLL)
(
and
(
temporalPart
?TIME
(
WhenFn
?ITEM))
(
instance
?MEMBER
WebListing
))))))
(
equal
(
SellersOtherItemsFn
?AGENT ?SITE ?LISTING ?TIME) ?COLL))
UXExperimentalTerms.kif 1230-1257
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
a physical
and
another physical
if
the physical
is an
instance
of
web listing
and
the physical
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 physical
and
the physical
is not
equal
to
the web listing
,
then
the physical
is a
member
of
the collection
and
if
the other physical
is a
member
of
the collection
,
then
the time point
is a
part
of the
time
of existence of
the physical
and
the other physical
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
?PURCHASES
Collection
)
(
forall
(?MEMBER)
(=>
(
member
?MEMBER ?PURCHASES)
(
instance
?MEMBER
Buying
)))
(
exists
(?REGION)
(
and
(
instance
?REGION
GeopoliticalArea
)
(
forall
(?BUYER ?BUYING)
(=>
(
and
(
instance
?BUYER
Agent
)
(
instance
?BUYING
Buying
)
(
member
?BUYING ?PURCHASES)
(
agent
?BUYING ?BUYER))
(
located
?BUYER ?REGION))))))
(
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 3163-3189
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 the
total
of values in the
class
described by
a symbolic string
is
an entity
_PURCHASE_AMOUNT and the
value
of
the collection
is
equal
to
the entity
_PURCHASE_AMOUNT
(=>
(
and
(
instance
?SALES
Collection
)
(
forall
(?MEMBER)
(=>
(
member
?MEMBER ?SALES)
(
instance
?MEMBER
Selling
)))
(
exists
(?REGION)
(
and
(
instance
?REGION
GeopoliticalArea
)
(
forall
(?SELLER ?SELLING)
(=>
(
and
(
instance
?SELLER
Agent
)
(
instance
?SELLING
Buying
)
(
member
?SELLING ?SALES)
(
agent
?SELLING ?SELLER))
(
located
?SELLER ?REGION))))))
(
and
(
total
(
KappaFn
?AMOUNT
(
and
(
instance
?SALE
Selling
)
(
member
?SALE ?SALES)
(
transactionAmount
?SALE ?AMOUNT))) ?TOTAL_SALE_AMOUNT)
(
equal
(
GMVFn
?SALES) ?TOTAL_SALE_AMOUNT)))
UXExperimentalTerms.kif 3206-3232
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
selling
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 the
total
of values in the
class
described by
a symbolic string
is
an entity
_SALE_AMOUNT and the
value
of
the collection
is
equal
to
the entity
_SALE_AMOUNT
(=>
(
and
(
instance
?SEAT
AuditoriumSeat
)
(
part
?SEAT ?AUDITORIUM)
(
part
?STAGE ?AUDITORIUM)
(
instance
?AUDITORIUM
Auditorium
)
(
instance
?STAGE
PerformanceStage
)
(
located
?PERSON ?SEAT)
(
instance
?PERSON
Human
)
(
subclass
?SEE
Seeing
)
(
forall
(?INST)
(=>
(
instance
?INST ?SEE)
(
patient
?INST ?STAGE))))
(
capability
?SEE
agent
?PERSON))
Mid-level-ontology.kif 7011-7025
If
an object
is an
instance
of
auditorium seat
and
the object
is a
part
of
another object
and
a third object
is a
part
of
the other object
and
the other object
is an
instance
of
auditorium
and
the third object
is an
instance
of
performance stage
and
a fourth object
is
located
at
the object
and
the fourth object
is an
instance
of
human
and
a kind of process
is a
subclass
of
seeing
and for all
another process
if
the other process
is an
instance
of
a kind of process
,
then
the third object
is a
patient
of
the other process
,
then
the fourth object
is
capable
of doing
the kind of process
as a
agent
(=>
(
and
(
instance
?VISITOR
Human
)
(
instance
?COLL
Collection
)
(
forall
(?EXPERIMENTING ?EVENT)
(=>
(
and
(
instance
?EXPERIMENTING
Experimenting
)
(
instance
?EVENT
Process
)
(
member
?EVENT
(
QualifyingEventsFn
?EXPERIMENT))
(
capability
?EVENT
experiencer
?VISITOR))
(
member
?EVENT ?COLL)))
(=>
(
member
?PROC ?COLL)
(
and
(
instance
?PROC
Process
)
(
exists
(?EXP)
(
and
(
instance
?EXP
Experimenting
)
(
member
?PROC
(
QualifyingEventsFn
?EXP))
(
capability
?PROC
experiencer
?VISITOR))))))
(
equal
(
QualifiedTreatmentsFn
?VISITOR) ?COLL))
UXExperimentalTerms.kif 4448-4471
If
a human
is an
instance
of
human
and
a collection
is an
instance
of
collection
and for all
an entity
and
a kind of process
if
the entity
is an
instance
of
experimenting
and
a kind of process
is an
instance
of
process
and
the kind of process
is a
member
of
events
in
an experimenting
and
the human
is
capable
of doing
the kind of process
as a
experiencer
,
then
the kind of process
is a
member
of
the collection
and
if
another kind of process
is a
member
of
the collection
,
then
another kind of process
is an
instance
of
process
and there exists
another experimenting
such that
the other experimenting
is an
instance
of
experimenting
and
the other kind of process
is a
member
of
events
in
the other experimenting
and
the human
is
capable
of doing
the other kind of process
as a
experiencer
,
then all the processes
the human
is
qualified
for is
equal
to
the collection
(=>
(
and
(
instance
?VISITOR
Human
)
(
instance
?QPVIEWS
Collection
)
(
forall
(?PAGE ?ACCESSING ?EXPERIMENT)
(=>
(
and
(
instance
?PAGE
WebPage
)
(
instance
?ACCESSING
AccessingWebPage
)
(
instance
?EXPERIMENT
Experimenting
)
(
agent
?ACCESSING ?VISITOR)
(
patient
?ACCESSING ?PAGE)
(
treatedPage
?PAGE ?EXPERIMENT))
(
member
?ACCESSING ?QPVIEWS))))
(
equal
?QPVIEWS
(
QPViewsFn
?VISITOR)))
UXExperimentalTerms.kif 4382-4397
If
a human
is an
instance
of
human
and
a collection
is an
instance
of
collection
and for all
a WebPage
,
a process
and
an experimenting
if
the WebPage
is an
instance
of
WebPage
and
the process
is an
instance
of
AccessingWebPage
and
the experimenting
is an
instance
of
experimenting
and
the human
is an
agent
of
the process
and
the WebPage
is a
patient
of
the process
and
the WebPage
is the object of study of
the experimenting
,
then
the process
is a
member
of
the collection
,
then
the collection
is
equal
to all the
treated
web
page
views from
the human
(=>
(
and
(
instance
?VISITS
Collection
)
(
instance
?HYPERLINK
HypertextLink
)
(
forall
(?ACCESSING)
(
and
(
member
?ACCESSING ?PAGE)
(
and
(
instance
?ACCESSING
AccessingWebPage
)
(
component
?PAGE ?HYPERLINK)))))
(
exists
(?CLICKS)
(
and
(
instance
?CLICKS
Collection
)
(
forall
(?CLICK)
(=>
(
and
(
instance
?CLICK
RequestingHyperlink
)
(
patient
?CLICK ?HYPERLINK))
(
member
?CLICK ?CLICKS)))
(
equal
(
ClickThroughRateFn
?VISITS ?HYPERLINK)
(
DivisionFn
(
CardinalityFn
?CLICKS)
(
CardinalityFn
?VISITS))))))
UXExperimentalTerms.kif 3541-3564
If
a collection
is an
instance
of
collection
and
a hyperlink
is an
instance
of
hyperlink
and for all
a physical
the physical
is a
member
of
another collection
and
the physical
is an
instance
of
AccessingWebPage
and
the other collection
is a
component
of
the hyperlink
,
then there exists
a third collection
such that
the third collection
is an
instance
of
collection
and for all
a process
if
the process
is an
instance
of
RequestingHyperlink
and
the hyperlink
is a
patient
of
the process
,
then
the process
is a
member
of
the third collection
and the
rate
of clicking through
the hyperlink
in
the collection
is
equal
to the number of
instances
in
the third collection
and the number of
instances
in
the collection
(=>
(
and
(
instance
?VISITS
Collection
)
(
instance
?PURCHASES
Collection
)
(
subCollection
?PURCHASES ?VISITS)
(
forall
(?MEMBER)
(=>
(
member
?MEMBER ?VISITS)
(
instance
?MEMBER
AccessingWebPage
)))
(
forall
(?BUYING ?VISITOR ?ACCESSING ?BUYING ?PAGE)
(=>
(
and
(
instance
?VISITOR
Human
)
(
instance
?BUYING
Buying
)
(
instance
?ACCESSING
AccessingWebPage
)
(
instance
?PAGE
WebPage
)
(
member
?ACCESSING ?VISITS)
(
destination
?ACCESSING ?PAGE)
(
agent
?BUYING ?VISITOR)
(
agent
?ACCESSING ?VISITOR)
(
during
(
WhenFn
?BUYING)
(
WhenFn
?ACCESSING))
(
instrument
?BUYING ?PAGE))
(
member
?BUYING ?PURCHASES))))
(
equal
(
SCRFn
?VISITS ?INTERVAL)
(
DivisionFn
(
CardinalityFn
(
KappaFn
?PURCHASE_IN_INTERVAL
(
and
(
member
?PURCHASE_IN_INTERVAL ?PURCHASES)
(
during
(
WhenFn
?PURCHASE_IN_INTERVAL) ?INTERVAL))))
(
CardinalityFn
(
KappaFn
?VISIT_IN_INTERVAL
(
and
(
member
?VISIT_IN_INTERVAL ?VISITS)
(
during
(
WhenFn
?PURCHASE_IN_INTERVAL) ?INTERVAL)))))))
UXExperimentalTerms.kif 3876-3911
If
a collection
is an
instance
of
collection
and
another collection
is an
instance
of
collection
and
the other collection
is a proper
sub
-collection of
the collection
and for all
a physical
if
the physical
is a
member
of
the collection
,
then
the physical
is an
instance
of
AccessingWebPage
and for all
a process
,
an agent
,, ,
another process
,, ,
the process
and
an object
if
the agent
is an
instance
of
human
and
the process
is an
instance
of
buying
and
the other process
is an
instance
of
AccessingWebPage
and
the object
is an
instance
of
WebPage
and
the other process
is a
member
of
the collection
and
the other process
end
s up at
the object
and
the agent
is an
agent
of
the process
and
the agent
is an
agent
of
the other process
and the
time
of existence of
the process
takes place
during
the
time
of existence of
the other process
and
the object
is an
instrument
for
the process
,
then
the process
is a
member
of
the other collection
,
then
purchases
made in
the collection
during
a time interval
is
equal
to the number of
instances
in the
class
described by
an entity
_IN_INTERVAL and the number of
instances
in the
class
described by
another entity
_IN_INTERVAL
consequent
(<=>
(
and
(
instance
?Y
(
YearFn
?YEAR))
(
equal
(
MaleLifeExpectancyAtBirthFn
?AREA ?Y) ?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) ?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 372-405
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 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
(<=>
(
average
?LIST1 ?AVERAGE)
(
exists
(?LIST2)
(
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 289-310
A real number
is an
average
of
a list
if and only if there exists
another list
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
a positive integer
if
the positive integer
is a
member
of
the other list
,
then there exist
another real number
,
the other real number
MINUSONE,, ,
another positive integer
and
a third 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 positive integer
th
element
of
the other list
is
equal
to
the other real number
and
the other positive integer
is a
member
of
the list
and
the other real number
is
equal
to
the other positive integer
th
element
of
the list
and
the third 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 third positive integer
th
element
of
the other list
and
the positive integer
is
equal
to (
the other positive integer
and
the third positive integer
)
and
a fourth positive integer
is
equal
to
length
of
the other list
and
the real number
is
equal
to
the fourth positive integer
th
element
of
the other list
and
the fourth positive integer
(<=>
(
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 418-449
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 327-357
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
(<=>
(
instance
?OBJ
SelfConnectedObject
)
(
forall
(?PART1 ?PART2)
(=>
(
equal
?OBJ
(
MereologicalSumFn
?PART1 ?PART2))
(
connected
?PART1 ?PART2))))
Merge.kif 9413-9418
An object
is an
instance
of
self connected object
if and only if for all
another object
and
a third object
if
the object
is
equal
to the
union
of the parts of
the other object
and
the third object
,
then
the other object
is
connected
to
the third object
(<=>
(
larger
?OBJ1 ?OBJ2)
(
forall
(?QUANT1 ?QUANT2 ?UNIT)
(=>
(
and
(
measure
?OBJ1
(
MeasureFn
?QUANT1 ?UNIT))
(
measure
?OBJ2
(
MeasureFn
?QUANT2 ?UNIT))
(
instance
?UNIT
UnitOfLength
))
(
greaterThan
?QUANT1 ?QUANT2))))
Merge.kif 7662-7670
An object
is
larger
than
another object
if and only if for all
a real number
,
another real number
and
an unit of measure
if the
measure
of
the object
is
the real number
the unit of measure
(s) and the
measure
of
the other object
is
the other real number
the unit of measure
(s) and
the unit of measure
is an
instance
of
UnitOfLength
,
then
the real number
is
greater
than
the other real number
(<=>
(
subCollection
?COLL1 ?COLL2)
(
forall
(?MEMBER)
(=>
(
member
?MEMBER ?COLL1)
(
member
?MEMBER ?COLL2))))
Merge.kif 1250-1255
A collection
is a proper
sub
-collection of
another collection
if and only if for all
a physical
if
the physical
is a
member
of
the collection
,
then
the physical
is a
member
of
the other collection
(=>
(
allRoomsPhysicalAmenity
?INV ?OBJ)
(
forall
(?X)
(=>
(
memberType
?INV ?X)
(
roomAmenity
?X ?OBJ))))
Hotel.kif 166-171
If
all
rooms
in
a room inventory
have
a kind of physical
,
then for all
a kind of hotel unit
if
a kind of hotel unit
is a
member
type of
the room inventory
,
then
a kind of physical
is an
amenity
in
the kind of hotel unit
(=>
(
allRoomsPolicy
?INV ?POLICY)
(
forall
(?X)
(=>
(
memberType
?INV ?X)
(
roomPolicy
?X ?POLICY))))
Hotel.kif 228-233
If all rooms in
a room inventory
have policy
a policy
,
then for all
a kind of hotel unit
if
a kind of hotel unit
is a
member
type of
the room inventory
,
then
the policy
is a
policy
that applies to
the kind of hotel unit
(=>
(
allRoomsServiceAmenity
?INV ?OBJ)
(
forall
(?X)
(=>
(
memberType
?INV ?X)
(
roomAmenity
?X ?OBJ))))
Hotel.kif 213-218
If all rooms in
a room inventory
have service
a kind of physical
,
then for all
a kind of hotel unit
if
a kind of hotel unit
is a
member
type of
the room inventory
,
then
a kind of physical
is an
amenity
in
the kind of hotel unit
(=>
(
and
(
attribute
?OBJ ?SPHERE)
(
instance
?SPHERE
Sphere
))
(
exists
(?CENTER ?DIST)
(
forall
(?PT)
(=>
(
pointOfFigure
?PT ?OBJ)
(
geometricDistance
?PT ?CENTER ?DIST)))))
Mid-level-ontology.kif 4712-4720
If
an attribute
is an
attribute
of
an object
and
the attribute
is an
instance
of
sphere
,
then there exist
a geometric point
and
a length measure
such that for all
another geometric point
if
the other geometric point
is a
vertex
of
the object
,
then
the other geometric point
is
geometric
distance
the geometric point
for
the length measure
(=>
(
and
(
attribute
?OBJ
Monochromatic
)
(
superficialPart
?PART ?OBJ)
(
attribute
?PART ?COLOR)
(
instance
?COLOR
PrimaryColor
))
(
forall
(?ELEMENT)
(=>
(
superficialPart
?ELEMENT ?OBJ)
(
attribute
?ELEMENT ?COLOR))))
Merge.kif 17419-17428
If
monochromatic
is an
attribute
of
an object
and
another object
is a
superficial
part of
the object
and
an attribute
is an
attribute
of
the other object
and
the attribute
is an
instance
of
primary color
,
then for all
a third object
if
the third object
is a
superficial
part of
the object
,
then
the attribute
is an
attribute
of
the third object
(=>
(
and
(
attribute
?X
DutyFree
)
(
instance
?X
Store
))
(
forall
(?OBJ)
(=>
(
and
(
instance
?SELL
Selling
)
(
patient
?SELL ?OBJ)
(
located
?SELL ?X)
(
instance
?OBJ
Product
))
(
attribute
?OBJ
DutyFree
))))
Hotel.kif 1454-1465
If
duty free
is an
attribute
of
an object
and
the object
is an
instance
of
store
,
then for all
another object
if
a process
is an
instance
of
selling
and
the other object
is a
patient
of
the process
and
the process
is
located
at
the object
and
the other object
is an
instance
of
product
,
then
duty free
is an
attribute
of
the other object
(=>
(
and
(
citizen
?AGENT ?POLITY)
(
subProposition
UniversalSuffrageLaw
(
RegionalLawFn
?POLITY)))
(
confersRight
(
forall
(?VOTINGAGE ?AGE ?ELECTION)
(=>
(
and
(
citizen
?AGENT ?POLITY)
(
suffrageAgeMinimum
?POLITY
(
MeasureFn
?VOTINGAGE
YearDuration
))
(
age
?AGENT
(
MeasureFn
?AGE
YearDuration
))
(
greaterThanOrEqualTo
?AGE ?VOTINGAGE)
(
instance
?ELECTION
(
ElectionFn
?POLITY)))
(
exists
(?VOTING)
(
and
(
instance
?VOTING
(
VotingFn
?ELECTION))
(
agent
?VOTING ?AGENT)))))
(
RegionalLawFn
?POLITY) ?AGENT))
Government.kif 1117-1137
If
a human
is a
citizen
of
a nation
and
universal suffrage law
is a
sub
-proposition of the
regional
law of
the nation
,
then the
regional
law of
the nation
allow
s
the human
to perform task of the type for all
an entity
,
another entity
and
a third entity
if
the human
is a
citizen
of
the nation
and
the entity
year duration
(s) is a
suffrage
age minimum of
the nation
and the
age
of
the human
is
the other entity
year duration
(s) and
the other entity
is
greater
than or equal to
the entity
and
the third entity
is an
instance
of the
election
of
the nation
,
then there exists
a fourth entity
such that
the fourth entity
is an
instance
of the
voting
of
the third entity
and
the human
is an
agent
of
the fourth entity
(=>
(
and
(
element
?X
(
PropertyFn
?HOTEL))
(
instance
?X
RoomInventory
))
(
forall
(?Y)
(=>
(
member
?Y ?X)
(
element
?Y
(
PropertyFn
?HOTEL)))))
Hotel.kif 142-149
If
a collection
is an
element
of
belongings
of
an agent
and
the collection
is an
instance
of
room inventory
,
then for all
a physical
if
the physical
is a
member
of
the collection
,
then
the physical
is an
element
of
belongings
of
the agent
(=>
(
and
(
equal
(
GreatestCommonDivisorFn
@ROW) ?NUMBER)
(
not
(
equal
?NUMBER 0)))
(
forall
(?ELEMENT)
(=>
(
inList
?ELEMENT
(
ListFn
@ROW))
(
equal
(
RemainderFn
?ELEMENT ?NUMBER) 0))))
Merge.kif 4765-4776
If the
greatest
common divisor of @ROW is
equal
to
an integer
and
the integer
is not
equal
to 0,
then for all
another integer
if
the other integer
is a
member
of (@ROW),
then
the other integer
mod
the integer
is
equal
to 0
(=>
(
and
(
equal
(
GreatestCommonDivisorFn
@ROW) ?NUMBER)
(
not
(
equal
?NUMBER 0)))
(
not
(
exists
(?GREATER)
(
and
(
greaterThan
?GREATER ?NUMBER)
(
forall
(?ELEMENT)
(=>
(
inList
?ELEMENT
(
ListFn
@ROW))
(
equal
(
RemainderFn
?ELEMENT ?GREATER) 0)))))))
Merge.kif 4778-4792
If the
greatest
common divisor of @ROW is
equal
to
an integer
and
the integer
is not
equal
to 0,
then there doesn't exist
another integer
such that
the other integer
is
greater
than
the integer
and for all
a third integer
if
the third integer
is a
member
of (@ROW),
then
the third integer
mod
the other integer
is
equal
to 0
(=>
(
and
(
equal
(
LeastCommonMultipleFn
@ROW) ?NUMBER)
(
not
(
equal
?NUMBER 0)))
(
forall
(?ELEMENT)
(=>
(
inList
?ELEMENT
(
ListFn
@ROW))
(
equal
(
RemainderFn
?NUMBER ?ELEMENT) 0))))
Merge.kif 4850-4860
If the
least
common multiple of @ROW is
equal
to
an integer
and
the integer
is not
equal
to 0,
then for all
another integer
if
the other integer
is a
member
of (@ROW),
then
the integer
mod
the other integer
is
equal
to 0
(=>
(
and
(
equal
(
LeastCommonMultipleFn
@ROW) ?NUMBER)
(
not
(
equal
?NUMBER 0)))
(
not
(
exists
(?LESS)
(
and
(
lessThan
?LESS ?NUMBER)
(
forall
(?ELEMENT)
(=>
(
inList
?ELEMENT
(
ListFn
@ROW))
(
equal
(
RemainderFn
?LESS ?ELEMENT) 0)))))))
Merge.kif 4862-4876
If the
least
common multiple of @ROW is
equal
to
an integer
and
the integer
is not
equal
to 0,
then there doesn't exist
another integer
such that
the other integer
is
less
than
the integer
and for all
a third integer
if
the third integer
is a
member
of (@ROW),
then
the other integer
mod
the third integer
is
equal
to 0
(=>
(
and
(
equal
(
MaximalWeightedPathFn
?NODE1 ?NODE2) ?PATH)
(
equal
(
PathWeightFn
?PATH) ?NUMBER1))
(
forall
(?PATH2)
(=>
(
and
(
instance
?PATH2
(
GraphPathFn
?NODE1 ?NODE2))
(
equal
(
PathWeightFn
?PATH2) ?NUMBER2))
(
lessThanOrEqualTo
?NUMBER2 ?NUMBER1))))
Merge.kif 5945-5954
If the
highest
cost
path
between
a graph node
and
another graph node
is
equal
to
a graph path
and the
value
of
the graph path
is
equal
to
a real number
,
then for all
the graph path
2
if
the graph path
2 is an
instance
of the
set
of paths between
the graph node
and
the other graph node
and the
value
of
the graph path
2 is
equal
to
another real number
,
then
the other real number
is
less
than or equal to
the real number
(=>
(
and
(
equal
(
MinimalWeightedPathFn
?NODE1 ?NODE2) ?PATH)
(
equal
(
PathWeightFn
?PATH) ?NUMBER1))
(
forall
(?PATH2)
(=>
(
and
(
instance
?PATH2
(
GraphPathFn
?NODE1 ?NODE2))
(
equal
(
PathWeightFn
?PATH2) ?NUMBER2))
(
greaterThanOrEqualTo
?NUMBER2 ?NUMBER1))))
Merge.kif 5920-5929
If the
lowest
cost
path
between
a graph node
and
another graph node
is
equal
to
a graph path
and the
value
of
the graph path
is
equal
to
a real number
,
then for all
the graph path
2
if
the graph path
2 is an
instance
of the
set
of paths between
the graph node
and
the other graph node
and the
value
of
the graph path
2 is
equal
to
another real number
,
then
the other real number
is
greater
than or equal to
the real number
(=>
(
and
(
equal
?D
(
AlbumCopiesFn
?A ?DS))
(
instance
?X ?D))
(
forall
(?S)
(=>
(
inList
?S ?A)
(
exists
(?C)
(
and
(
copy
?C ?S)
(
stored
?C ?D))))))
Music.kif 931-941
If
a kind of DataStorageDevice
is
equal
to the
set
of copies on
a kind of DataStorageDevice
S of
an album
and
an entity
is an
instance
of
the kind of DataStorageDevice
,
then for all
an object
if
the object
is a
member
of
the album
,
then there exists
a content bearing object
such that
the content bearing object
is a
copy
of
the object
and
the content bearing object
is
stored
on
the kind of DataStorageDevice
(=>
(
and
(
hole
?HOLE1 ?OBJ)
(
hole
?HOLE2 ?OBJ))
(
forall
(?HOLE3)
(=>
(
part
?HOLE3
(
MereologicalSumFn
?HOLE1 ?HOLE2))
(
hole
?HOLE3 ?OBJ))))
Merge.kif 9801-9808
If
a hole
is a
hole
in
a self connected object
and
another hole
is a
hole
in
the self connected object
,
then for all
a third hole
if
the third hole
is a
part
of the
union
of the parts of
the hole
and
the other hole
,
then
the third hole
is a
hole
in
the self connected object
(=>
(
and
(
instance
?AGENT
Agent
)
(
instance
?SITE
WebSite
))
(
exists
(?COLL)
(
and
(
instance
?COLL
Collection
)
(
forall
(?LISTING)
(=>
(
and
(
instance
?LISTING
WebListing
)
(
hostedOn
?LISTING ?SITE)
(
listingSeller
?LISTING ?AGENT))
(
member
?LISTING ?COLL)))
(
equal
(
SellersItemsFn
?AGENT ?SITE) ?COLL))))
UXExperimentalTerms.kif 1189-1205
If
an agent
is an
instance
of
agent
and
a WebSite
is an
instance
of
WebSite
,
then there exists
a collection
such that
the collection
is an
instance
of
collection
and for all
a web listing
if
the web listing
is an
instance
of
web listing
and
the web listing
is
hosted
on
the WebSite
and
the agent
sells
the web listing
,
then
the web listing
is a
member
of
the collection
and items for
sale
by
the agent
at
the WebSite
is
equal
to
the collection
(=>
(
and
(
instance
?CHIN
Chin
)
(
instance
?FACE
Face
)
(
part
?CHIN ?FACE))
(
forall
(?PART)
(=>
(
and
(
part
?PART ?FACE)
(
not
(
part
?PART ?CHIN)))
(
orientation
?PART ?CHIN
Below
))))
Mid-level-ontology.kif 12391-12402
If
an object
is an
instance
of
chin
and
another object
is an
instance
of
face
and
the object
is a
part
of
the other object
,
then for all
a third object
if
the third object
is a
part
of
the other object
and
the third object
is not a
part
of
the object
,
then
the third object
is
below
to
the object
Display limited to 25 items.
Show next 25
Display limited to 25 items.
Show next 25
statement
(
containsInformation
(
forall
(?AGENT ?VOTER ?ELECTION ?VOTING)
(=>
(
and
(
instance
?ELECTION
(
ElectionFn
?AGENT))
(
instance
?VOTING
(
VotingFn
?ELECTION))
(
agent
?VOTING ?VOTER))
(
attribute
?VOTER
Male
)))
ExclusiveMaleSuffrage
)
Government.kif 1226-1233
For all ?AGENT, ?VOTER,, , ?ELECTION and ?VOTING
if ?ELECTION is an
instance
of the
election
of ?AGENT and ?VOTING is an
instance
of the
voting
of ?ELECTION and ?VOTER is an
agent
of ?VOTING,
then
male
is an
attribute
of ?VOTER
contain
s information
exclusive male suffrage
(
containsInformation
(
forall
(?COUNTRY ?ELECTION ?VOTING ?VOTER)
(=>
(
and
(
instance
?COUNTRY
Nation
)
(
instance
?ELECTION
(
ElectionFn
?COUNTRY))
(
instance
?VOTING
(
VotingFn
?ELECTION))
(
agent
?VOTING ?VOTER))
(
citizen
?VOTER ?COUNTRY)))
VoterCitizenshipRequirement
)
Government.kif 908-916
For all ?COUNTRY, ?ELECTION,, , ?VOTING and ?VOTER
if ?COUNTRY is an
instance
of
nation
and ?ELECTION is an
instance
of the
election
of ?COUNTRY and ?VOTING is an
instance
of the
voting
of ?ELECTION and ?VOTER is an
agent
of ?VOTING,
then ?VOTER is a
citizen
of ?COUNTRY
contain
s information
voter citizenship requirement
(
containsInformation
(
forall
(?POLITY ?AGENT ?ELECTION ?VOTINGAGE ?AGE)
(=>
(
and
(
citizen
?AGENT ?POLITY)
(
suffrageAgeMinimum
?POLITY
(
MeasureFn
?VOTINGAGE
YearDuration
))
(
age
?AGENT
(
MeasureFn
?AGE
YearDuration
))
(
greaterThanOrEqualTo
?AGE ?VOTINGAGE)
(
instance
?ELECTION
(
ElectionFn
?POLITY)))
(
capability
(
VotingFn
?ELECTION)
agent
?AGENT)))
UniversalSuffrageLaw
)
Government.kif 1077-1088
For all ?POLITY, ?AGENT,, , ?ELECTION,, , ?VOTINGAGE and ?AGE
if ?AGENT is a
citizen
of ?POLITY and ?VOTINGAGE
year duration
(s) is a
suffrage
age minimum of ?POLITY and the
age
of ?AGENT 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 ?AGENT is
capable
of doing the
voting
of ?ELECTION as a
agent
contain
s information
universal suffrage law
(
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 1145-1159
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
(
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 1968-1976
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
appearance as argument number 0
(
forall
(?NUMBER)
(
equal
(
MeasureFn
?NUMBER
OunceMass
)
(
MeasureFn
(
DivisionFn
?NUMBER 16.0)
PoundMass
)))
Mid-level-ontology.kif 12794-12797
For all
a real number
the real number
Ounce
(s) is
equal
to
the real number
and 16.0
pound mass
(s)
(
forall
(?NUMBER)
(
equal
(
PredecessorFn
?NUMBER)
(
SubtractionFn
?NUMBER 1)))
Merge.kif 4640-4641
For all
an integer
(
the integer
+2) is
equal
to (
the integer
and 1)
(
forall
(?NUMBER)
(
equal
(
SuccessorFn
?NUMBER)
(
AdditionFn
?NUMBER 1)))
Merge.kif 4624-4625
For all
an integer
(
the integer
+1) is
equal
to (
the integer
and 1)
(
forall
(@ROW ?ITEM)
(
equal
(
ListLengthFn
(
ListFn
@ROW ?ITEM))
(
SuccessorFn
(
ListLengthFn
(
ListFn
@ROW)))))
Merge.kif 2965-2968
For all @ROW and
another entity
length
of (@ROW and
the other entity
) is
equal
to (
length
of (@ROW)+1)
(
forall
(@ROW ?ITEM)
(
equal
(
ListOrderFn
(
ListFn
@ROW ?ITEM)
(
ListLengthFn
(
ListFn
@ROW ?ITEM))) ?ITEM))
Merge.kif 2970-2974
For all @ROW and
another entity
length
of (@ROW and
the other entity
)th
element
of (@ROW and
the other entity
) is
equal
to
the other entity
(
forall
(@ROW ?ITEM)
(
initialList
(
ListFn
@ROW)
(
ListFn
@ROW ?ITEM)))
Merge.kif 3244-3245
For all @ROW and
another entity
(@ROW)
start
s (@ROW and
the other entity
)
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