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
forall
Sigma KEE - forall
forall
appearance as argument number 2
(
termFormat
EnglishLanguage
forall
"forall")
domainEnglishFormat.kif 65833-65833
antecedent
(<=>
(
holdsDuring
?T
(
and
(
instance
?PERSON
Human
)
(
forall
(?ORG)
(
not
(
employs
?ORG ?PERSON)))))
(
holdsDuring
?T
(
attribute
?PERSON
Unemployed
)))
Merge.kif 17254-17262
Entidade
e' uma
instancia
de
Humano
Entidade
Entidade
nao
emprega
%n
Entidade
vale
durante
Posicao Temporal
Unemployed
e' um
atributo
de
Entidade
vale
durante
Posicao Temporal
(=>
(
and
(
climateTypeInArea
?AREA
ColdClimateZone
)
(
forall
(?MO)
(
and
(
instance
?MO
Month
)
(
averageTemperatureForPeriod
?AREA ?MO
(
MeasureFn
?TEMP
CelsiusDegree
)))))
(
greaterThan
10.0 ?TEMP))
Geography.kif 1522-1530
climateTypeInArea
Area Geografica
and
ColdClimateZone
Intervalo Temporal
Intervalo Temporal
e' uma
instancia
de
Mes
averageTemperatureForPeriod
Area Geografica
,
Intervalo Temporal
and
Numero Real
CelsiusDegree
(s)
10.0 e'
maior
que
Numero Real
(=>
(
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 5993-6006
O
valor
de
Caminho do Grafo
e'
igual
a
Numero Real
Arco do Grafo
e' uma &parte de
Caminho do Grafo
Arco do Grafo
e' uma &parte de
Caminho do Grafo
o
valor
de
Arco do Grafo
e'
Numero Real
o
valor
de
Arco do Grafo
e'
Numero Real
Elemento do Grafo
Elemento do Grafo
e' uma &parte de
Caminho do Grafo
Elemento do Grafo
e'
igual
a
Arco do Grafo
Elemento do Grafo
e'
igual
a
Arco do Grafo
o
valor
de
Caminho do Grafo
e'
igual
a (
Numero Real
+
Numero Real
)
(=>
(
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 5979-5991
O
valor
de
Caminho do Grafo
e'
igual
a
Numero Real
Caminho do Grafo
e' um
sub
-grafo de
Caminho do Grafo
Arco do Grafo
e' uma &parte de
Caminho do Grafo
o
valor
de
Arco do Grafo
e'
Numero Real
Elemento do Grafo
Elemento do Grafo
e' uma &parte de
Caminho do Grafo
Elemento do Grafo
e' uma &parte de
Caminho do Grafo
Elemento do Grafo
e'
igual
a
Arco do Grafo
Numero Real
e'
igual
a (o
valor
de
Caminho do Grafo
+
Numero Real
)
(=>
(
and
(
instance
?AUCTIONS
Collection
)
(
forall
(?AUC)
(=>
(
member
?AUC ?AUCTIONS)
(
instance
?AUC
Auctioning
))))
(
exists
(?AMOUNT ?TOTAL_PURCHASE_AMOUNT)
(
and
(
total
(
KappaFn
?AMOUNT
(
transactionAmount
?AUC ?AMOUNT)) ?TOTAL_PURCHASE_AMOUNT)
(
equal
(
AuctionGMBFn
?AUCTIONS) ?TOTAL_PURCHASE_AMOUNT))))
UXExperimentalTerms.kif 3202-3215
Colecao
e' uma
instancia
de
Colecao
Fisico
Fisico
e'
membro
de
Colecao
Fisico
e' uma
instancia
de
Auctioning
Sequencia Simbolica
Entidade
_PURCHASE_AMOUNT
total
a
classe
descrita por
Sequencia Simbolica
and
Entidade
_PURCHASE_AMOUNT
AuctionGMBFn
Colecao
e'
igual
a
Entidade
_PURCHASE_AMOUNT
(=>
(
and
(
instance
?COLL
Collection
)
(
forall
(?MEMBER)
(=>
(
member
?MEMBER ?COLL)
(
instance
?MEMBER
FinancialTransaction
))))
(
exists
(?ITEM ?BUYING)
(
equal
(
CardinalityFn
(
KappaFn
?ITEM
(
and
(
instance
?ITEM
Physical
)
(
instance
?BUYING
Buying
)
(
member
?BUYING ?COLL)
(
patient
?BUYING ?ITEM))))
(
BoughtItemsFn
?COLL))))
UXExperimentalTerms.kif 2887-2903
Colecao
e' uma
instancia
de
Colecao
Fisico
Fisico
e'
membro
de
Colecao
Fisico
e' uma
instancia
de
Transacao Financeira
Sequencia Simbolica
Entidade
o numero de
instancias
dentro de a
classe
descrita por
Sequencia Simbolica
e'
igual
a
BoughtItemsFn
Colecao
(=>
(
and
(
instance
?COLL
Collection
)
(
forall
(?MEMBER)
(=>
(
member
?MEMBER ?COLL)
(
instance
?MEMBER
WebListing
))))
(
equal
(
DivisionFn
(
CardinalityFn
(
exists
(?LISTING ?SITE ?ITEM)
(
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 2845-2870
Colecao
e' uma
instancia
de
Colecao
Fisico
Fisico
e'
membro
de
Colecao
Fisico
e' uma
instancia
de
WebListing
o numero de
instancias
dentro de
Entidade
Entidade
and
Entidade
a
classe
descrita por
Entidade
+ o numero de
instancias
dentro de
Colecao
e'
igual
a
BidCountFn
Colecao
(=>
(
and
(
instance
?COLL
Collection
)
(
forall
(?MEMBER)
(=>
(
member
?MEMBER ?COLL)
(
instance
?MEMBER
WebListing
))))
(
exists
(?BIDDING ?ITEM ?LISTING ?BIDDING)
(
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 2922-2940
Colecao
e' uma
instancia
de
Colecao
Fisico
Fisico
e'
membro
de
Colecao
Fisico
e' uma
instancia
de
WebListing
Sequencia Simbolica
Entidade
,
Entidade
and
Sequencia Simbolica
o numero de
instancias
dentro de a
classe
descrita por
Sequencia Simbolica
e'
igual
a
BidCountFn
Colecao
(=>
(
and
(
instance
?COLL
Collection
)
(
instance
?SITE
WebSite
)
(
instance
?AGENT
AutonomousAgent
)
(
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 1033-1060
Colecao
e' uma
instancia
de
Colecao
WebSite
e' uma
instancia
de
WebSite
AutonomousAgent
e' uma
instancia
de
AutonomousAgent
WebListing
e' uma
instancia
de
WebListing
Ponto no tempo
e' uma
instancia
de
Ponto no tempo
listingSeller
WebListing
and
AutonomousAgent
WebListing
e'
membro
de
Colecao
Fisico
Fisico
Fisico
e' uma
instancia
de
WebListing
Fisico
e'
membro
de
SellersItemsFn
AutonomousAgent
and
WebSite
Ponto no tempo
e' uma &parte de
tempo
de existencia de
Fisico
Fisico
e'
igual
a
WebListing
Fisico
e'
membro
de
Colecao
Fisico
e'
membro
de
Colecao
Ponto no tempo
e' uma &parte de
tempo
de existencia de
Fisico
Fisico
e' uma
instancia
de
WebListing
SellersOtherItemsFn
AutonomousAgent
,
WebSite
,
WebListing
and
Ponto no tempo
e'
igual
a
Colecao
(=>
(
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
Colecao
e' uma
instancia
de
Colecao
Fisico
Fisico
e'
membro
de
Colecao
Fisico
e' uma
instancia
de
Comprar
Objeto
Objeto
e' uma
instancia
de
Area Geopolitica
AutonomousAgent
Processo
AutonomousAgent
e' uma
instancia
de
AutonomousAgent
Processo
e' uma
instancia
de
Comprar
Processo
e'
membro
de
Colecao
Processo
e' um
agente
de
AutonomousAgent
AutonomousAgent
e'
situado
em
Objeto
Sequencia Simbolica
Entidade
and
Entidade
_PURCHASE_AMOUNT
total
a
classe
descrita por
Sequencia Simbolica
and
Entidade
_PURCHASE_AMOUNT
GMBFn
Colecao
e'
igual
a
Entidade
_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
AutonomousAgent
)
(
instance
?SELLING
Buying
)
(
member
?SELLING ?SALES)
(
agent
?SELLING ?SELLER))
(
located
?SELLER ?REGION))))))
(
exists
(?AMOUNT ?SALE ?TOTAL_SALE_AMOUNT)
(
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 2999-3026
Colecao
e' uma
instancia
de
Colecao
Fisico
Fisico
e'
membro
de
Colecao
Fisico
e' uma
instancia
de
Vender
Objeto
Objeto
e' uma
instancia
de
Area Geopolitica
AutonomousAgent
Processo
AutonomousAgent
e' uma
instancia
de
AutonomousAgent
Processo
e' uma
instancia
de
Comprar
Processo
e'
membro
de
Colecao
Processo
e' um
agente
de
AutonomousAgent
AutonomousAgent
e'
situado
em
Objeto
Sequencia Simbolica
Entidade
and
Entidade
_SALE_AMOUNT
total
a
classe
descrita por
Sequencia Simbolica
and
Entidade
_SALE_AMOUNT
GMVFn
Colecao
e'
igual
a
Entidade
_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 7351-7365
Objeto
e' uma
instancia
de
AuditoriumSeat
Objeto
e' uma &parte de
Objeto
Objeto
e' uma &parte de
Objeto
Objeto
e' uma
instancia
de
Auditorium
Objeto
e' uma
instancia
de
PerformanceStage
Objeto
e'
situado
em
Objeto
Objeto
e' uma
instancia
de
Humano
Processo
e' uma
sub
-classe de
Visao
Processo
Processo
e' uma
instancia
de
Processo
Objeto
e' um
patient
de
Processo
Objeto
e'
capaz
de fazer
Processo
no role
agent
(=>
(
and
(
instance
?VISITOR
Human
)
(
instance
?COLL
Collection
)
(
forall
(?EXPERIMENT ?EVENT)
(=>
(
exists
(?CLASS)
(
and
(
instance
?EXPERIMENT
Experimenting
)
(
instance
?EVENT
Process
)
(
member
?EVENT
(
QualifyingEventsFn
?EXPERIMENT))
(
instance
?EVENT ?CLASS)
(
capability
?CLASS
experiencer
?VISITOR)))
(
member
?EVENT ?COLL)))
(=>
(
member
?PROC ?COLL)
(
and
(
instance
?PROC
Process
)
(
exists
(?EXP ?PROCESS)
(
and
(
instance
?EXP
Experimenting
)
(
member
?PROC
(
QualifyingEventsFn
?EXP))
(
instance
?PROC ?PROCESS)
(
capability
?PROCESS
experiencer
?VISITOR))))))
(
equal
(
QualifiedTreatmentsFn
?VISITOR) ?COLL))
UXExperimentalTerms.kif 4241-4267
Humano
e' uma
instancia
de
Humano
Colecao
e' uma
instancia
de
Colecao
Experimenting
Fisico
Processo
Experimenting
e' uma
instancia
de
Experimenting
Fisico
e' uma
instancia
de
Processo
Fisico
e'
membro
de
QualifyingEventsFn
Experimenting
Fisico
e' uma
instancia
de
Processo
Humano
e'
capaz
de fazer
Processo
no role
experiencer
Fisico
e'
membro
de
Colecao
Fisico
e'
membro
de
Colecao
Fisico
e' uma
instancia
de
Processo
Experimenting
Fisico
ESS
Experimenting
e' uma
instancia
de
Experimenting
Fisico
e'
membro
de
QualifyingEventsFn
Experimenting
Fisico
e' uma
instancia
de
Fisico
ESS
Humano
e'
capaz
de fazer
Fisico
ESS no role
experiencer
QualifiedTreatmentsFn
Humano
e'
igual
a
Colecao
(=>
(
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 4175-4190
Humano
e' uma
instancia
de
Humano
Colecao
e' uma
instancia
de
Colecao
WebPage
Processo
and
Experimenting
WebPage
e' uma
instancia
de
WebPage
Processo
e' uma
instancia
de
AccessingWebPage
Experimenting
e' uma
instancia
de
Experimenting
Processo
e' um
agente
de
Humano
WebPage
e' um
patient
de
Processo
treatedPage
WebPage
and
Experimenting
Processo
e'
membro
de
Colecao
Colecao
e'
igual
a
QPViewsFn
Humano
(=>
(
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 3333-3356
Colecao
e' uma
instancia
de
Colecao
Objeto Corpuscular
e' uma
instancia
de
HypertextLink
Fisico
Fisico
e'
membro
de
Colecao
Fisico
e' uma
instancia
de
AccessingWebPage
Colecao
e' um
componente
de
Objeto Corpuscular
Colecao
Colecao
e' uma
instancia
de
Colecao
Processo
Processo
e' uma
instancia
de
RequestingHyperlink
Objeto Corpuscular
e' um
patient
de
Processo
Processo
e'
membro
de
Colecao
ClickThroughRateFn
Colecao
and
Objeto Corpuscular
e'
igual
a o numero de
instancias
dentro de
Colecao
+ o numero de
instancias
dentro de
Colecao
(=>
(
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))))
(
exists
(?INTERVAL ?PURCHASE_IN_INTERVAL ?VISIT_IN_INTERVAL)
(
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 3668-3704
Colecao
e' uma
instancia
de
Colecao
Colecao
e' uma
instancia
de
Colecao
Colecao
e' uma
sub
-colecao de
Colecao
Fisico
Fisico
e'
membro
de
Colecao
Fisico
e' uma
instancia
de
AccessingWebPage
Processo
AutonomousAgent
,
Processo
,
Processo
and
Objeto
AutonomousAgent
e' uma
instancia
de
Humano
Processo
e' uma
instancia
de
Comprar
Processo
e' uma
instancia
de
AccessingWebPage
Objeto
e' uma
instancia
de
WebPage
Processo
e'
membro
de
Colecao
Processo
termina
em
Objeto
Processo
e' um
agente
de
AutonomousAgent
Processo
e' um
agente
de
AutonomousAgent
tempo
de existencia de
Processo
acontece
durante
tempo
de existencia de
Processo
Objeto
e' um
instrumento
para
Processo
Processo
e'
membro
de
Colecao
Intervalo Temporal
Entidade
_IN_INTERVAL and
Entidade
_IN_INTERVAL
SCRFn
Colecao
and
Intervalo Temporal
e'
igual
a o numero de
instancias
dentro de a
classe
descrita por
Entidade
_IN_INTERVAL + o numero de
instancias
dentro de a
classe
descrita por
Entidade
_IN_INTERVAL
consequent
(<=>
(
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
Ano
e' uma
instancia
de o
ano
Ano
EAR
MaleLifeExpectancyAtBirthFn
Area Geopolitica
and
Ano
e'
igual
a
Numero Real
Lista
Numero Inteiro
,
Sequencia Simbolica
,
Entidade
,
Entidade
and
Entidade
Lista
e' uma
instancia
de
Lista
comprimento
de
Lista
e' uma
instancia
de
Numero Inteiro
Lista
ITEM
Lista
ITEM e' um
membro
de
Lista
Lista
ITEM e' uma
instancia
de
Sequencia Simbolica
Entidade
Entidade
e' uma
instancia
de
Sequencia Simbolica
Entidade
e' um
membro
de
Lista
Numero Inteiro
e'
igual
a o numero de
instancias
dentro de a
classe
descrita por
Sequencia Simbolica
average
Lista
and
Numero Real
(<=>
(
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
Ano
e' uma
instancia
de o
ano
Numero Inteiro
FemaleLifeExpectancyAtBirthFn
Area Geopolitica
and
Ano
e'
igual
a
Numero Real
Lista
Numero Inteiro
,
Sequencia Simbolica
,
Entidade
,
Entidade
and
Entidade
Lista
e' uma
instancia
de
Lista
comprimento
de
Lista
e' uma
instancia
de
Numero Inteiro
Lista
ITEM
Lista
ITEM e' um
membro
de
Lista
Lista
ITEM e' uma
instancia
de
Sequencia Simbolica
Entidade
Entidade
e' uma
instancia
de
Sequencia Simbolica
Entidade
e' um
membro
de
Lista
Numero Inteiro
e'
igual
a o numero de
instancias
dentro de a
classe
descrita por
Sequencia Simbolica
average
Lista
and
Numero Real
(<=>
(
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
Ano
e' uma
instancia
de o
ano
Numero Inteiro
LifeExpectancyAtBirthFn
Area Geopolitica
and
Ano
e'
igual
a
Numero Real
Lista
Numero Inteiro
,
Sequencia Simbolica
,
Entidade
,
Entidade
and
Entidade
Lista
e' uma
instancia
de
Lista
comprimento
de
Lista
e' uma
instancia
de
Numero Inteiro
Lista
ITEM
Lista
ITEM e' um
membro
de
Lista
Lista
ITEM e' uma
instancia
de
Sequencia Simbolica
Entidade
Entidade
e' uma
instancia
de
Sequencia Simbolica
Entidade
e' um
membro
de
Lista
Numero Inteiro
e'
igual
a o numero de
instancias
dentro de a
classe
descrita por
Sequencia Simbolica
average
Lista
and
Numero Real
(<=>
(
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
average
Lista
and
Numero Real
Lista
Inteiro positivo
comprimento
de
Lista
e'
igual
a
comprimento
de
Lista
1th
elemento
de
Lista
e'
igual
a 1th
elemento
de
Lista
Inteiro positivo
Inteiro positivo
e' um
membro
de
Lista
Numero Real
Numero Real
MINUSONE,
Inteiro positivo
and
Inteiro positivo
Numero Real
e'
maior
que 1
Numero Real
e'
menor
ou igual a
comprimento
de
Lista
Inteiro positivo
th
elemento
de
Lista
e'
igual
a
Numero Real
Inteiro positivo
e' um
membro
de
Lista
Numero Real
e'
igual
a
Inteiro positivo
th
elemento
de
Lista
Inteiro positivo
e' um
membro
de
Lista
Numero Real
MINUSONE e'
igual
a (
Numero Real
+ 1)
Numero Real
MINUSONE e'
igual
a
Inteiro positivo
th
elemento
de
Lista
Inteiro positivo
e'
igual
a (
Inteiro positivo
+
Inteiro positivo
)
Inteiro positivo
e'
igual
a
comprimento
de
Lista
Numero Real
e'
igual
a
Inteiro positivo
th
elemento
de
Lista
+
Inteiro positivo
(<=>
(
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 7758-7766
Objeto
e'
maior
do que
Objeto
Numero Real
Numero Real
and
Unidade de Medida
a
medida
de
Objeto
e'
Numero Real
Unidade de Medida
(s) a
medida
de
Objeto
e'
Numero Real
Unidade de Medida
(s)
Unidade de Medida
e' uma
instancia
de
UnitOfLength
Numero Real
e'
maior
que
Numero Real
(<=>
(
subCollection
?COLL1 ?COLL2)
(
forall
(?MEMBER)
(=>
(
member
?MEMBER ?COLL1)
(
member
?MEMBER ?COLL2))))
Merge.kif 1297-1302
Colecao
e' uma
sub
-colecao de
Colecao
Fisico
Fisico
e'
membro
de
Colecao
Fisico
e'
membro
de
Colecao
(=>
(
allRoomsPhysicalAmenity
?INV ?OBJ)
(
forall
(?X)
(=>
(
memberType
?INV ?X)
(
roomAmenity
?X ?OBJ))))
Hotel.kif 171-176
allRoomsPhysicalAmenity
RoomInventory
and
Fisico
HotelUnit
memberType
RoomInventory
and
HotelUnit
roomAmenity
HotelUnit
and
Fisico
(=>
(
allRoomsPolicy
?INV ?POLICY)
(
forall
(?X)
(=>
(
memberType
?INV ?X)
(
roomPolicy
?X ?POLICY))))
Hotel.kif 233-238
allRoomsPolicy
RoomInventory
and
Policy
HotelUnit
memberType
RoomInventory
and
HotelUnit
roomPolicy
HotelUnit
and
Policy
(=>
(
allRoomsServiceAmenity
?INV ?OBJ)
(
forall
(?X)
(=>
(
memberType
?INV ?X)
(
roomAmenity
?X ?OBJ))))
Hotel.kif 218-223
allRoomsServiceAmenity
RoomInventory
and
Fisico
HotelUnit
memberType
RoomInventory
and
HotelUnit
roomAmenity
HotelUnit
and
Fisico
(=>
(
and
(
attribute
?OBJ ?SPHERE)
(
instance
?SPHERE
Sphere
))
(
exists
(?CENTER ?DIST)
(
forall
(?PT)
(=>
(
pointOfFigure
?PT ?OBJ)
(
geometricDistance
?PT ?CENTER ?DIST)))))
Mid-level-ontology.kif 4990-4998
Atributo
e' um
atributo
de
Objeto
Atributo
e' uma
instancia
de
Sphere
GeometricPoint
Medida de Comprimento
GeometricPoint
GeometricPoint
e' um
ponto
de
Objeto
geometricDistance
GeometricPoint
,
GeometricPoint
and
Medida de Comprimento
(=>
(
and
(
attribute
?OBJ
Monochromatic
)
(
superficialPart
?PART ?OBJ)
(
attribute
?PART ?COLOR)
(
instance
?COLOR
PrimaryColor
))
(
forall
(?ELEMENT)
(=>
(
superficialPart
?ELEMENT ?OBJ)
(
attribute
?ELEMENT ?COLOR))))
Merge.kif 17688-17697
Monochromatic
e' um
atributo
de
Objeto
Objeto
e' uma parte
superficial
de
Objeto
Atributo
e' um
atributo
de
Objeto
Atributo
e' uma
instancia
de
Cor Primaria
Objeto
Objeto
e' uma parte
superficial
de
Objeto
Atributo
e' um
atributo
de
Objeto
(=>
(
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 1132-1152
Humano
e' um
cidadao
de
Nacao
UniversalSuffrageLaw
e' uma &sub-proposicao de
RegionalLawFn
Nacao
RegionalLawFn
Nacao
autoriza
Humano
a executar tarefas de tipo
Entidade
Entidade
and
Entidade
Humano
e' um
cidadao
de
Nacao
suffrageAgeMinimum
Nacao
and
Entidade
YearDuration
(s) a
idade
de
Humano
e'
Entidade
YearDuration
(s)
Entidade
e'
maior
ou igual a
Entidade
Entidade
e' uma
instancia
de
ElectionFn
Nacao
Entidade
Entidade
e' uma
instancia
de
VotingFn
Entidade
Entidade
e' um
agente
de
Humano
(=>
(
and
(
element
?X
(
PropertyFn
?HOTEL))
(
instance
?X
RoomInventory
))
(
forall
(?Y)
(=>
(
member
?Y ?X)
(
element
?Y
(
PropertyFn
?HOTEL)))))
Hotel.kif 147-154
Colecao
e' um
elemento
de
propriedade
de
AutonomousAgent
Colecao
e' uma
instancia
de
RoomInventory
Fisico
Fisico
e'
membro
de
Colecao
Fisico
e' um
elemento
de
propriedade
de
AutonomousAgent
(=>
(
and
(
equal
(
GreatestCommonDivisorFn
@ROW) ?NUMBER)
(
not
(
equal
?NUMBER 0)))
(
forall
(?ELEMENT)
(=>
(
inList
?ELEMENT
(
ListFn
@ROW))
(
equal
(
RemainderFn
?ELEMENT ?NUMBER) 0))))
Merge.kif 4861-4872
O maior divisor comum de @ROW e'
igual
a
Numero Inteiro
Numero Inteiro
e'
igual
a 0
Numero Inteiro
Numero Inteiro
e' um
membro
de (@ROW)
Numero Inteiro
mod
Numero Inteiro
e'
igual
a 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 4874-4888
O maior divisor comum de @ROW e'
igual
a
Numero Inteiro
Numero Inteiro
e'
igual
a 0
Numero Inteiro
Numero Inteiro
e'
maior
que
Numero Inteiro
Numero Inteiro
Numero Inteiro
e' um
membro
de (@ROW)
Numero Inteiro
mod
Numero Inteiro
e'
igual
a 0
(=>
(
and
(
equal
(
LeastCommonMultipleFn
@ROW) ?NUMBER)
(
not
(
equal
?NUMBER 0)))
(
forall
(?ELEMENT)
(=>
(
inList
?ELEMENT
(
ListFn
@ROW))
(
equal
(
RemainderFn
?NUMBER ?ELEMENT) 0))))
Merge.kif 4946-4956
O minimo multiplo comum de
numero
, de
inteiro
@ROW e'
igual
a
Numero Inteiro
Numero Inteiro
e'
igual
a 0
Numero Inteiro
Numero Inteiro
e' um
membro
de (@ROW)
Numero Inteiro
mod
Numero Inteiro
e'
igual
a 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 4958-4972
O minimo multiplo comum de
numero
, de
inteiro
@ROW e'
igual
a
Numero Inteiro
Numero Inteiro
e'
igual
a 0
Numero Inteiro
Numero Inteiro
e'
menos
que
Numero Inteiro
Numero Inteiro
Numero Inteiro
e' um
membro
de (@ROW)
Numero Inteiro
mod
Numero Inteiro
e'
igual
a 0
(=>
(
and
(
equal
?D
(
AlbumCopiesFn
?A ?DS))
(
instance
?X ?D))
(
forall
(?S)
(=>
(
inList
?S ?A)
(
exists
(?C)
(
and
(
copy
?C ?S)
(
stored
?C ?X))))))
Music.kif 936-946
DataStorageDevice
e'
igual
a
AlbumCopiesFn
Album
and
DataStorageDevice
S
DataStorageDevice
e' uma
instancia
de
DataStorageDevice
Objeto
Objeto
e' um
membro
de
Album
Objeto Representendo Conteudo Abstrato
Objeto Representendo Conteudo Abstrato
e' uma
copia
exata de
Objeto
stored
Objeto Representendo Conteudo Abstrato
and
DataStorageDevice
(=>
(
and
(
hole
?HOLE1 ?OBJ)
(
hole
?HOLE2 ?OBJ))
(
forall
(?HOLE3)
(=>
(
part
?HOLE3
(
MereologicalSumFn
?HOLE1 ?HOLE2))
(
hole
?HOLE3 ?OBJ))))
Merge.kif 9894-9901
Buraco
e' um
buraco
dans
Objeto auto-conectado
Buraco
e' um
buraco
dans
Objeto auto-conectado
Buraco
Buraco
e' uma &parte de a
uniao
das partes de
Buraco
e
Buraco
Buraco
e' um
buraco
dans
Objeto auto-conectado
(=>
(
and
(
instance
?AGENT
AutonomousAgent
)
(
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 992-1008
AutonomousAgent
e' uma
instancia
de
AutonomousAgent
WebSite
e' uma
instancia
de
WebSite
Colecao
Colecao
e' uma
instancia
de
Colecao
WebListing
WebListing
e' uma
instancia
de
WebListing
hostedOn
WebListing
and
WebSite
listingSeller
WebListing
and
AutonomousAgent
WebListing
e'
membro
de
Colecao
SellersItemsFn
AutonomousAgent
and
WebSite
e'
igual
a
Colecao
(=>
(
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 12930-12941
Objeto
e' uma
instancia
de
Chin
Objeto
e' uma
instancia
de
Face
Objeto
e' uma &parte de
Objeto
Objeto
Objeto
e' uma &parte de
Objeto
Objeto
e' uma &parte de
Objeto
Objeto
e'
Below
em relacao a
Objeto
(=>
(
and
(
instance
?G
Grinding
)
(
patient
?G ?O)
(
instance
?O
CorpuscularObject
))
(
holdsDuring
(
EndFn
(
WhenFn
?G))
(
exists
(?C)
(
and
(
result
?G ?C)
(
instance
?C
Collection
)
(
forall
(?M)
(=>
(
member
?M ?C)
(
part
?M ?O)))))))
Food.kif 1012-1026
Processo
e' uma
instancia
de
Grinding
Entidade
e' um
patient
de
Processo
Entidade
e' uma
instancia
de
Objeto Corpuscular
Entidade
Entidade
e' o
resultado
de
Processo
Entidade
e' uma
instancia
de
Colecao
Entidade
Entidade
e'
membro
de
Entidade
Entidade
e' uma &parte de
Entidade
vale
durante o
fim
de
tempo
de existencia de
Processo
(=>
(
and
(
instance
?INTERVAL
TimeInterval
)
(
instance
?SITE
WebSite
))
(
exists
(?NEWBUYERS)
(
and
(
instance
?NEWBUYERS
Collection
)
(
forall
(?AGENT)
(=>
(
member
?AGENT ?NEWBUYERS)
(
and
(
exists
(?BUYING)
(
and
(
instance
?AGENT
AutonomousAgent
)
(
instance
?BUYING
Buying
)
(
agent
?BUYING ?AGENT)
(
instrument
?BUYING ?SITE)
(
during
?BUYING ?INTERVAL)))
(
not
(
exists
(?INTERVAL_BEFORE)
(
and
(
instance
?INTERVAL_BEFORE
TimeInterval
)
(
earlier
?INTERVAL_BEFORE ?INTERVAL)
(
holdsDuring
?INTERVAL_BEFORE
(
exists
(?BUYING_BEFORE)
(
and
(
instance
?BUYING_BEFORE
Buying
)
(
agent
?BUYING_BEFORE ?AGENT)
(
instrument
?BUYING_BEFORE ?SITE)
(
during
?BUYING_BEFORE ?INTERVAL))))))))))
(
equal
(
SiteWideNewBuyersFn
?INTERVAL ?SITE) ?NEWBUYERS))))
UXExperimentalTerms.kif 3376-3408
Intervalo Temporal
e' uma
instancia
de
Intervalo Temporal
WebSite
e' uma
instancia
de
WebSite
Colecao
Colecao
e' uma
instancia
de
Colecao
AutonomousAgent
AutonomousAgent
e'
membro
de
Colecao
Intervalo Temporal
AutonomousAgent
e' uma
instancia
de
AutonomousAgent
Intervalo Temporal
e' uma
instancia
de
Comprar
Intervalo Temporal
e' um
agente
de
AutonomousAgent
WebSite
e' um
instrumento
para
Intervalo Temporal
Intervalo Temporal
acontece
durante
Intervalo Temporal
Intervalo Temporal
_BEFORE
Intervalo Temporal
_BEFORE e' uma
instancia
de
Intervalo Temporal
Intervalo Temporal
_BEFORE acontence
antes
de
Intervalo Temporal
Intervalo Temporal
_BEFORE
Intervalo Temporal
_BEFORE e' uma
instancia
de
Comprar
Intervalo Temporal
_BEFORE e' um
agente
de
AutonomousAgent
WebSite
e' um
instrumento
para
Intervalo Temporal
_BEFORE
Intervalo Temporal
_BEFORE acontece
durante
Intervalo Temporal
vale
durante
Intervalo Temporal
_BEFORE
SiteWideNewBuyersFn
Intervalo Temporal
and
WebSite
e'
igual
a
Colecao
(=>
(
and
(
instance
?INTERVAL
TimeInterval
)
(
instance
?SITE
WebSite
))
(
exists
(?NEWREGISTRATIONS)
(
and
(
instance
?NEWREGISTRATIONS
Collection
)
(
forall
(?USER)
(=>
(
and
(
instance
?USER
Human
)
(
not
(
exists
(?INTERVAL_BEFORE)
(
and
(
instance
?INTERVAL_BEFORE
TimeInterval
)
(
earlier
?INTERVAL_BEFORE ?INTERVAL)
(
holdsDuring
?INTERVAL_BEFORE
(
registeredUser
?USER ?SITE)))))
(
exists
(?INTERVAL_DURING)
(
and
(
instance
?INTERVAL_DURING
TimeInterval
)
(
during
?INTERVAL_DURING ?INTERVAL)
(
holdsDuring
?INTERVAL
(
registeredUser
?USER ?SITE)))))
(
member
?USER ?NEWREGISTRATIONS)))
(
equal
?NEWREGISTRATIONS
(
SiteWideNewRegistrationsFn
?INTERVAL ?SITE)))))
UXExperimentalTerms.kif 3428-3455
Intervalo Temporal
e' uma
instancia
de
Intervalo Temporal
WebSite
e' uma
instancia
de
WebSite
Colecao
Colecao
e' uma
instancia
de
Colecao
Fisico
Fisico
e' uma
instancia
de
Humano
Intervalo Temporal
_BEFORE
Intervalo Temporal
_BEFORE e' uma
instancia
de
Intervalo Temporal
Intervalo Temporal
_BEFORE acontence
antes
de
Intervalo Temporal
registeredUser
Fisico
and
WebSite
vale
durante
Intervalo Temporal
_BEFORE
Intervalo Temporal
_DURING
Intervalo Temporal
_DURING e' uma
instancia
de
Intervalo Temporal
Intervalo Temporal
_DURING acontece
durante
Intervalo Temporal
registeredUser
Fisico
and
WebSite
vale
durante
Intervalo Temporal
Fisico
e'
membro
de
Colecao
Colecao
e'
igual
a
SiteWideNewRegistrationsFn
Intervalo Temporal
and
WebSite
(=>
(
and
(
instance
?INTERVAL
TimeInterval
)
(
instance
?SITE
WebSite
))
(
exists
(?NEWSELLERS)
(
and
(
instance
?NEWSELLERS
Collection
)
(
forall
(?AGENT)
(=>
(
member
?AGENT ?NEWSELLERS)
(
and
(
exists
(?SELLING)
(
and
(
instance
?AGENT
AutonomousAgent
)
(
instance
?SELLING
Selling
)
(
agent
?SELLING ?AGENT)
(
instrument
?SELLING ?SITE)
(
during
?SELLING ?INTERVAL)))
(
not
(
exists
(?INTERVAL_BEFORE)
(
and
(
instance
?INTERVAL_BEFORE
TimeInterval
)
(
earlier
?INTERVAL_BEFORE ?INTERVAL)
(
holdsDuring
?INTERVAL_BEFORE
(
exists
(?SELLING_BEFORE)
(
and
(
instance
?SELLING_BEFORE
Selling
)
(
agent
?SELLING_BEFORE ?AGENT)
(
instrument
?SELLING_BEFORE ?SITE)
(
during
?SELLING_BEFORE ?INTERVAL))))))))))
(
equal
(
SiteWideNewSellersFn
?INTERVAL ?SITE) ?NEWSELLERS))))
UXExperimentalTerms.kif 3475-3507
Intervalo Temporal
e' uma
instancia
de
Intervalo Temporal
WebSite
e' uma
instancia
de
WebSite
Colecao
Colecao
e' uma
instancia
de
Colecao
AutonomousAgent
AutonomousAgent
e'
membro
de
Colecao
Intervalo Temporal
AutonomousAgent
e' uma
instancia
de
AutonomousAgent
Intervalo Temporal
e' uma
instancia
de
Vender
Intervalo Temporal
e' um
agente
de
AutonomousAgent
WebSite
e' um
instrumento
para
Intervalo Temporal
Intervalo Temporal
acontece
durante
Intervalo Temporal
Intervalo Temporal
_BEFORE
Intervalo Temporal
_BEFORE e' uma
instancia
de
Intervalo Temporal
Intervalo Temporal
_BEFORE acontence
antes
de
Intervalo Temporal
Intervalo Temporal
_BEFORE
Intervalo Temporal
_BEFORE e' uma
instancia
de
Vender
Intervalo Temporal
_BEFORE e' um
agente
de
AutonomousAgent
WebSite
e' um
instrumento
para
Intervalo Temporal
_BEFORE
Intervalo Temporal
_BEFORE acontece
durante
Intervalo Temporal
vale
durante
Intervalo Temporal
_BEFORE
SiteWideNewSellersFn
Intervalo Temporal
and
WebSite
e'
igual
a
Colecao
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 1241-1248
?AGENT ?VOTER, ?ELECTION and ?VOTING
?ELECTION e' uma
instancia
de
ElectionFn
?AGENT ?VOTING e' uma
instancia
de
VotingFn
?ELECTION ?VOTING e' um
agente
de ?VOTER
Male
e' um
atributo
de ?VOTER
contem
informacao
ExclusiveMaleSuffrage
(
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 923-931
?COUNTRY ?ELECTION, ?VOTING and ?VOTER
?COUNTRY e' uma
instancia
de
Nacao
?ELECTION e' uma
instancia
de
ElectionFn
?COUNTRY ?VOTING e' uma
instancia
de
VotingFn
?ELECTION ?VOTING e' um
agente
de ?VOTER
?VOTER e' um
cidadao
de ?COUNTRY
contem
informacao
VoterCitizenshipRequirement
(
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 1092-1103
?POLITY ?AGENT, ?ELECTION, ?VOTINGAGE and ?AGE
?AGENT e' um
cidadao
de ?POLITY
suffrageAgeMinimum
?POLITY and ?VOTINGAGE
YearDuration
(s) a
idade
de ?AGENT e' ?AGE
YearDuration
(s) ?AGE e'
maior
ou igual a ?VOTINGAGE ?ELECTION e' uma
instancia
de
ElectionFn
?POLITY
?AGENT e'
capaz
de fazer
VotingFn
?ELECTION no role
agent
contem
informacao
UniversalSuffrageLaw
(
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 1160-1174
?POLITY ?VOTER, ?ELECTION, ?VOTINGAGE and ?AGE
?VOTER e' um
cidadao
de ?POLITY
suffrageAgeMinimum
?POLITY and ?VOTINGAGE
YearDuration
(s) a
idade
de ?VOTER e' ?AGE
YearDuration
(s) ?AGE e'
maior
ou igual a ?VOTINGAGE ?ELECTION e' uma
instancia
de
ElectionFn
?POLITY
?VOTING ?VOTING e' uma
instancia
de
VotingFn
?ELECTION ?VOTING e' um
agente
de ?VOTER
contem
informacao
CompulsorySuffrageLaw
(
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
Intervalo Temporal
Intervalo Temporal
e' uma
instancia
de
Intervalo Temporal
Intervalo Temporal
termina
em
tempo
de existencia de
JesusOfNazareth
Intervalo Temporal
comeca
em
tempo
de existencia de
TwelveApostles
Entidade
Entidade
e'
membro
de
TwelveApostles
vale
durante
Intervalo Temporal
friend
Entidade
and
JesusOfNazareth
vale
durante
Intervalo Temporal
appearance as argument number 0
(
forall
(?NUMBER)
(
equal
(
MeasureFn
?NUMBER
OunceMass
)
(
MeasureFn
(
DivisionFn
?NUMBER 16.0)
PoundMass
)))
Mid-level-ontology.kif 13333-13336
Numero Real
Numero Real
OunceMass
(s) e'
igual
a
Numero Real
+ 16.0
PoundMass
(s)
(
forall
(?NUMBER)
(
equal
(
PredecessorFn
?NUMBER)
(
SubtractionFn
?NUMBER 1)))
Merge.kif 4736-4737
Numero Inteiro
(
Numero Inteiro
+2) e'
igual
a (
Numero Inteiro
+ 1)
(
forall
(?NUMBER)
(
equal
(
SuccessorFn
?NUMBER)
(
AdditionFn
?NUMBER 1)))
Merge.kif 4720-4721
Numero Inteiro
(
Numero Inteiro
+1) e'
igual
a (
Numero Inteiro
+ 1)
(
forall
(@ROW ?ITEM)
(
equal
(
ListLengthFn
(
ListFn
@ROW ?ITEM))
(
SuccessorFn
(
ListLengthFn
(
ListFn
@ROW)))))
Merge.kif 3037-3040
@ROW
Entidade
comprimento
de (@ROW +
Entidade
) e'
igual
a (
comprimento
de (@ROW)+1)
(
forall
(@ROW ?ITEM)
(
equal
(
ListOrderFn
(
ListFn
@ROW ?ITEM)
(
ListLengthFn
(
ListFn
@ROW ?ITEM))) ?ITEM))
Merge.kif 3042-3046
@ROW
Entidade
comprimento
de (@ROW +
Entidade
)th
elemento
de (@ROW +
Entidade
) e'
igual
a
Entidade
(
forall
(@ROW ?ITEM)
(
initialList
(
ListFn
@ROW)
(
ListFn
@ROW ?ITEM)))
Merge.kif 3315-3316
@ROW
Entidade
(@ROW) e' o
comeco
de (@ROW +
Entidade
)
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