Browsing Interface
: Welcome guest :
log in
[
Home
|
Graph
| ]
KB:
SUMO
Language:
AlbanianLanguage
ArabicLanguage
BasqueLanguage
BulgarianLanguage
CatalanLanguage
ChineseLanguage
ChineseTraditionalLanguage
CroatianLanguage
DanishLanguage
EnglishLanguage
FarsiLanguage
FinnishLanguage
FrenchLanguage
GalicianLanguage
GreekLanguage
HebrewLanguage
IcelandicLanguage
IndonesianLanguage
ItalianLanguage
JapaneseLanguage
MalayLanguage
NorwegianBokmalLanguage
NorwegianNorskLanguage
PolishLanguage
PortugueseLanguage
SpanishLanguage
SwedishLanguage
TaiwanChineseLanguage
ThaiLanguage
de
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)就是这些数字的算术和。")
Merge.kif 4864-4865
(
documentation
AdditionFn
EnglishLanguage
"If ?NUMBER1 and ?NUMBER2 are
Number
s, then (
AdditionFn
?NUMBER1 ?NUMBER2) is the arithmetical sum of these numbers.")
Merge.kif 4861-4863
(
domain
AdditionFn
1
Quantity
)
Merge.kif 4858-4858
The number 1 argument of
addition
is an
instance
of
quantity
(
domain
AdditionFn
2
Quantity
)
Merge.kif 4859-4859
The number 2 argument of
addition
is an
instance
of
quantity
(
identityElement
AdditionFn
0)
Merge.kif 5386-5386
0 is an
identity
element of
addition
(
instance
AdditionFn
AssociativeFunction
)
Merge.kif 4854-4854
Addition
is an
instance
of
associative function
(
instance
AdditionFn
BinaryFunction
)
Merge.kif 4853-4853
Addition
is an
instance
of
binary function
(
instance
AdditionFn
CommutativeFunction
)
Merge.kif 4855-4855
Addition
is an
instance
of
commutative function
(
instance
AdditionFn
TotalValuedRelation
)
Merge.kif 4857-4857
Addition
is an
instance
of
total valued relation
(
range
AdditionFn
Quantity
)
Merge.kif 4860-4860
The
range
of
addition
is an instance of
quantity
appearance as argument number 2
(
format
ChineseLanguage
AdditionFn
"(%*[+])")
chinese_format.kif 682-682
(
format
EnglishLanguage
AdditionFn
"(%*[+])")
english_format.kif 425-425
(
termFormat
ChineseLanguage
AdditionFn
"加法函数")
chinese_format.kif 683-683
"加法函数" is the
printable
form
of
addition
in
ChineseLanguage
(
termFormat
EnglishLanguage
AdditionFn
"addition")
domainEnglishFormat.kif 1337-1337
"addition" is the
printable
form
of
addition
in
english language
antecedent
(=>
(
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 1166-1175
If
a financial account
is an
instance
of
credit account
and
a cognitive agent
holds
account
the financial account
and
a currency measure
is a
principal
amount of
the financial account
and
a time interval
is an
agreement
period of
the financial account
and
the financial account
interest
earned
an interest
for
the time interval
and
a quantity
is
equal
to (
the currency measure
and
the interest
),
then
the cognitive agent
is
obliged
to perform tasks of type the
class
described by
a symbolic string
(=>
(
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 1215-1224
If
a loan
is an
instance
of
loan
and
the loan
is the
borrower
of
a cognitive agent
and
a currency measure
is a
principal
amount of
the loan
and
a time interval
is an
agreement
period of
the loan
and
the loan
interest
earned
an interest
for
the time interval
and
a quantity
is
equal
to (
the currency measure
and
the interest
),
then
the cognitive agent
is
obliged
to perform tasks of type the
class
described by
a symbolic string
(=>
(
and
(
instance
?Bond
ZeroCouponBond
)
(
maturityDate
(
AccountFn
?Bond) ?Date)
(
possesses
?BondHolder ?Bond)
(
principalAmount
(
AccountFn
?Bond) ?Principal)
(
agreementPeriod
(
AccountFn
?Bond) ?Period)
(
interestEarned
(
AccountFn
?Bond) ?Interest ?Period)
(
equal
?Total
(
AdditionFn
?Principal ?Interest)))
(
exists
(?Payment)
(
and
(
instance
?Payment
Payment
)
(
destination
?Payment ?BondHolder)
(
origin
?Payment
(
CurrencyFn
?BondAccount))
(
transactionAmount
?Payment ?Total))))
FinancialOntology.kif 2264-2278
If
a financial asset
is an
instance
of
zero coupon bond
and
a day
is a
maturity
date of the
account
of
the financial asset
and
the financial asset
Holder
possess
es
the financial asset
and
a currency measure
is a
principal
amount of the
account
of
the financial asset
and
a time interval
is an
agreement
period of the
account
of
the financial asset
and the
account
of
the financial asset
interest
earned
an interest
for
the time interval
and
another currency measure
is
equal
to (
the currency measure
and
the interest
),
then there exists
a financial transaction
such that
the financial transaction
is an
instance
of
payment
and
the financial transaction
end
s up at
the financial asset
Holder and
the financial transaction
originate
s at the
currency
of
the financial asset
Account and
the other currency measure
is a
transaction
amount of
the financial transaction
(=>
(
and
(
instance
?Deposit
Deposit
)
(
time
?Deposit ?TimeOfDeposit)
(
instance
?Account
FinancialAccount
)
(
destination
?Deposit
(
CurrencyFn
?Account))
(
transactionAmount
?Deposit ?Amount)
(
currentAccountBalance
?Account
(
ImmediatePastFn
(
WhenFn
?Deposit)) ?Balance1)
(
equal
?Balance2
(
AdditionFn
?Balance1 ?Amount)))
(
currentAccountBalance
?Account
(
ImmediateFutureFn
(
FutureFn
?Deposit)) ?Balance2))
FinancialOntology.kif 428-437
If
a financial transaction
is an
instance
of
deposit
and
the financial transaction
exists
during
a time position
and
a financial account
is an
instance
of
financial account
and
the financial transaction
end
s up at the
currency
of
the financial account
and
a currency measure
is a
transaction
amount of
the financial transaction
and
the financial account
current
account balance immediately
before
the
time
of existence of
the financial transaction
for
another currency measure
and
a third currency measure
is
equal
to (
the other currency measure
and
the currency measure
),
then
the financial account
current
account balance immediately
after
after
the financial transaction
for
the third currency measure
(=>
(
and
(
principalAmount
?Account ?Balance)
(
fixedInterestRate
?Account ?Rate)
(
compoundInterest
?Account ?Interest ?Period)
(
equal
?Rate-Decimal
(
DivisionFn
?Rate 100))
(
equal
?Add
(
AdditionFn
1 ?Rate-Decimal))
(
equal
?Exponent
(
ExponentiationFn
?Add
(
MagnitudeFn
?Period)))
(
equal
?Multiply
(
MultiplicationFn
?Exponent ?Balance)))
(
equal
?Interest
(
SubtractionFn
?Multiply ?Balance)))
FinancialOntology.kif 532-541
If
a currency measure
is a
principal
amount of
a financial account
and
an interest rate
is a
fixed
interest rate of
the financial account
and
the financial account
compound
interest
an interest
for
a time interval
and
the interest rate
-Decimal is
equal
to
the interest rate
and 100 and
a real number
is
equal
to (1 and
the interest rate
-Decimal) and
another real number
is
equal
to
the real number
raised to the
power
the
magnitude
of
the time interval
and
a quantity
is
equal
to
the other real number
and
the currency measure
,
then
the interest
is
equal
to (
the quantity
and
the currency measure
)
consequent
(<=>
(
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 285-306
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
a quantity
,
the quantity
MINUSONE,, ,
another positive integer
and
a third positive integer
such that
the quantity
is
greater
than 1 and
the quantity
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 quantity
and
the other positive integer
is a
member
of
the list
and
the quantity
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 quantity
MINUSONE is
equal
to (
the quantity
and 1) and
the quantity
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
(
RemainderFn
?NUMBER1 ?NUMBER2) ?NUMBER)
(
equal
(
AdditionFn
(
MultiplicationFn
(
FloorFn
(
DivisionFn
?NUMBER1 ?NUMBER2)) ?NUMBER2) ?NUMBER) ?NUMBER1))
Merge.kif 5261-5263
An integer
mod
another integer
is
equal
to
a third integer
if and only if (the
largest
integer less than or equal to
the integer
and
the other integer
and
the other integer
and
the third integer
) is
equal
to
the integer
(=>
(
and
(
courseWRTMagneticNorth
?OBJ1 ?OBJ2 ?MAGDEGREE)
(
partlyLocated
?OBJ1 ?AREA)
(
partlyLocated
?OBJ2 ?AREA)
(
magneticVariation
?AREA ?DEGREE ?DIRECTION))
(
exists
(?DIFFDEGREE ?TRUEDEGREE)
(
and
(=>
(
and
(
equal
?DIRECTION
East
)
(
equal
?DIFFDEGREE
(
AdditionFn
?MAGDEGREE ?DEGREE)))
(
courseWRTTrueNorth
?OBJ1 ?OBJ2 ?TRUEDEGREE))
(=>
(
and
(
equal
?DIRECTION
West
)
(
equal
?DIFFDEGREE
(
SubtractionFn
?MAGDEGREE ?DEGREE)))
(
courseWRTTrueNorth
?OBJ1 ?OBJ2 ?TRUEDEGREE)))))
Geography.kif 3619-3636
If
a physical
courseWRT
magnetic north
another physical
for
a plane angle measure
and
the physical
is
partly
located in
a geographic area
and
the other physical
is
partly
located in
the geographic area
and
the geographic area
magnetic
variation
another plane angle measure
for
a directional attribute
,
then there exist
a quantity
and
a third plane angle measure
such that
if
the directional attribute
is
equal
to
east
and
the quantity
is
equal
to (
the plane angle measure
and
the other plane angle measure
),
then
the physical
courseWRT
true north
the other physical
for
the third plane angle measure
and
if
the directional attribute
is
equal
to
west
and
the quantity
is
equal
to (
the plane angle measure
and
the other plane angle measure
),
then
the physical
courseWRT
true north
the other physical
for
the third plane angle measure
(=>
(
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 6113-6126
If the
value
of
a graph path
is
equal
to
a quantity
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 quantity
and the
value
of
the other graph arc
is
a third quantity
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 quantity
and
the third quantity
)
(=>
(
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 6099-6111
If the
value
of
a graph path
is
equal
to
a quantity
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 quantity
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 quantity
is
equal
to (the
value
of
the other graph path
and
the other quantity
)
(=>
(
and
(
instance
?UNIT
UnitOfArea
)
(
landAreaOnly
?AREA
(
MeasureFn
?LAND ?UNIT))
(
waterAreaOnly
?AREA
(
MeasureFn
?WATER ?UNIT)))
(
totalArea
?AREA
(
MeasureFn
(
AdditionFn
?LAND ?WATER) ?UNIT)))
Geography.kif 559-564
If
an unit of measure
is an
instance
of
UnitOfArea
and
a real number
the unit of measure
(s) is a
land
area only of
a geographic area
and
another real number
the unit of measure
(s) is a
water
area only of
the geographic area
,
then (
the real number
and
the other real number
)
the unit of measure
(s) is a
total
area of
the geographic area
(=>
(
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 504-511
If
a real number
an unit of measure
(s) is a
total
length of highway system of
a geographic area
and
the real number
1
the unit of measure
(s) is a
length
of paved highway of
the geographic area
and
the real number
2
the unit of measure
(s) is a
length
of unpaved highway of
the geographic area
and
the unit of measure
is an
instance
of
UnitOfLength
,
then (
the real number
1 and
the real number
2)
the unit of measure
(s) is a
total
length of highway system of
the geographic area
(=>
(
and
(
totalLengthOfHighwaySystem
?AREA ?LENGTH)
(
lengthOfPavedHighway
?AREA ?LENGTH1)
(
lengthOfUnpavedHighway
?AREA ?LENGTH2))
(
equal
?LENGTH
(
AdditionFn
?LENGTH1 ?LENGTH2)))
Transportation.kif 497-502
If
a length measure
is a
total
length of highway system of
a geographic area
and
the length measure
1 is a
length
of paved highway of
the geographic area
and
the length measure
2 is a
length
of unpaved highway of
the geographic area
,
then
the length measure
is
equal
to (
the length measure
1 and
the length measure
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 6189-6197
If
a compound substance
is a
conjugate
of
another compound substance
,
then there exist
a positive integer
and
another positive integer
such that
the positive integer
is a
proton
number of
the other compound substance
and
the other positive integer
is a
proton
number of
the compound substance
and
the positive integer
is
equal
to (
the other positive integer
and 1) or
the other positive integer
is
equal
to (
the positive integer
and 1)
(=>
(
equal
(
RelativeTimeFn
?TIME1
CentralTimeZone
) ?TIME2)
(
equal
?TIME2
(
AdditionFn
?TIME1
(
MeasureFn
6
HourDuration
))))
Merge.kif 17554-17556
If the time
a time position
in zone
central time zone
is
equal
to
another time position
,
then
the other time position
is
equal
to (
the time position
and 6
hour duration
(s))
(=>
(
equal
(
RelativeTimeFn
?TIME1
EasternTimeZone
) ?TIME2)
(
equal
?TIME2
(
AdditionFn
?TIME1
(
MeasureFn
5
HourDuration
))))
Merge.kif 17563-17565
If the time
a time position
in zone
eastern time zone
is
equal
to
another time position
,
then
the other time position
is
equal
to (
the time position
and 5
hour duration
(s))
(=>
(
equal
(
RelativeTimeFn
?TIME1
MountainTimeZone
) ?TIME2)
(
equal
?TIME2
(
AdditionFn
?TIME1
(
MeasureFn
7
HourDuration
))))
Merge.kif 17545-17547
If the time
a time position
in zone
mountain time zone
is
equal
to
another time position
,
then
the other time position
is
equal
to (
the time position
and 7
hour duration
(s))
(=>
(
equal
(
RelativeTimeFn
?TIME1
PacificTimeZone
) ?TIME2)
(
equal
?TIME2
(
AdditionFn
?TIME1
(
MeasureFn
8
HourDuration
))))
Merge.kif 17536-17538
If the time
a time position
in zone
pacific time zone
is
equal
to
another time position
,
then
the other time position
is
equal
to (
the time position
and 8
hour duration
(s))
statement
(
forall
(?NUMBER)
(
equal
(
SuccessorFn
?NUMBER)
(
AdditionFn
?NUMBER 1)))
Merge.kif 4867-4868
For all
an integer
(
the integer
+1) is
equal
to (
the integer
and 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 2.99c (>= 2017/11/20) is
open source software
produced by
Articulate Software
and its partners
