Browsing Interface
: Welcome guest :
log in
[
Home
| 
Graph
|  ]
KB:
SUMO
Language:
ChineseLanguage
ChinesePinyinWriting
ChineseSimplifiedWriting
ChineseTraditionalLanguage
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
PerformanceAct
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
AdditionFn
の数値 1 引数は
実数
の
instance
では
(
domain
AdditionFn
2
RealNumber
)
Merge.kif 4741-4741
AdditionFn
の数値 2 引数は
実数
の
instance
では
(
identityElement
AdditionFn
0)
Merge.kif 5323-5323
0 は
AdditionFn
の
identity
要素では
(
instance
AdditionFn
AssociativeFunction
)
Merge.kif 4736-4736
AdditionFn
は
結合関数
の
instance
では
(
instance
AdditionFn
BinaryFunction
)
Merge.kif 4735-4735
AdditionFn
は
2変数関数
の
instance
では
(
instance
AdditionFn
CommutativeFunction
)
Merge.kif 4737-4737
AdditionFn
は
可換関数
の
instance
では
(
instance
AdditionFn
TotalValuedRelation
)
Merge.kif 4739-4739
AdditionFn
は
合計値関係
の
instance
では
(
range
AdditionFn
RealNumber
)
Merge.kif 4742-4742
AdditionFn
の
range
は
実数
のインスタンス では
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
equal
記号文字列
and
ReverseFn
記号文字列
equal
非負整数
and
StringLengthFn
記号文字列
非負整数
は 1 より
greater
では
非負整数
は 0 より
greater
では
非負整数
は
非負整数
より
less
では
equal
整数
and (
非負整数
+ 1) + 2 の
ceiling
equal
非負整数
EW and ((
整数
+
非負整数
) +
整数
)
equal
記号文字列
and
SubstringFn
記号文字列
,
非負整数
and (1 +
非負整数
)
equal
記号文字列
and
SubstringFn
記号文字列
,
非負整数
EW and (1 +
非負整数
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
Menopausal
は
人[人間]
の
attribute
では は
時間間隔
の
during
holds
birthdate
人[人間]
and
日
日
は
正の整数
day
目 の
instance
では
equal
実数
and (49 +
整数
)
equal
実数
and (52 +
整数
)
equal
時点
and
時間間隔
の
beginning
ステートメント
時点
は
実数
より
greater
では
実数
は
時点
より
greater
では には
Likely
の
modal
force
が ある
(=>
(
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
FinancialAccount
は
CreditAccount
の
instance
では
accountHolder
FinancialAccount
and
認識エージェント
principalAmount
FinancialAccount
and
実数
agreementPeriod
FinancialAccount
and
時間間隔
interestEarned
FinancialAccount
,
Interest
and
時間間隔
equal
実数
and (
実数
+
Interest
)
認識エージェント
はタイプ
エンティティー
class
のタスクを実行する
obliged
(=>
(
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
Loan
は
Loan
の
instance
では
borrower
Loan
and
認識エージェント
principalAmount
Loan
and
実数
agreementPeriod
Loan
and
時間間隔
interestEarned
Loan
,
Interest
and
時間間隔
equal
実数
and (
実数
+
Interest
)
認識エージェント
はタイプ
エンティティー
class
のタスクを実行する
obliged
(=>
(
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
FinancialAsset
は
ZeroCouponBond
の
instance
では
maturityDate
AccountFn
FinancialAsset
and
日
FinancialAsset
Holder は
FinancialAsset
を
possess
es
principalAmount
AccountFn
FinancialAsset
and
実数
の
測定単位
(s)
agreementPeriod
AccountFn
FinancialAsset
and
時間間隔
interestEarned
AccountFn
FinancialAsset
,
実数
の
測定単位
(s) and
時間間隔
equal
実数
and (
実数
+
実数
)
金融取引
金融取引
は
Payment
の
instance
では
金融取引
は
FinancialAsset
Holder に
end
s
金融取引
は
AccountFn
FinancialAsset
から
originate
s
transactionAmount
金融取引
and
実数
の
測定単位
(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 438-455
金融取引
は
Deposit
の
instance
では
FinancialAccount
は
FinancialAccount
の
instance
では
金融取引
は
CurrencyFn
FinancialAccount
に
end
s
transactionAmount
金融取引
and
実数
の
測定単位
(s)
currentAccountBalance
FinancialAccount
,
金融取引
の
time
の existence の immediately
before
and
実数
の
測定単位
(s)
equal
実数
and (
実数
+
実数
)
currentAccountBalance
FinancialAccount
,
金融取引
の
after
の すぐ
after
and
実数
の
測定単位
(s)
(=>
(
and
(
instance
?LIST
ConsecutiveTimeIntervalList
)
(
equal
?T1
(
ListOrderFn
?LIST ?N))
(
equal
?T2
(
ListOrderFn
?LIST
(
AdditionFn
?N 1))))
(
equal
(
BeginFn
?T2)
(
EndFn
?T1)))
Weather.kif 2764-2773
リスト
は
ConsecutiveTimeIntervalList
の
instance
では
equal
時間間隔
and
リスト
の
エンティティー
element
equal
時間間隔
and
リスト
の (
正の整数
+ 1)th
element
equal
時間間隔
の
beginning
and
時間間隔
の
end
(=>
(
and
(
not
(
equal
?NUMBER2 0))
(
equal
(
AdditionFn
(
MultiplicationFn
(
FloorFn
(
DivisionFn
?NUMBER1 ?NUMBER2)) ?NUMBER2) ?NUMBER) ?NUMBER1))
(
equal
(
RemainderFn
?NUMBER1 ?NUMBER2) ?NUMBER))
Merge.kif 5145-5156
equal
整数
and 0
equal
(
整数
+
整数
以下の
largest
整数 +
整数
+
整数
) and
整数
equal
整数
を
整数
で割った剰余数 and
整数
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
リスト
and
実数
リスト
正の整数
equal
リスト
の
length
and
リスト
の
length
equal
リスト
の 1th
element
and
リスト
の 1th
element
正の整数
正の整数
は
リスト
の
member
では
実数
実数
MINUSONE,
正の整数
and
正の整数
実数
は 1 より
greater
では
実数
は
リスト
の
length
より
less
または同等 では
equal
リスト
の
正の整数
th
element
and
実数
正の整数
は
リスト
の
member
では
equal
実数
and
リスト
の
正の整数
th
element
正の整数
は
リスト
の
member
では
equal
実数
MINUSONE and (
実数
+ 1)
equal
実数
MINUSONE and
リスト
の
正の整数
th
element
equal
正の整数
and (
正の整数
+
正の整数
)
equal
正の整数
and
リスト
の
length
equal
実数
and
リスト
の
正の整数
th
element
+
正の整数
(=>
(
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
arcLength
CircularArc
and
実数
の
測定単位
(s)
equal
CircularArc
and
SemicircularArc
Circle
実数
equal
Circle
and
Circle
geometricPart
CircularArc
and
Circle
circumference
Circle
and
実数
の
測定単位
(s)
equal
実数
and (
実数
+
実数
)
(=>
(
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
equal
グラフパス
の
value
and
実数
グラフアーク
は
グラフパス
の
part
では
グラフアーク
は
グラフパス
の
part
では
グラフアーク
の
value
は
実数
では
グラフアーク
の
value
は
実数
では
グラフ要素
グラフ要素
は
グラフパス
の
part
では
equal
グラフ要素
and
グラフアーク
equal
グラフ要素
and
グラフアーク
equal
グラフパス
の
value
and (
実数
+
実数
)
(=>
(
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
equal
グラフパス
の
value
and
実数
グラフパス
は
グラフパス
の
subgraph
では
グラフアーク
は
グラフパス
の
part
では
グラフアーク
の
value
は
実数
では
グラフ要素
グラフ要素
は
グラフパス
の
part
では
グラフ要素
は
グラフパス
の
part
では
equal
グラフ要素
and
グラフアーク
equal
実数
and (
グラフパス
の
value
+
実数
)
(=>
(
and
(
equal
(
RemainderFn
?NUMBER1 ?NUMBER2) ?NUMBER)
(
not
(
equal
?NUMBER2 0)))
(
equal
(
AdditionFn
(
MultiplicationFn
(
FloorFn
(
DivisionFn
?NUMBER1 ?NUMBER2)) ?NUMBER2) ?NUMBER) ?NUMBER1))
Merge.kif 5132-5143
equal
整数
を
整数
で割った剰余数 and
整数
equal
整数
and 0
equal
(
整数
+
整数
以下の
largest
整数 +
整数
+
整数
) and
整数
(=>
(
and
(
equal
?A
(
ListSumFn
?L))
(
greaterThan
(
ListLengthFn
?L) 1))
(
equal
?A
(
AdditionFn
(
FirstFn
?L)
(
ListSumFn
(
SubListFn
2
(
ListLengthFn
?L) ?L)))))
Merge.kif 3271-3281
equal
実数
and
ListSumFn
リスト
リスト
の
length
は 1 より
greater
では
equal
実数
and (
FirstFn
リスト
+
ListSumFn
SubListFn
2,
リスト
の
length
and
リスト
)
(=>
(
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
equal
リスト
and
リスト
と
リスト
で構成される
list
equal
リスト
and
NullList
equal
リスト
and
NullList
正の整数
は
リスト
の
length
より
less
または同等 では
正の整数
は
リスト
の
length
より
less
または同等 では
正の整数
は
正の整数
の
instance
では
正の整数
は
正の整数
の
instance
では
equal
リスト
の
正の整数
th
element
and
リスト
の
正の整数
th
element
equal
リスト
の (
リスト
の
length
+
正の整数
)th
element
and
リスト
の
正の整数
th
element
(=>
(
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
equal
記号文字列
and
ReverseFn
記号文字列
equal
非負整数
and
StringLengthFn
記号文字列
非負整数
は 1 より
greater
では
非負整数
は 0 より
greater
では
非負整数
は
非負整数
より
less
では
equal
整数
and (
非負整数
+ 1) + 2 の
ceiling
equal
非負整数
EW and ((
整数
+
非負整数
) +
整数
)
equal
記号文字列
and
SubstringFn
記号文字列
,
非負整数
and (1 +
非負整数
)
equal
記号文字列
and
SubstringFn
記号文字列
,
非負整数
EW and (1 +
非負整数
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
equal
リスト
and
SubListFn
正の整数
,
整数
and
リスト
(
整数
+
正の整数
) は 1 より
greater
では
equal
リスト
and (
リスト
の
正の整数
th
element
) と
SubListFn
(1 +
正の整数
),
整数
and
リスト
で構成される
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 2283-2295
equal
実数
and
VarianceAverageFn
数
and
リスト
リスト
の
length
は 1 より
greater
では
equal
実数
and (
VarianceAverageFn
数
and
リスト
の 1th
element
+
VarianceAverageFn
数
and
SubListFn
2,
リスト
の
length
and
リスト
)
(=>
(
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 3950-3962
オブジェクト
は
地理的地域
の
instance
では
objectGeographicCoordinates
オブジェクト
,
Latitude
and
Longitude
equal
実数
の
AngularDegree
(s) and
MagneticDeclinationFn
Latitude
and
Longitude
実数
headingWRTMagneticNorth
オブジェクト
and
実数
の
AngularDegree
(s)
headingWRTTrueNorth
オブジェクト
and (
実数
+
実数
) の
AngularDegree
(s)
(=>
(
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
オブジェクト
は
混合物
の
instance
では
測定単位
は
測定単位
の
instance
では
mixtureRatio
物質
,
物質
,
実数
,
実数
and
測定単位
オブジェクト
の
measure
は
実数
の
測定単位
(s) では
物質
は
オブジェクト
の
part
では
物質
は
オブジェクト
の
part
では
物質
の
measure
は
実数
の
測定単位
(s) では
物質
の
measure
は
実数
の
測定単位
(s) では
equal
実数
and (
実数
+
実数
)
(=>
(
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
工程
は
BarMitzvah
の
instance
では
人[人間]
は
工程
の
patient
では
人[人間]
は
Boy
の
instance
では
人[人間]
は
コレクション
の
member
では
コレクション
は
Judaism
の
instance
では
birthdate
人[人間]
and
日
日
は
正の整数
day
目 の
instance
では
整数
時間位置
整数
は
整数
の
instance
では
equal
整数
and (
整数
+ 13)
時間位置
は
正の整数
day
目 の
instance
では
equal
工程
の
time
の existence and
時間位置
の すぐ
after
(=>
(
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
工程
は
BatMitzvah
の
instance
では
人[人間]
は
工程
の
patient
では
人[人間]
は
Girl
の
instance
では
人[人間]
は
コレクション
の
member
では
コレクション
は
Judaism
の
instance
では
birthdate
人[人間]
and
日
日
は
正の整数
day
目 の
instance
では
整数
時間位置
整数
は
整数
の
instance
では
equal
整数
and (
整数
+ 13)
時間位置
は
正の整数
day
目 の
instance
では
equal
工程
の
time
の existence and
時間位置
の すぐ
after
(=>
(
and
(
instance
?UNIT
UnitOfArea
)
(
landAreaOnly
?AREA
(
MeasureFn
?LAND ?UNIT))
(
waterAreaOnly
?AREA
(
MeasureFn
?WATER ?UNIT)))
(
totalArea
?AREA
(
MeasureFn
(
AdditionFn
?LAND ?WATER) ?UNIT)))
Geography.kif 725-730
測定単位
は
UnitOfArea
の
instance
では
landAreaOnly
地理的地域
and
実数
の
測定単位
(s)
waterAreaOnly
地理的地域
and
実数
の
測定単位
(s)
totalArea
地理的地域
and (
実数
+
実数
) の
測定単位
(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 17381-17387
時間位置
は
非負整数
hour
目 の
instance
では
時間位置
は
非負整数
hour
目 の
instance
では
equal
ゾーン
CentralTimeZone
の時間
時間位置
and
時間位置
equal
非負整数
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
時間位置
は
非負整数
hour
目 の
instance
では
時間位置
は
非負整数
hour
目 の
instance
では
equal
ゾーン
EasternTimeZone
の時間
時間位置
and
時間位置
equal
非負整数
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
時間位置
は
非負整数
hour
目 の
instance
では
時間位置
は
非負整数
hour
目 の
instance
では
equal
ゾーン
MountainTimeZone
の時間
時間位置
and
時間位置
equal
非負整数
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
時間位置
は
非負整数
hour
目 の
instance
では
時間位置
は
非負整数
hour
目 の
instance
では
equal
ゾーン
PacificTimeZone
の時間
時間位置
and
時間位置
equal
非負整数
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
totalLengthOfHighwaySystem
地理的地域
and
実数
の
測定単位
(s)
lengthOfPavedHighway
地理的地域
and
実数
1 の
測定単位
(s)
lengthOfUnpavedHighway
地理的地域
and
実数
2 の
測定単位
(s)
測定単位
は
UnitOfLength
の
instance
では
totalLengthOfHighwaySystem
地理的地域
and (
実数
1 +
実数
2) の
測定単位
(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
地理的地域
and
実数
の
測定単位
(s)
lengthOfPavedHighway
地理的地域
and
実数
1 の
測定単位
(s)
lengthOfUnpavedHighway
地理的地域
and
実数
2 の
測定単位
(s)
equal
実数
and (
実数
1 +
実数
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
conjugate
合成物質
and
合成物質
正の整数
正の整数
protonNumber
合成物質
and
正の整数
protonNumber
合成物質
and
正の整数
equal
正の整数
and (
正の整数
+ 1)
equal
正の整数
and (
正の整数
+ 1)
statement
(
forall
(?NUMBER)
(
equal
(
SuccessorFn
?NUMBER)
(
AdditionFn
?NUMBER 1)))
Merge.kif 4748-4749
整数
equal
(
整数
+1) 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