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
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 4687-4689
(
domain
AdditionFn
1
RealNumber
)
Merge.kif 4683-4683
(
domain
AdditionFn
2
RealNumber
)
Merge.kif 4684-4684
(
identityElement
AdditionFn
0)
Merge.kif 5262-5262
(
instance
AdditionFn
AssociativeFunction
)
Merge.kif 4679-4679
(
instance
AdditionFn
BinaryFunction
)
Merge.kif 4678-4678
(
instance
AdditionFn
CommutativeFunction
)
Merge.kif 4680-4680
(
instance
AdditionFn
TotalValuedRelation
)
Merge.kif 4682-4682
(
range
AdditionFn
RealNumber
)
Merge.kif 4685-4685
appearance as argument number 2
(
format
ChineseLanguage
AdditionFn
"(%*[+])")
chinese_format.kif 682-682
(
format
EnglishLanguage
AdditionFn
"(%*[+])")
english_format.kif 684-684
(
termFormat
ChineseLanguage
AdditionFn
"加成")
domainEnglishFormat.kif 5422-5422
(
termFormat
ChineseLanguage
AdditionFn
"加法函数")
chinese_format.kif 683-683
(
termFormat
ChineseTraditionalLanguage
AdditionFn
"加成")
domainEnglishFormat.kif 5421-5421
(
termFormat
EnglishLanguage
AdditionFn
"addition")
domainEnglishFormat.kif 5420-5420
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 3068-3089
(=>
(
and
(
holdsDuring
?T
(
attribute
?F
Menopausal
))
(
birthdate
?F ?B)
(
equal
?A1
(
AdditionFn
(
MeasureFn
49
YearDuration
) ?B))
(
equal
?A2
(
AdditionFn
(
MeasureFn
52
YearDuration
) ?B))
(
equal
?START
(
BeginFn
?T)))
(
modalAttribute
(
and
(
greaterThan
?START ?A1)
(
greaterThan
?A2 ?START))
Likely
))
Mid-level-ontology.kif 23882-23899
(=>
(
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
(=>
(
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
(=>
(
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 2347-2369
(=>
(
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
(=>
(
and
(
instance
?LIST
ConsecutiveTimeIntervalList
)
(
equal
?T1
(
ListOrderFn
?LIST ?N))
(
equal
?T2
(
ListOrderFn
?LIST
(
AdditionFn
?N 1))))
(
equal
(
BeginFn
?T2)
(
EndFn
?T1)))
Weather.kif 1935-1944
(=>
(
and
(
not
(
equal
?NUMBER2 0))
(
equal
(
AdditionFn
(
MultiplicationFn
(
FloorFn
(
DivisionFn
?NUMBER1 ?NUMBER2)) ?NUMBER2) ?NUMBER) ?NUMBER1))
(
equal
(
RemainderFn
?NUMBER1 ?NUMBER2) ?NUMBER))
Merge.kif 5088-5099
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 298-319
(=>
(
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 5960-5973
(=>
(
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 5946-5958
(=>
(
and
(
equal
(
RemainderFn
?NUMBER1 ?NUMBER2) ?NUMBER)
(
not
(
equal
?NUMBER2 0)))
(
equal
(
AdditionFn
(
MultiplicationFn
(
FloorFn
(
DivisionFn
?NUMBER1 ?NUMBER2)) ?NUMBER2) ?NUMBER) ?NUMBER1))
Merge.kif 5075-5086
(=>
(
and
(
equal
?A
(
ListSumFn
?L))
(
greaterThan
(
ListLengthFn
?L) 1))
(
equal
?A
(
AdditionFn
(
FirstFn
?L)
(
ListSumFn
(
SubListFn
2
(
ListLengthFn
?L) ?L)))))
Merge.kif 3235-3245
(=>
(
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 3060-3079
(=>
(
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 3068-3089
(=>
(
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 3167-3179
(=>
(
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 1453-1465
(=>
(
and
(
instance
?UNIT
UnitOfArea
)
(
landAreaOnly
?AREA
(
MeasureFn
?LAND ?UNIT))
(
waterAreaOnly
?AREA
(
MeasureFn
?WATER ?UNIT)))
(
totalArea
?AREA
(
MeasureFn
(
AdditionFn
?LAND ?WATER) ?UNIT)))
Geography.kif 562-567
(=>
(
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 17057-17063
(=>
(
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 17069-17075
(=>
(
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 17045-17051
(=>
(
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 17033-17039
(=>
(
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
(=>
(
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
(=>
(
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 6461-6469
statement
(
forall
(?NUMBER)
(
equal
(
SuccessorFn
?NUMBER)
(
AdditionFn
?NUMBER 1)))
Merge.kif 4691-4692
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