Browsing Interface
: Welcome guest :
log in
[
Home
| 
Graph
|  ]
KB:
SUMO
Language:
ChineseLanguage
ChinesePinyinWriting
ChineseSimplifiedWriting
ChineseTraditionalLanguage
EnglishLanguage
Englishlanguage
FrenchLanguage
GermanLanguage
Hindi
ItalianLanguage
JapaneseLanguage
PortugueseLanguage
SpanishLanguage
SwedishLanguage
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 4744-4746
(
documentation
AdditionFn
JapaneseLanguage
"?NUMBER1 と ?NUMBER2 が
Number
の場合、 (
AdditionFn
?NUMBER1 ?NUMBER2) はこれらの数値の算術合計である。")
japanese_format.kif 878-879
(
domain
AdditionFn
1
RealNumber
)
Merge.kif 4740-4740
The number 1 argument of
addition
is an
instance
of
real number
(
domain
AdditionFn
2
RealNumber
)
Merge.kif 4741-4741
The number 2 argument of
addition
is an
instance
of
real number
(
identityElement
AdditionFn
0)
Merge.kif 5323-5323
0 is an
identity
element of
addition
(
instance
AdditionFn
AssociativeFunction
)
Merge.kif 4736-4736
Addition
is an
instance
of
associative function
(
instance
AdditionFn
BinaryFunction
)
Merge.kif 4735-4735
Addition
is an
instance
of
binary function
(
instance
AdditionFn
CommutativeFunction
)
Merge.kif 4737-4737
Addition
is an
instance
of
commutative function
(
instance
AdditionFn
TotalValuedRelation
)
Merge.kif 4739-4739
Addition
is an
instance
of
total valued relation
(
range
AdditionFn
RealNumber
)
Merge.kif 4742-4742
The
range
of
addition
is an instance of
real number
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 5427-5427
(
termFormat
ChineseLanguage
AdditionFn
"加法函数")
chinese_format.kif 683-683
(
termFormat
ChineseTraditionalLanguage
AdditionFn
"加成")
domainEnglishFormat.kif 5426-5426
(
termFormat
EnglishLanguage
AdditionFn
"addition")
domainEnglishFormat.kif 5425-5425
(
termFormat
de
AdditionFn
"AdditionFn")
terms-de.txt 263-263
(
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 3052-3073
If
equal
a symbolic string
and the reverse of
another symbolic string
and
equal
a nonnegative integer
and the
length
of
the other symbolic string
and
the nonnegative integer
is
greater
than 1 and
another nonnegative integer
is
greater
than 0 and
the other nonnegative integer
is
less
than
the nonnegative integer
and
equal
an integer
and the
ceiling
of (
the nonnegative integer
and 1) and 2 and
equal
the other nonnegative integer
EW and ((
the integer
and
the other nonnegative integer
) and
the integer
) and
equal
a third symbolic string
and the
sub
-string of
the other symbolic string
from
the other nonnegative integer
to (1 and
the other nonnegative integer
),
then
equal
the third symbolic string
and the
sub
-string of
the symbolic string
from
the other nonnegative integer
EW to (1 and
the other nonnegative integer
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 25562-25578
If
menopause
is an
attribute
of
a human
holds
during
a time interval
and
a day
is a
birthdate
of
the human
and
the day
is an
instance
of the
day
a positive integer
of month the
month
a kind of month
and
equal
a real number
and (49 and
an integer
) and
equal
another real number
and (52 and
the integer
) and
equal
a time point
and the
beginning
of
the time interval
,
then the statement
the time point
is
greater
than
the real number
and
the other real number
is
greater
than
the time point
has the
modal
force
of
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 1240-1249
If
a financial account
is an
instance
of
credit account
and
a cognitive agent
holds
account
the financial account
and
a real number
is a
principal
amount of
the financial account
and
a time interval
is an
agreement
period of
the financial account
and
the financial account
is
interest
earned
an interest
for
the time interval
and
equal
another real number
and (
the real number
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 1289-1298
If
a loan
is an
instance
of
loan
and
the loan
is the
borrower
of
a cognitive agent
and
a real number
is a
principal
amount of
the loan
and
a time interval
is an
agreement
period of
the loan
and
the loan
is
interest
earned
an interest
for
the time interval
and
equal
another real number
and (
the real number
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)
(
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 2350-2372
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 real number
an unit of measure
(s) 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
is
interest
earned
another real number
the unit of measure
(s) for
the time interval
and
equal
a third real number
and (
the real number
and
the other real number
),
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
account
of
the financial asset
and
the third real number
the unit of measure
(s) is a
transaction
amount of
the financial transaction
(=>
(
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 438-455
If
a financial transaction
is an
instance
of
deposit
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 real number
an unit of measure
(s) 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 real number
the unit of measure
(s) and
equal
a third real number
and (
the other real number
and
the real number
),
then
the financial account
current
account balance immediately
after
after
the financial transaction
for
the third real number
the unit of measure
(s)
(=>
(
and
(
instance
?LIST
ConsecutiveTimeIntervalList
)
(
equal
?T1
(
ListOrderFn
?LIST ?N))
(
equal
?T2
(
ListOrderFn
?LIST
(
AdditionFn
?N 1))))
(
equal
(
BeginFn
?T2)
(
EndFn
?T1)))
Weather.kif 2620-2629
If
a list
is an
instance
of
consecutive time interval list
and
equal
a time interval
and
an entity
element
of
the list
and
equal
another time interval
and (
a positive integer
and 1)th
element
of
the list
,
then
equal
the
beginning
of
the other time interval
and the
end
of
the time interval
(=>
(
and
(
not
(
equal
?NUMBER2 0))
(
equal
(
AdditionFn
(
MultiplicationFn
(
FloorFn
(
DivisionFn
?NUMBER1 ?NUMBER2)) ?NUMBER2) ?NUMBER) ?NUMBER1))
(
equal
(
RemainderFn
?NUMBER1 ?NUMBER2) ?NUMBER))
Merge.kif 5145-5156
If
equal
an integer
and 0 and
equal
(the
largest
integer less than or equal to
another integer
and
the integer
and
the integer
and
a third integer
) and
the other integer
,
then
equal
the other integer
mod
the integer
and
the third integer
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
A real number
is an
average
of
a list
if and only if there exist
another list
and
a positive integer
such that
equal
length
of
the other list
and
length
of
the list
and
equal
1th
element
of
the other list
and 1th
element
of
the list
and for all
another positive integer
if
the other positive integer
is a
member
of
the other list
,
then there exist
another real number
,
the other real number
MINUSONE,, ,
a third positive integer
and
a fourth positive integer
such that
the other real number
is
greater
than 1 and
the other real number
is
less
than or equal to
length
of
the other list
and
equal
the other positive integer
th
element
of
the other list
and
the other real number
and
the third positive integer
is a
member
of
the list
and
equal
the other real number
and
the third positive integer
th
element
of
the list
and
the fourth positive integer
is a
member
of
the other list
and
equal
the other real number
MINUSONE and (
the other real number
and 1) and
equal
the other real number
MINUSONE and
the fourth positive integer
th
element
of
the other list
and
equal
the other positive integer
and (
the third positive integer
and
the fourth positive integer
)
and
equal
the positive integer
and
length
of
the other list
and
equal
the real number
and
the positive integer
th
element
of
the other list
and
the positive integer
(=>
(
and
(
arcLength
?SEMI
(
MeasureFn
?L ?U))
(
equal
?SEMI
SemicircularArc
))
(
exists
(?CIR ?C)
(
and
(
equal
?CIR
Circle
)
(
geometricPart
?SEMI ?CIR)
(
circumference
?CIR
(
MeasureFn
?C ?U))
(
equal
?C
(
AdditionFn
?L ?L)))))
Mid-level-ontology.kif 5700-5710
If
a real number
an unit of measure
(s) is the
LengthMeasure
of
a circular arc
and
equal
the circular arc
and
semicircular arc
,
then there exist
a circle
and
another real number
such that
equal
the circle
and
circle
and
the circle
is a
geometric
part of
the circular arc
and
circumference
the circle
and
the other real number
the unit of measure
(s) and
equal
the other real number
and (
the real number
and
the real number
)
(=>
(
and
(
equal
(
PathWeightFn
?PATH) ?SUM)
(
graphPart
?ARC1 ?PATH)
(
graphPart
?ARC2 ?PATH)
(
arcWeight
?ARC1 ?NUMBER1)
(
arcWeight
?ARC2 ?NUMBER2)
(
forall
(?ARC3)
(=>
(
graphPart
?ARC3 ?PATH)
(
or
(
equal
?ARC3 ?ARC1)
(
equal
?ARC3 ?ARC2)))))
(
equal
(
PathWeightFn
?PATH)
(
AdditionFn
?NUMBER1 ?NUMBER2)))
Merge.kif 6018-6031
If
equal
the
value
of
a graph path
and
a real number
and
a graph arc
is a
part
of
the graph path
and
another graph arc
is a
part
of
the graph path
and the
value
of
the graph arc
is
another real number
and the
value
of
the other graph arc
is
a third real number
and for all
a graph element
if
the graph element
is a
part
of
the graph path
,
then
equal
the graph element
and
the graph arc
or
equal
the graph element
and
the other graph arc
,
then
equal
the
value
of
the graph path
and (
the other real number
and
the third real number
)
(=>
(
and
(
equal
(
PathWeightFn
?PATH) ?SUM)
(
subGraph
?SUBPATH ?PATH)
(
graphPart
?ARC1 ?PATH)
(
arcWeight
?ARC1 ?NUMBER1)
(
forall
(?ARC2)
(=>
(
graphPart
?ARC2 ?PATH)
(
or
(
graphPart
?ARC2 ?SUBPATH)
(
equal
?ARC2 ?ARC1)))))
(
equal
?SUM
(
AdditionFn
(
PathWeightFn
?SUBPATH) ?NUMBER1)))
Merge.kif 6004-6016
If
equal
the
value
of
a graph path
and
a real number
and
another graph path
is a
subgraph
of
the graph path
and
a graph arc
is a
part
of
the graph path
and the
value
of
the graph arc
is
another real number
and for all
a graph element
if
the graph element
is a
part
of
the graph path
,
then
the graph element
is a
part
of
the other graph path
or
equal
the graph element
and
the graph arc
,
then
equal
the real number
and (the
value
of
the other graph path
and
the other real number
)
(=>
(
and
(
equal
(
RemainderFn
?NUMBER1 ?NUMBER2) ?NUMBER)
(
not
(
equal
?NUMBER2 0)))
(
equal
(
AdditionFn
(
MultiplicationFn
(
FloorFn
(
DivisionFn
?NUMBER1 ?NUMBER2)) ?NUMBER2) ?NUMBER) ?NUMBER1))
Merge.kif 5132-5143
If
equal
an integer
mod
another integer
and
a third integer
and
equal
the other integer
and 0,
then
equal
(the
largest
integer less than or equal to
the integer
and
the other integer
and
the other integer
and
the third integer
) and
the integer
(=>
(
and
(
equal
?A
(
ListSumFn
?L))
(
greaterThan
(
ListLengthFn
?L) 1))
(
equal
?A
(
AdditionFn
(
FirstFn
?L)
(
ListSumFn
(
SubListFn
2
(
ListLengthFn
?L) ?L)))))
Merge.kif 3271-3281
If
equal
a real number
and the
sum
of
a list
and
length
of
the list
is
greater
than 1,
then
equal
the real number
and (the
first
of
the list
and the
sum
of the sub-list from 2 to
length
of
the list
of
the list
)
(=>
(
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 3096-3115
If
equal
a list
and the
list
composed of
another list
and
a third list
and
equal
the other list
and
null list
and
equal
the third list
and
null list
and
a positive integer
is
less
than or equal to
length
of
the other list
and
another positive integer
is
less
than or equal to
length
of
the third list
and
the positive integer
is an
instance
of
positive integer
and
the other positive integer
is an
instance
of
positive integer
,
then
equal
the positive integer
th
element
of
the list
and
the positive integer
th
element
of
the other list
and
equal
(
length
of
the other list
and
the other positive integer
)th
element
of
the list
and
the other positive integer
th
element
of
the third list
(=>
(
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 3052-3073
If
equal
a symbolic string
and the reverse of
another symbolic string
and
equal
a nonnegative integer
and the
length
of
the other symbolic string
and
the nonnegative integer
is
greater
than 1 and
another nonnegative integer
is
greater
than 0 and
the other nonnegative integer
is
less
than
the nonnegative integer
and
equal
an integer
and the
ceiling
of (
the nonnegative integer
and 1) and 2 and
equal
the other nonnegative integer
EW and ((
the integer
and
the other nonnegative integer
) and
the integer
) and
equal
a third symbolic string
and the
sub
-string of
the other symbolic string
from
the other nonnegative integer
to (1 and
the other nonnegative integer
),
then
equal
the third symbolic string
and the
sub
-string of
the symbolic string
from
the other nonnegative integer
EW to (1 and
the other nonnegative integer
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 3203-3215
If
equal
a list
and the sub-list from
a positive integer
to
an integer
of
another list
and (
the integer
and
the positive integer
) is
greater
than 1,
then
equal
the list
and the
list
composed of (
the positive integer
th
element
of
the other list
) and the sub-list from (1 and
the positive integer
) to
the integer
of
the other list
(=>
(
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 2139-2151
If
equal
a real number
and
VarianceAverageFn
of
a list
with the mean of
a number
and
length
of
the list
is
greater
than 1,
then
equal
the real number
and (
VarianceAverageFn
of 1th
element
of
the list
with the mean of
the number
and
VarianceAverageFn
of the sub-list from 2 to
length
of
the list
of
the list
with the mean of
the number
)
(=>
(
and
(
instance
?AREA
GeographicArea
)
(
objectGeographicCoordinates
?AREA ?LAT ?LONG)
(
equal
(
MeasureFn
?DEG
AngularDegree
)
(
MagneticDeclinationFn
?LAT ?LONG)))
(
exists
(?MN)
(
and
(
headingWRTMagneticNorth
?AREA
(
MeasureFn
?MN
AngularDegree
))
(
headingWRTTrueNorth
?AREA
(
MeasureFn
(
AdditionFn
?MN ?DEG)
AngularDegree
)))))
Geography.kif 3917-3929
If
an object
is an
instance
of
geographic area
and
the object
is
object
geographic coordinates
a latitude
for
a longitude
and
equal
a real number
angular degree
(s) and Location on Earth at Latitude
the latitude
and Longitude
the longitude
has a magnetic declination of
PlaneAngleMeasure
. (+) denotes easterly declination, (-) denotes westerly declination. zero value means at the agonic line.,
then there exists
another real number
such that
the other real number
angular degree
(s) is a
headingWRT
magnetic north of
the object
and (
the other real number
and
the real number
)
angular degree
(s) is a
headingWRT
true north of
the object
(=>
(
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 1249-1263
If
an object
is an
instance
of
mixture
and
an unit of measure
is an
instance
of
unit of measure
and A
Mixture
containing
a real number
unit
the unit of measure
of
a substance
and
another real number
unit
the unit of measure
of
another substance
and the
measure
of
the object
is
a third real number
the unit of measure
(s) and
the substance
is a
part
of
the object
and
the other substance
is a
part
of
the object
and the
measure
of
the substance
is
the real number
the unit of measure
(s) and the
measure
of
the other substance
is
the other real number
the unit of measure
(s),
then
equal
the third real number
and (
the real number
and
the other real number
)
(=>
(
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 71-87
If
a process
is an
instance
of
bar mitzvah
and
a human
is a
patient
of
the process
and
the human
is an
instance
of
boy
and
the human
is a
member
of
a collection
and
the collection
is an
instance
of
judaism
and
a day
is a
birthdate
of
the human
and
the day
is an
instance
of the
day
a positive integer
of month the
month
a kind of month
,
then there exist
an integer
and
a time position
such that
the integer
is an
instance
of
integer
and
equal
the integer
and (
another integer
and 13) and
the time position
is an
instance
of the
day
the positive integer
of month the
month
a kind of month
and
equal
the
time
of existence of
the process
and immediately
after
the time position
(=>
(
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 102-118
If
a process
is an
instance
of
bat mitzvah
and
a human
is a
patient
of
the process
and
the human
is an
instance
of
girl
and
the human
is a
member
of
a collection
and
the collection
is an
instance
of
judaism
and
a day
is a
birthdate
of
the human
and
the day
is an
instance
of the
day
a positive integer
of month the
month
a kind of month
,
then there exist
an integer
and
a time position
such that
the integer
is an
instance
of
integer
and
equal
the integer
and (
another integer
and 13) and
the time position
is an
instance
of the
day
the positive integer
of month the
month
a kind of month
and
equal
the
time
of existence of
the process
and immediately
after
the time position
(=>
(
and
(
instance
?UNIT
UnitOfArea
)
(
landAreaOnly
?AREA
(
MeasureFn
?LAND ?UNIT))
(
waterAreaOnly
?AREA
(
MeasureFn
?WATER ?UNIT)))
(
totalArea
?AREA
(
MeasureFn
(
AdditionFn
?LAND ?WATER) ?UNIT)))
Geography.kif 692-697
If
an unit of measure
is an
instance
of
unit of area
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
(
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 17381-17387
If
a time position
is an
instance
of the
hour
a nonnegative integer
and
another time position
is an
instance
of the
hour
another nonnegative integer
and
equal
the time
the time position
in zone
central time zone
and
the other time position
,
then
equal
the other nonnegative integer
and (
the nonnegative integer
and 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 17393-17399
If
a time position
is an
instance
of the
hour
a nonnegative integer
and
another time position
is an
instance
of the
hour
another nonnegative integer
and
equal
the time
the time position
in zone
eastern time zone
and
the other time position
,
then
equal
the other nonnegative integer
and (
the nonnegative integer
and 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 17369-17375
If
a time position
is an
instance
of the
hour
a nonnegative integer
and
another time position
is an
instance
of the
hour
another nonnegative integer
and
equal
the time
the time position
in zone
mountain time zone
and
the other time position
,
then
equal
the other nonnegative integer
and (
the nonnegative integer
and 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 17357-17363
If
a time position
is an
instance
of the
hour
a nonnegative integer
and
another time position
is an
instance
of the
hour
another nonnegative integer
and
equal
the time
the time position
in zone
pacific time zone
and
the other time position
,
then
equal
the other nonnegative integer
and (
the nonnegative integer
and 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
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
unit of length
,
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
(
MeasureFn
?LENGTH ?UNIT))
(
lengthOfPavedHighway
?AREA
(
MeasureFn
?LENGTH1 ?UNIT))
(
lengthOfUnpavedHighway
?AREA
(
MeasureFn
?LENGTH2 ?UNIT)))
(
equal
?LENGTH
(
AdditionFn
?LENGTH1 ?LENGTH2)))
Transportation.kif 503-508
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
,
then
equal
the real number
and (
the real number
1 and
the real number
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 7438-7446
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
equal
the positive integer
and (
the other positive integer
and 1) or
equal
the other positive integer
and (
the positive integer
and 1)
statement
(
forall
(?NUMBER)
(
equal
(
SuccessorFn
?NUMBER)
(
AdditionFn
?NUMBER 1)))
Merge.kif 4748-4749
For all
an integer
equal
(
the integer
+1) and (
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 3.0 is
open source software
produced by
Articulate Software
and its partners