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
Entity
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 4714-4716
(
documentation
AdditionFn
JapaneseLanguage
"?NUMBER1 と ?NUMBER2 が
Number
の場合、 (
AdditionFn
?NUMBER1 ?NUMBER2) はこれらの数値の算術合計である。")
japanese_format.kif 878-879
(
domain
AdditionFn
1
RealNumber
)
Merge.kif 4710-4710
The number 1 argument of
addition
is an
instance
of
real number
(
domain
AdditionFn
2
RealNumber
)
Merge.kif 4711-4711
The number 2 argument of
addition
is an
instance
of
real number
(
identityElement
AdditionFn
0)
Merge.kif 5293-5293
0 is an
identity
element of
addition
(
instance
AdditionFn
AssociativeFunction
)
Merge.kif 4706-4706
Addition
is an
instance
of
associative function
(
instance
AdditionFn
BinaryFunction
)
Merge.kif 4705-4705
Addition
is an
instance
of
binary function
(
instance
AdditionFn
CommutativeFunction
)
Merge.kif 4707-4707
Addition
is an
instance
of
commutative function
(
instance
AdditionFn
TotalValuedRelation
)
Merge.kif 4709-4709
Addition
is an
instance
of
total valued relation
(
range
AdditionFn
RealNumber
)
Merge.kif 4712-4712
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 5423-5423
(
termFormat
ChineseLanguage
AdditionFn
"加法函数")
chinese_format.kif 683-683
(
termFormat
ChineseTraditionalLanguage
AdditionFn
"加成")
domainEnglishFormat.kif 5422-5422
(
termFormat
EnglishLanguage
AdditionFn
"addition")
domainEnglishFormat.kif 5421-5421
(
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
If
a symbolic string
is
equal
to the reverse of
another symbolic string
and
a nonnegative integer
is
equal
to 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
an integer
is
equal
to the
ceiling
of (
the nonnegative integer
and 1) and 2 and
the other nonnegative integer
EW is
equal
to ((
the integer
and
the other nonnegative integer
) and
the integer
) and
a third symbolic string
is
equal
to the
sub_string
of
the other symbolic string
from
the other nonnegative integer
to (1 and
the other nonnegative integer
),
then
the third symbolic string
is
equal
to 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 24236-24252
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
and
a real number
is
equal
to (49 and
an integer
) and
another real number
is
equal
to (52 and
the integer
) and
a time point
is
equal
to 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 1224-1233
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
another real number
is
equal
to (
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 1273-1282
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
another real number
is
equal
to (
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 2333-2355
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
a third real number
is
equal
to (
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 436-453
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
a third real number
is
equal
to (
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 1918-1927
If
a list
is an
instance
of
consecutive time interval list
and
a time interval
is
equal
to
an entity
element
of
the list
and
another time interval
is
equal
to (
a positive integer
and 1)th
element
of
the list
,
then the
beginning
of
the other time interval
is
equal
to 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 5115-5126
If
an integer
is not
equal
to 0 and (the
largest
integer less than or equal to
another integer
and
the integer
and
the integer
and
a third integer
) is
equal
to
the other integer
,
then
the other integer
mod
the integer
is
equal
to
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
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
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
the other positive integer
th
element
of
the other list
is
equal
to
the other real number
and
the third positive integer
is a
member
of
the list
and
the other real number
is
equal
to
the third positive integer
th
element
of
the list
and
the fourth positive integer
is a
member
of
the other list
and
the other real number
MINUSONE is
equal
to (
the other real number
and 1) and
the other real number
MINUSONE is
equal
to
the fourth positive integer
th
element
of
the other list
and
the other positive integer
is
equal
to (
the third positive integer
and
the fourth positive integer
)
and
the positive integer
is
equal
to
length
of
the other list
and
the real number
is
equal
to
the positive integer
th
element
of
the other list
and
the positive integer
(=>
(
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 5988-6001
If the
value
of
a graph path
is
equal
to
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
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 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 5974-5986
If the
value
of
a graph path
is
equal
to
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
the graph element
is
equal
to
the graph arc
,
then
the real number
is
equal
to (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 5102-5113
If
an integer
mod
another integer
is
equal
to
a third integer
and
the other integer
is not
equal
to 0,
then (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
(
equal
?A
(
ListSumFn
?L))
(
greaterThan
(
ListLengthFn
?L) 1))
(
equal
?A
(
AdditionFn
(
FirstFn
?L)
(
ListSumFn
(
SubListFn
2
(
ListLengthFn
?L) ?L)))))
Merge.kif 3259-3269
If
a real number
is
equal
to the
sum
of
a list
and
length
of
the list
is
greater
than 1,
then
the real number
is
equal
to (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 3084-3103
If
a list
is
equal
to the
list
composed of
another list
and
a third list
and
the other list
is not
equal
to
null list
and
the third list
is not
equal
to
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
the positive integer
th
element
of
the list
is
equal
to
the positive integer
th
element
of
the other list
and (
length
of
the other list
and
the other positive integer
)th
element
of
the list
is
equal
to
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 3050-3071
If
a symbolic string
is
equal
to the reverse of
another symbolic string
and
a nonnegative integer
is
equal
to 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
an integer
is
equal
to the
ceiling
of (
the nonnegative integer
and 1) and 2 and
the other nonnegative integer
EW is
equal
to ((
the integer
and
the other nonnegative integer
) and
the integer
) and
a third symbolic string
is
equal
to the
sub_string
of
the other symbolic string
from
the other nonnegative integer
to (1 and
the other nonnegative integer
),
then
the third symbolic string
is
equal
to 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 3191-3203
If
a list
is
equal
to 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
the list
is
equal
to 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 1437-1449
If
a real number
is
equal
to
VarianceAverageFn
of
a list
with the mean of
a number
and
length
of
the list
is
greater
than 1,
then
the real number
is
equal
to (
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
?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
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
the third real number
is
equal
to (
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 69-85
If
a process
is an
instance
of
BarMitzvah
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
,
then there exist
an integer
and
a time position
such that
the integer
is an
instance
of
integer
and
the integer
is
equal
to (
another integer
and 13) and
the time position
is an
instance
of the
day
the positive integer
and the
time
of existence of
the process
is
equal
to 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 99-115
If
a process
is an
instance
of
BatMitzvah
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
,
then there exist
an integer
and
a time position
such that
the integer
is an
instance
of
integer
and
the integer
is
equal
to (
another integer
and 13) and
the time position
is an
instance
of the
day
the positive integer
and the
time
of existence of
the process
is
equal
to 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 555-560
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 17283-17289
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 the time
the time position
in zone
central time zone
is
equal
to
the other time position
,
then
the other nonnegative integer
is
equal
to (
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 17295-17301
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 the time
the time position
in zone
eastern time zone
is
equal
to
the other time position
,
then
the other nonnegative integer
is
equal
to (
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 17271-17277
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 the time
the time position
in zone
mountain time zone
is
equal
to
the other time position
,
then
the other nonnegative integer
is
equal
to (
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 17259-17265
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 the time
the time position
in zone
pacific time zone
is
equal
to
the other time position
,
then
the other nonnegative integer
is
equal
to (
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
the real number
is
equal
to (
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 6495-6503
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)
statement
(
forall
(?NUMBER)
(
equal
(
SuccessorFn
?NUMBER)
(
AdditionFn
?NUMBER 1)))
Merge.kif 4718-4719
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 3.0 is
open source software
produced by
Articulate Software
and its partners