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
AdditionFn
Sigma KEE - AdditionFn
AdditionFn
appearance as argument number 1
(
documentation
AdditionFn
ChineseLanguage
"如果 ?NUMBER1 和 ?NUMBER2 是
Number
,那么 (
AdditionFn
?NUMBER1 ?NUMBER2)就是这些数字的算术和。")
chinese_format.kif 2214-2215
(
documentation
AdditionFn
EnglishLanguage
"If ?NUMBER1 and ?NUMBER2 are
Number
s, then (
AdditionFn
?NUMBER1 ?NUMBER2) is the arithmetical sum of these numbers.")
Merge.kif 4717-4719
(
documentation
AdditionFn
JapaneseLanguage
"?NUMBER1 と ?NUMBER2 が
Number
の場合、 (
AdditionFn
?NUMBER1 ?NUMBER2) はこれらの数値の算術合計である。")
japanese_format.kif 878-879
(
domain
AdditionFn
1
RealNumber
)
Merge.kif 4713-4713
O argumento numero 1 de
AdditionFn
e' uma
instancia
de
Numero Real
(
domain
AdditionFn
2
RealNumber
)
Merge.kif 4714-4714
O argumento numero 2 de
AdditionFn
e' uma
instancia
de
Numero Real
(
identityElement
AdditionFn
0)
Merge.kif 5296-5296
0 e' um
elemento
identificador de
AdditionFn
(
instance
AdditionFn
AssociativeFunction
)
Merge.kif 4709-4709
AdditionFn
e' uma
instancia
de
Funcao Associativa
(
instance
AdditionFn
BinaryFunction
)
Merge.kif 4708-4708
AdditionFn
e' uma
instancia
de
Funcao Binaria
(
instance
AdditionFn
CommutativeFunction
)
Merge.kif 4710-4710
AdditionFn
e' uma
instancia
de
Funcao Commutativa
(
instance
AdditionFn
TotalValuedRelation
)
Merge.kif 4712-4712
AdditionFn
e' uma
instancia
de
Relacao Total
(
range
AdditionFn
RealNumber
)
Merge.kif 4715-4715
O
contra
-dominio de
AdditionFn
e' uma instancia de
Numero Real
appearance as argument number 2
(
format
ChineseLanguage
AdditionFn
"(%*[+])")
chinese_format.kif 682-682
(
format
EnglishLanguage
AdditionFn
"(%*[+])")
english_format.kif 684-684
(
format
FrenchLanguage
AdditionFn
"(%*[+])")
french_format.kif 414-414
(
format
ItalianLanguage
AdditionFn
"(%*[+]")
relations-it.txt 20-20
(
format
JapaneseLanguage
AdditionFn
"(%*[+])")
japanese_format.kif 2131-2131
(
format
PortugueseLanguage
AdditionFn
"(%*[+])")
portuguese_format.kif 366-366
(
format
cz
AdditionFn
"(%*[+])")
relations-cz.txt 423-423
(
format
de
AdditionFn
"(%*[+])")
relations-de.txt 889-889
(
format
hi
AdditionFn
"(%*[+]")
relations-hindi.txt 65-65
(
format
ro
AdditionFn
"(%*[+])")
relations-ro.kif 436-436
(
format
sv
AdditionFn
"(%*[+])")
relations-sv.txt 458-458
(
format
tg
AdditionFn
"(%*[+]")
relations-cb.txt 54-54
(
termFormat
ChineseLanguage
AdditionFn
"加成")
domainEnglishFormat.kif 5418-5418
(
termFormat
ChineseLanguage
AdditionFn
"加法函数")
chinese_format.kif 683-683
(
termFormat
ChineseTraditionalLanguage
AdditionFn
"加成")
domainEnglishFormat.kif 5417-5417
(
termFormat
EnglishLanguage
AdditionFn
"addition")
domainEnglishFormat.kif 5416-5416
(
termFormat
tg
AdditionFn
"tungkulin ng pagsasama")
relations-tg.txt 57-57
antecedent
(=>
(
and
(
equal
?OUT
(
ReverseFn
?IN))
(
equal
?LEN
(
StringLengthFn
?IN))
(
greaterThan
?LEN 1)
(
greaterThan
?N 0)
(
lessThan
?N ?LEN)
(
equal
?PIVOT
(
CeilingFn
(
DivisionFn
(
SubtractionFn
?LEN 1) 2)))
(
equal
?NEW
(
AdditionFn
(
SubtractionFn
?PIVOT ?N) ?PIVOT))
(
equal
?S
(
SubstringFn
?IN ?N
(
AdditionFn
1 ?N))))
(
equal
?S
(
SubstringFn
?OUT ?NEW
(
AdditionFn
1 ?NEW))))
Media.kif 3050-3071
Sequencia Simbolica
e'
igual
a
ReverseFn
Sequencia Simbolica
Numero Inteiro nao-negativo
e'
igual
a
StringLengthFn
Sequencia Simbolica
Numero Inteiro nao-negativo
e'
maior
que 1
Numero Inteiro nao-negativo
e'
maior
que 0
Numero Inteiro nao-negativo
e'
menos
que
Numero Inteiro nao-negativo
Numero Inteiro
e'
igual
a o
teto
de (
Numero Inteiro nao-negativo
+ 1) + 2
Numero Inteiro nao-negativo
EW e'
igual
a ((
Numero Inteiro
+
Numero Inteiro nao-negativo
) +
Numero Inteiro
)
Sequencia Simbolica
e'
igual
a
SubstringFn
Sequencia Simbolica
,
Numero Inteiro nao-negativo
and (1 +
Numero Inteiro nao-negativo
)
Sequencia Simbolica
e'
igual
a
SubstringFn
Sequencia Simbolica
,
Numero Inteiro nao-negativo
EW and (1 +
Numero Inteiro nao-negativo
EW)
(=>
(
and
(
holdsDuring
?T
(
attribute
?F
Menopausal
))
(
birthdate
?F ?B)
(
instance
?B
(
DayFn
?D
(
MonthFn
?M
(
YearFn
?Y))))
(
equal
?A1
(
AdditionFn
49 ?Y))
(
equal
?A2
(
AdditionFn
52 ?Y))
(
equal
?START
(
BeginFn
?T)))
(
modalAttribute
(
and
(
greaterThan
?START ?A1)
(
greaterThan
?A2 ?START))
Likely
))
Mid-level-ontology.kif 23973-23989
Menopausal
e' um
atributo
de
Humano
vale
durante
Intervalo Temporal
birthdate
Humano
and
Dia
Dia
e' uma
instancia
de o
dia
Inteiro positivo
Numero Real
e'
igual
a (49 +
Numero Inteiro
)
Numero Real
e'
igual
a (52 +
Numero Inteiro
)
Ponto no tempo
e'
igual
a o
comeco
de
Intervalo Temporal
o argumento
Ponto no tempo
e'
maior
que
Numero Real
Numero Real
e'
maior
que
Ponto no tempo
tem a
forca
modal
de
Likely
(=>
(
and
(
instance
?Account
CreditAccount
)
(
accountHolder
?Account ?Agent)
(
principalAmount
?Account ?Principal)
(
agreementPeriod
?Account ?Period)
(
interestEarned
?Account ?Interest ?Period)
(
equal
?Total
(
AdditionFn
?Principal ?Interest)))
(
holdsObligation
(
KappaFn
?Payment
(
transactionAmount
?Payment ?Total)) ?Agent))
FinancialOntology.kif 1224-1233
FinancialAccount
e' uma
instancia
de
CreditAccount
accountHolder
FinancialAccount
and
Agente Cognitivo
principalAmount
FinancialAccount
and
Numero Real
agreementPeriod
FinancialAccount
and
Intervalo Temporal
interestEarned
FinancialAccount
,
Interest
and
Intervalo Temporal
Numero Real
e'
igual
a (
Numero Real
+
Interest
)
Agente Cognitivo
e'
obrigado
a executar tarefas de tipo a
classe
descrita por
Sequencia Simbolica
(=>
(
and
(
instance
?Account
Loan
)
(
borrower
?Account ?Agent)
(
principalAmount
?Account ?Principal)
(
agreementPeriod
?Account ?Period)
(
interestEarned
?Account ?Interest ?Period)
(
equal
?Total
(
AdditionFn
?Principal ?Interest)))
(
holdsObligation
(
KappaFn
?Payment
(
transactionAmount
?Payment ?Total)) ?Agent))
FinancialOntology.kif 1273-1282
Loan
e' uma
instancia
de
Loan
borrower
Loan
and
Agente Cognitivo
principalAmount
Loan
and
Numero Real
agreementPeriod
Loan
and
Intervalo Temporal
interestEarned
Loan
,
Interest
and
Intervalo Temporal
Numero Real
e'
igual
a (
Numero Real
+
Interest
)
Agente Cognitivo
e'
obrigado
a executar tarefas de tipo a
classe
descrita por
Sequencia Simbolica
(=>
(
and
(
instance
?Bond
ZeroCouponBond
)
(
maturityDate
(
AccountFn
?Bond) ?Date)
(
possesses
?BondHolder ?Bond)
(
principalAmount
(
AccountFn
?Bond)
(
MeasureFn
?Principal ?CUNIT))
(
agreementPeriod
(
AccountFn
?Bond) ?Period)
(
interestEarned
(
AccountFn
?Bond)
(
MeasureFn
?Interest ?CUNIT) ?Period)
(
equal
?Total
(
AdditionFn
?Principal ?Interest)))
(
exists
(?Payment)
(
and
(
instance
?Payment
Payment
)
(
destination
?Payment ?BondHolder)
(
origin
?Payment
(
AccountFn
?Bond))
(
transactionAmount
?Payment
(
MeasureFn
?Total ?CUNIT)))))
FinancialOntology.kif 2333-2355
FinancialAsset
e' uma
instancia
de
ZeroCouponBond
maturityDate
AccountFn
FinancialAsset
and
Dia
FinancialAsset
Holder
possui
FinancialAsset
principalAmount
AccountFn
FinancialAsset
and
Numero Real
Unidade de Medida
(s)
agreementPeriod
AccountFn
FinancialAsset
and
Intervalo Temporal
interestEarned
AccountFn
FinancialAsset
,
Numero Real
Unidade de Medida
(s) and
Intervalo Temporal
Numero Real
e'
igual
a (
Numero Real
+
Numero Real
)
Transacao Financeira
Transacao Financeira
e' uma
instancia
de
Payment
Transacao Financeira
termina
em
FinancialAsset
Holder
Transacao Financeira
tem como
origem
AccountFn
FinancialAsset
transactionAmount
Transacao Financeira
and
Numero Real
Unidade de Medida
(s)
(=>
(
and
(
instance
?Deposit
Deposit
)
(
instance
?Account
FinancialAccount
)
(
destination
?Deposit
(
CurrencyFn
?Account))
(
transactionAmount
?Deposit
(
MeasureFn
?Amount ?CUNIT))
(
currentAccountBalance
?Account
(
ImmediatePastFn
(
WhenFn
?Deposit))
(
MeasureFn
?Balance1 ?CUNIT))
(
equal
?Balance2
(
AdditionFn
?Balance1 ?Amount)))
(
currentAccountBalance
?Account
(
ImmediateFutureFn
(
FutureFn
?Deposit))
(
MeasureFn
?Balance2 ?CUNIT)))
FinancialOntology.kif 436-453
Transacao Financeira
e' uma
instancia
de
Deposit
FinancialAccount
e' uma
instancia
de
FinancialAccount
Transacao Financeira
termina
em
CurrencyFn
FinancialAccount
transactionAmount
Transacao Financeira
and
Numero Real
Unidade de Medida
(s)
currentAccountBalance
FinancialAccount
, imediatemente
antes
de
tempo
de existencia de
Transacao Financeira
and
Numero Real
Unidade de Medida
(s)
Numero Real
e'
igual
a (
Numero Real
+
Numero Real
)
currentAccountBalance
FinancialAccount
, imediatemente
apos
apos
Transacao Financeira
and
Numero Real
Unidade de Medida
(s)
(=>
(
and
(
instance
?LIST
ConsecutiveTimeIntervalList
)
(
equal
?T1
(
ListOrderFn
?LIST ?N))
(
equal
?T2
(
ListOrderFn
?LIST
(
AdditionFn
?N 1))))
(
equal
(
BeginFn
?T2)
(
EndFn
?T1)))
Weather.kif 1918-1927
Lista
e' uma
instancia
de
ConsecutiveTimeIntervalList
Intervalo Temporal
e'
igual
a
Entidade
elemento
de
Lista
Intervalo Temporal
e'
igual
a (
Inteiro positivo
+ 1)th
elemento
de
Lista
o
comeco
de
Intervalo Temporal
e'
igual
a o
fim
de
Intervalo Temporal
(=>
(
and
(
not
(
equal
?NUMBER2 0))
(
equal
(
AdditionFn
(
MultiplicationFn
(
FloorFn
(
DivisionFn
?NUMBER1 ?NUMBER2)) ?NUMBER2) ?NUMBER) ?NUMBER1))
(
equal
(
RemainderFn
?NUMBER1 ?NUMBER2) ?NUMBER))
Merge.kif 5118-5129
Numero Inteiro
e'
igual
a 0 (o
maior
numero inteiro menor or igual a
Numero Inteiro
+
Numero Inteiro
+
Numero Inteiro
+
Numero Inteiro
) e'
igual
a
Numero Inteiro
Numero Inteiro
mod
Numero Inteiro
e'
igual
a
Numero Inteiro
consequent
(<=>
(
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
(=>
(
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 5994-6007
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 5980-5992
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
(
equal
(
RemainderFn
?NUMBER1 ?NUMBER2) ?NUMBER)
(
not
(
equal
?NUMBER2 0)))
(
equal
(
AdditionFn
(
MultiplicationFn
(
FloorFn
(
DivisionFn
?NUMBER1 ?NUMBER2)) ?NUMBER2) ?NUMBER) ?NUMBER1))
Merge.kif 5105-5116
Numero Inteiro
mod
Numero Inteiro
e'
igual
a
Numero Inteiro
Numero Inteiro
e'
igual
a 0
(o
maior
numero inteiro menor or igual a
Numero Inteiro
+
Numero Inteiro
+
Numero Inteiro
+
Numero Inteiro
) e'
igual
a
Numero Inteiro
(=>
(
and
(
equal
?A
(
ListSumFn
?L))
(
greaterThan
(
ListLengthFn
?L) 1))
(
equal
?A
(
AdditionFn
(
FirstFn
?L)
(
ListSumFn
(
SubListFn
2
(
ListLengthFn
?L) ?L)))))
Merge.kif 3259-3269
Numero Real
e'
igual
a
ListSumFn
Lista
comprimento
de
Lista
e'
maior
que 1
Numero Real
e'
igual
a (
FirstFn
Lista
+
ListSumFn
SubListFn
2,
comprimento
de
Lista
and
Lista
)
(=>
(
and
(
equal
?LIST3
(
ListConcatenateFn
?LIST1 ?LIST2))
(
not
(
equal
?LIST1
NullList
))
(
not
(
equal
?LIST2
NullList
))
(
lessThanOrEqualTo
?NUMBER1
(
ListLengthFn
?LIST1))
(
lessThanOrEqualTo
?NUMBER2
(
ListLengthFn
?LIST2))
(
instance
?NUMBER1
PositiveInteger
)
(
instance
?NUMBER2
PositiveInteger
))
(
and
(
equal
(
ListOrderFn
?LIST3 ?NUMBER1)
(
ListOrderFn
?LIST1 ?NUMBER1))
(
equal
(
ListOrderFn
?LIST3
(
AdditionFn
(
ListLengthFn
?LIST1) ?NUMBER2))
(
ListOrderFn
?LIST2 ?NUMBER2))))
Merge.kif 3084-3103
Lista
e'
igual
a a
lista
composta de
Lista
e
Lista
Lista
e'
igual
a
NullList
Lista
e'
igual
a
NullList
Inteiro positivo
e'
menor
ou igual a
comprimento
de
Lista
Inteiro positivo
e'
menor
ou igual a
comprimento
de
Lista
Inteiro positivo
e' uma
instancia
de
Inteiro positivo
Inteiro positivo
e' uma
instancia
de
Inteiro positivo
Inteiro positivo
th
elemento
de
Lista
e'
igual
a
Inteiro positivo
th
elemento
de
Lista
(
comprimento
de
Lista
+
Inteiro positivo
)th
elemento
de
Lista
e'
igual
a
Inteiro positivo
th
elemento
de
Lista
(=>
(
and
(
equal
?OUT
(
ReverseFn
?IN))
(
equal
?LEN
(
StringLengthFn
?IN))
(
greaterThan
?LEN 1)
(
greaterThan
?N 0)
(
lessThan
?N ?LEN)
(
equal
?PIVOT
(
CeilingFn
(
DivisionFn
(
SubtractionFn
?LEN 1) 2)))
(
equal
?NEW
(
AdditionFn
(
SubtractionFn
?PIVOT ?N) ?PIVOT))
(
equal
?S
(
SubstringFn
?IN ?N
(
AdditionFn
1 ?N))))
(
equal
?S
(
SubstringFn
?OUT ?NEW
(
AdditionFn
1 ?NEW))))
Media.kif 3050-3071
Sequencia Simbolica
e'
igual
a
ReverseFn
Sequencia Simbolica
Numero Inteiro nao-negativo
e'
igual
a
StringLengthFn
Sequencia Simbolica
Numero Inteiro nao-negativo
e'
maior
que 1
Numero Inteiro nao-negativo
e'
maior
que 0
Numero Inteiro nao-negativo
e'
menos
que
Numero Inteiro nao-negativo
Numero Inteiro
e'
igual
a o
teto
de (
Numero Inteiro nao-negativo
+ 1) + 2
Numero Inteiro nao-negativo
EW e'
igual
a ((
Numero Inteiro
+
Numero Inteiro nao-negativo
) +
Numero Inteiro
)
Sequencia Simbolica
e'
igual
a
SubstringFn
Sequencia Simbolica
,
Numero Inteiro nao-negativo
and (1 +
Numero Inteiro nao-negativo
)
Sequencia Simbolica
e'
igual
a
SubstringFn
Sequencia Simbolica
,
Numero Inteiro nao-negativo
EW and (1 +
Numero Inteiro nao-negativo
EW)
(=>
(
and
(
equal
?R
(
SubListFn
?S ?E ?L))
(
greaterThan
(
SubtractionFn
?E ?S) 1))
(
equal
?R
(
ListConcatenateFn
(
ListFn
(
ListOrderFn
?L ?S))
(
SubListFn
(
AdditionFn
1 ?S) ?E ?L))))
Merge.kif 3191-3203
Lista
e'
igual
a
SubListFn
Inteiro positivo
,
Numero Inteiro
and
Lista
(
Numero Inteiro
+
Inteiro positivo
) e'
maior
que 1
Lista
e'
igual
a a
lista
composta de (
Inteiro positivo
th
elemento
de
Lista
) e
SubListFn
(1 +
Inteiro positivo
),
Numero Inteiro
and
Lista
(=>
(
and
(
equal
?VA
(
VarianceAverageFn
?M ?L))
(
greaterThan
(
ListLengthFn
?L) 1))
(
equal
?VA
(
AdditionFn
(
VarianceAverageFn
?M
(
ListOrderFn
?L 1))
(
VarianceAverageFn
?M
(
SubListFn
2
(
ListLengthFn
?L) ?L)))))
Weather.kif 1437-1449
Numero Real
e'
igual
a
VarianceAverageFn
Numero
and
Lista
comprimento
de
Lista
e'
maior
que 1
Numero Real
e'
igual
a (
VarianceAverageFn
Numero
and 1th
elemento
de
Lista
+
VarianceAverageFn
Numero
and
SubListFn
2,
comprimento
de
Lista
and
Lista
)
(=>
(
and
(
instance
?M
Mixture
)
(
instance
?Z
UnitOfMeasure
)
(
mixtureRatio
?A ?B ?X ?Y ?Z)
(
measure
?M
(
MeasureFn
?T ?Z))
(
part
?A ?M)
(
part
?B ?M)
(
measure
?A
(
MeasureFn
?X ?Z))
(
measure
?B
(
MeasureFn
?Y ?Z)))
(
equal
?T
(
AdditionFn
?X ?Y)))
Food.kif 1248-1262
Objeto
e' uma
instancia
de
Mistura
Unidade de Medida
e' uma
instancia
de
Unidade de Medida
mixtureRatio
Substancia
,
Substancia
,
Numero Real
,
Numero Real
and
Unidade de Medida
a
medida
de
Objeto
e'
Numero Real
Unidade de Medida
(s)
Substancia
e' uma &parte de
Objeto
Substancia
e' uma &parte de
Objeto
a
medida
de
Substancia
e'
Numero Real
Unidade de Medida
(s) a
medida
de
Substancia
e'
Numero Real
Unidade de Medida
(s)
Numero Real
e'
igual
a (
Numero Real
+
Numero Real
)
(=>
(
and
(
instance
?MIT
BarMitzvah
)
(
patient
?MIT ?X)
(
instance
?X
Boy
)
(
member
?X ?GROUP)
(
instance
?GROUP
Judaism
)
(
birthdate
?X ?DAY)
(
instance
?DAY
(
DayFn
?D
(
MonthFn
?M
(
YearFn
?Y)))))
(
exists
(?Y13 ?BD13)
(
and
(
instance
?Y13
Integer
)
(
equal
?Y13
(
AdditionFn
?Y 13))
(
instance
?BD13
(
DayFn
?D
(
MonthFn
?M
(
YearFn
?Y13))))
(
equal
(
WhenFn
?MIT)
(
ImmediateFutureFn
?BD13)))))
Biography.kif 69-85
Processo
e' uma
instancia
de
BarMitzvah
Humano
e' um
patient
de
Processo
Humano
e' uma
instancia
de
Boy
Humano
e'
membro
de
Colecao
Colecao
e' uma
instancia
de
Judaism
birthdate
Humano
and
Dia
Dia
e' uma
instancia
de o
dia
Inteiro positivo
Numero Inteiro
Posicao Temporal
Numero Inteiro
e' uma
instancia
de
Numero Inteiro
Numero Inteiro
e'
igual
a (
Numero Inteiro
+ 13)
Posicao Temporal
e' uma
instancia
de o
dia
Inteiro positivo
tempo
de existencia de
Processo
e'
igual
a imediatemente
apos
Posicao Temporal
(=>
(
and
(
instance
?MIT
BatMitzvah
)
(
patient
?MIT ?X)
(
instance
?X
Girl
)
(
member
?X ?GROUP)
(
instance
?GROUP
Judaism
)
(
birthdate
?X ?DAY)
(
instance
?DAY
(
DayFn
?D
(
MonthFn
?M
(
YearFn
?Y)))))
(
exists
(?Y13 ?BD13)
(
and
(
instance
?Y13
Integer
)
(
equal
?Y13
(
AdditionFn
?Y 13))
(
instance
?BD13
(
DayFn
?D
(
MonthFn
?M
(
YearFn
?Y13))))
(
equal
(
WhenFn
?MIT)
(
ImmediateFutureFn
?BD13)))))
Biography.kif 99-115
Processo
e' uma
instancia
de
BatMitzvah
Humano
e' um
patient
de
Processo
Humano
e' uma
instancia
de
Girl
Humano
e'
membro
de
Colecao
Colecao
e' uma
instancia
de
Judaism
birthdate
Humano
and
Dia
Dia
e' uma
instancia
de o
dia
Inteiro positivo
Numero Inteiro
Posicao Temporal
Numero Inteiro
e' uma
instancia
de
Numero Inteiro
Numero Inteiro
e'
igual
a (
Numero Inteiro
+ 13)
Posicao Temporal
e' uma
instancia
de o
dia
Inteiro positivo
tempo
de existencia de
Processo
e'
igual
a imediatemente
apos
Posicao Temporal
(=>
(
and
(
instance
?UNIT
UnitOfArea
)
(
landAreaOnly
?AREA
(
MeasureFn
?LAND ?UNIT))
(
waterAreaOnly
?AREA
(
MeasureFn
?WATER ?UNIT)))
(
totalArea
?AREA
(
MeasureFn
(
AdditionFn
?LAND ?WATER) ?UNIT)))
Geography.kif 555-560
Unidade de Medida
e' uma
instancia
de
UnitOfArea
landAreaOnly
Area Geografica
and
Numero Real
Unidade de Medida
(s)
waterAreaOnly
Area Geografica
and
Numero Real
Unidade de Medida
(s)
totalArea
Area Geografica
and (
Numero Real
+
Numero Real
)
Unidade de Medida
(s)
(=>
(
and
(
instance
?UTC
(
HourFn
?H1
(
DayFn
?D
(
MonthFn
?M
(
YearFn
?Y)))))
(
instance
?CST
(
HourFn
?H2
(
DayFn
?D
(
MonthFn
?M
(
YearFn
?Y)))))
(
equal
(
RelativeTimeFn
?UTC
CentralTimeZone
) ?CST))
(
equal
?H2
(
AdditionFn
?H1 6)))
Merge.kif 17277-17283
Posicao Temporal
e' uma
instancia
de a
hora
Numero Inteiro nao-negativo
Posicao Temporal
e' uma
instancia
de a
hora
Numero Inteiro nao-negativo
o tempo
Posicao Temporal
na zona
CentralTimeZone
e'
igual
a
Posicao Temporal
Numero Inteiro nao-negativo
e'
igual
a (
Numero Inteiro nao-negativo
+ 6)
(=>
(
and
(
instance
?UTC
(
HourFn
?H1
(
DayFn
?D
(
MonthFn
?M
(
YearFn
?Y)))))
(
instance
?EST
(
HourFn
?H2
(
DayFn
?D
(
MonthFn
?M
(
YearFn
?Y)))))
(
equal
(
RelativeTimeFn
?UTC
EasternTimeZone
) ?EST))
(
equal
?H2
(
AdditionFn
?H1 5)))
Merge.kif 17289-17295
Posicao Temporal
e' uma
instancia
de a
hora
Numero Inteiro nao-negativo
Posicao Temporal
e' uma
instancia
de a
hora
Numero Inteiro nao-negativo
o tempo
Posicao Temporal
na zona
EasternTimeZone
e'
igual
a
Posicao Temporal
Numero Inteiro nao-negativo
e'
igual
a (
Numero Inteiro nao-negativo
+ 5)
(=>
(
and
(
instance
?UTC
(
HourFn
?H1
(
DayFn
?D
(
MonthFn
?M
(
YearFn
?Y)))))
(
instance
?MST
(
HourFn
?H2
(
DayFn
?D
(
MonthFn
?M
(
YearFn
?Y)))))
(
equal
(
RelativeTimeFn
?UTC
MountainTimeZone
) ?MST))
(
equal
?H2
(
AdditionFn
?H1 7)))
Merge.kif 17265-17271
Posicao Temporal
e' uma
instancia
de a
hora
Numero Inteiro nao-negativo
Posicao Temporal
e' uma
instancia
de a
hora
Numero Inteiro nao-negativo
o tempo
Posicao Temporal
na zona
MountainTimeZone
e'
igual
a
Posicao Temporal
Numero Inteiro nao-negativo
e'
igual
a (
Numero Inteiro nao-negativo
+ 7)
(=>
(
and
(
instance
?UTC
(
HourFn
?H1
(
DayFn
?D
(
MonthFn
?M
(
YearFn
?Y)))))
(
instance
?PST
(
HourFn
?H2
(
DayFn
?D
(
MonthFn
?M
(
YearFn
?Y)))))
(
equal
(
RelativeTimeFn
?UTC
PacificTimeZone
) ?PST))
(
equal
?H2
(
AdditionFn
?H1 8)))
Merge.kif 17253-17259
Posicao Temporal
e' uma
instancia
de a
hora
Numero Inteiro nao-negativo
Posicao Temporal
e' uma
instancia
de a
hora
Numero Inteiro nao-negativo
o tempo
Posicao Temporal
na zona
PacificTimeZone
e'
igual
a
Posicao Temporal
Numero Inteiro nao-negativo
e'
igual
a (
Numero Inteiro nao-negativo
+ 8)
(=>
(
and
(
totalLengthOfHighwaySystem
?AREA
(
MeasureFn
?LENGTH ?UNIT))
(
lengthOfPavedHighway
?AREA
(
MeasureFn
?LENGTH1 ?UNIT))
(
lengthOfUnpavedHighway
?AREA
(
MeasureFn
?LENGTH2 ?UNIT))
(
instance
?UNIT
UnitOfLength
))
(
totalLengthOfHighwaySystem
?AREA
(
MeasureFn
(
AdditionFn
?LENGTH1 ?LENGTH2) ?UNIT)))
Transportation.kif 510-517
totalLengthOfHighwaySystem
Area Geografica
and
Numero Real
Unidade de Medida
(s)
lengthOfPavedHighway
Area Geografica
and
Numero Real
1
Unidade de Medida
(s)
lengthOfUnpavedHighway
Area Geografica
and
Numero Real
2
Unidade de Medida
(s)
Unidade de Medida
e' uma
instancia
de
UnitOfLength
totalLengthOfHighwaySystem
Area Geografica
and (
Numero Real
1 +
Numero Real
2)
Unidade de Medida
(s)
(=>
(
and
(
totalLengthOfHighwaySystem
?AREA
(
MeasureFn
?LENGTH ?UNIT))
(
lengthOfPavedHighway
?AREA
(
MeasureFn
?LENGTH1 ?UNIT))
(
lengthOfUnpavedHighway
?AREA
(
MeasureFn
?LENGTH2 ?UNIT)))
(
equal
?LENGTH
(
AdditionFn
?LENGTH1 ?LENGTH2)))
Transportation.kif 503-508
totalLengthOfHighwaySystem
Area Geografica
and
Numero Real
Unidade de Medida
(s)
lengthOfPavedHighway
Area Geografica
and
Numero Real
1
Unidade de Medida
(s)
lengthOfUnpavedHighway
Area Geografica
and
Numero Real
2
Unidade de Medida
(s)
Numero Real
e'
igual
a (
Numero Real
1 +
Numero Real
2)
(=>
(
conjugate
?COMPOUND1 ?COMPOUND2)
(
exists
(?NUMBER1 ?NUMBER2)
(
and
(
protonNumber
?COMPOUND1 ?NUMBER1)
(
protonNumber
?COMPOUND2 ?NUMBER2)
(
or
(
equal
?NUMBER1
(
AdditionFn
?NUMBER2 1))
(
equal
?NUMBER2
(
AdditionFn
?NUMBER1 1))))))
Mid-level-ontology.kif 6495-6503
conjugate
Substancia Composta
and
Substancia Composta
Inteiro positivo
Inteiro positivo
protonNumber
Substancia Composta
and
Inteiro positivo
protonNumber
Substancia Composta
and
Inteiro positivo
Inteiro positivo
e'
igual
a (
Inteiro positivo
+ 1)
Inteiro positivo
e'
igual
a (
Inteiro positivo
+ 1)
statement
(
forall
(?NUMBER)
(
equal
(
SuccessorFn
?NUMBER)
(
AdditionFn
?NUMBER 1)))
Merge.kif 4721-4722
Numero Inteiro
(
Numero Inteiro
+1) e'
igual
a (
Numero Inteiro
+ 1)
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