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
DivisionFn
Sigma KEE - DivisionFn
DivisionFn
appearance as argument number 1
No TPTP formula. May not be expressible in strict first order.
chinese_format.kif 2220-2223
No TPTP formula. May not be expressible in strict first order.
Merge.kif 4746-4750
No TPTP formula. May not be expressible in strict first order.
japanese_format.kif 884-887
No TPTP formula. May not be expressible in strict first order.
Merge.kif 4742-4742
除法函数
的 1 数量 是
实数
的
instance
No TPTP formula. May not be expressible in strict first order.
Merge.kif 4743-4743
除法函数
的 2 数量 是
实数
的
instance
No TPTP formula. May not be expressible in strict first order.
Merge.kif 5297-5297
1 是
除法函数
的单位元
No TPTP formula. May not be expressible in strict first order.
Merge.kif 4739-4739
除法函数
是
二元函数
的
instance
No TPTP formula. May not be expressible in strict first order.
Merge.kif 4741-4741
除法函数
是
部分值关系
的
instance
No TPTP formula. May not be expressible in strict first order.
Merge.kif 4744-4744
除法函数
的
range
是
实数
的实例
appearance as argument number 2
No TPTP formula. May not be expressible in strict first order.
chinese_format.kif 686-686
No TPTP formula. May not be expressible in strict first order.
english_format.kif 688-688
No TPTP formula. May not be expressible in strict first order.
french_format.kif 416-416
No TPTP formula. May not be expressible in strict first order.
relations-it.txt 80-80
No TPTP formula. May not be expressible in strict first order.
japanese_format.kif 2133-2133
No TPTP formula. May not be expressible in strict first order.
portuguese_format.kif 368-368
No TPTP formula. May not be expressible in strict first order.
relations-cz.txt 425-425
No TPTP formula. May not be expressible in strict first order.
relations-de.txt 893-893
No TPTP formula. May not be expressible in strict first order.
relations-hindi.txt 120-120
No TPTP formula. May not be expressible in strict first order.
relations-ro.kif 438-438
No TPTP formula. May not be expressible in strict first order.
relations-sv.txt 460-460
No TPTP formula. May not be expressible in strict first order.
relations-cb.txt 114-114
No TPTP formula. May not be expressible in strict first order.
domainEnglishFormat.kif 19992-19992
No TPTP formula. May not be expressible in strict first order.
chinese_format.kif 687-687
No TPTP formula. May not be expressible in strict first order.
domainEnglishFormat.kif 19991-19991
No TPTP formula. May not be expressible in strict first order.
domainEnglishFormat.kif 19990-19990
No TPTP formula. May not be expressible in strict first order.
relations-tg.txt 176-176
antecedent
No TPTP formula. May not be expressible in strict first order.
Mid-level-ontology.kif 17948-17959
如果 1 的
approximate
diameter
是 %2 和
客体
的
radius
是
实数
和 2.0
那个 实数
M 和
那个 客体
的
measure
是
另一个 实数
另一个 测量单位
和
自身连接物体
的
measure
是
第三 实数
那个 另外 测量单位
和
那个 实数
M 是
UnitOfLength
的
instance
和
那个 另外 测量单位
是
UnitOfVolume
的
instance
,
然后
那个 另外 实数
equal
那个 第三 实数
No TPTP formula. May not be expressible in strict first order.
Media.kif 3068-3089
如果
符号串
equal
ReverseFn
另一个 符号串
和
非负整数
equal
那个 另外 符号串
的
length
和
那个 非负整数
是
greaterThan
1 和
另一个 非负整数
是
greaterThan
0 和
那个 另外 非负整数
是
lessThan
那个 非负整数
和
整数
equal
取(
那个 非负整数
和 1) 和 2 的顶整数 和
那个 另外 非负整数
EW
equal
((
那个 整数
和
那个 另外 非负整数
) 和
那个 整数
) 和
第三 符号串
equal
那个 另外 符号串
的
sub
-string 从
那个 另外 非负整数
对于 (1 和
那个 另外 非负整数
) ,
然后
那个 第三 符号串
equal
那个 符号串
的
sub
-string 从
那个 另外 非负整数
EW 对于 (1 和
那个 另外 非负整数
EW)
No TPTP formula. May not be expressible in strict first order.
Economy.kif 4645-4658
如果
客体
是
CoffeeArabica
的
instance
和
那个 客体
的
measure
是
实数
公克
和
那个 客体
C 是
Caffeine
的
instance
和
那个 客体
C 是
那个 客体
的
part
和
那个 客体
C 的
measure
是
另一个 实数
公克
和
第三 实数
equal
那个 另外 实数
和
那个 实数
,
然后
那个 第三 实数
是
greaterThanOrEqualTo
0.008 和
那个 第三 实数
是
lessThanOrEqualTo
0.014
No TPTP formula. May not be expressible in strict first order.
Economy.kif 4669-4682
如果
客体
是
CoffeeRobusta
的
instance
和
那个 客体
的
measure
是
实数
公克
和
那个 客体
C 是
Caffeine
的
instance
和
那个 客体
C 是
那个 客体
的
part
和
那个 客体
C 的
measure
是
另一个 实数
公克
和
第三 实数
equal
那个 另外 实数
和
那个 实数
,
然后
那个 第三 实数
是
greaterThanOrEqualTo
0.017 和
那个 第三 实数
是
lessThanOrEqualTo
0.04
No TPTP formula. May not be expressible in strict first order.
Geography.kif 2215-2225
如果
实数
测量单位
是
地理区域
的
irrigated
土地 和
那个 测量单位
是
UnitOfArea
的
instance
和
另一个 实数
那个 测量单位
是
那个 地理区域
的
total
區域 和
第三 实数
equal
那个 实数
和
那个 另外 实数
,
然后
那个 第三 实数
那个 测量单位
是
那个 地理区域
的
irrigated
土地
No TPTP formula. May not be expressible in strict first order.
Geography.kif 2227-2237
如果
实数
测量单位
是
地理区域
的
irrigated
土地 和
另一个 实数
那个 测量单位
是
那个 地理区域
的
total
區域 和
那个 测量单位
是
UnitOfArea
的
instance
和
第三 实数
equal
那个 实数
和
那个 另外 实数
,
然后
那个 第三 实数
那个 测量单位
是
那个 地理区域
的
irrigated
土地
No TPTP formula. May not be expressible in strict first order.
ComputingBrands.kif 3735-3756
如果
客体
的
measure
是
实数
流明
和
另一个 客体
的
measure
是
另一个 实数
流明
和
那个 客体
是
第三 客体
的
part
和
那个 另外 客体
是
那个 第三 客体
的
part
和
那个 客体
不
equal
那个 另外 客体
和
那个 实数
是
greaterThan
那个 另外 实数
和
那个 实数
和
那个 另外 实数
equal
第三 实数
和
contrastRatio
那个 第三 客体
and
那个 第三 实数
,
然后 不存在
第四 客体
,
第五 客体
,, ,
第四 实数
, and 和
第五 实数
这样
那个 第四 客体
的
measure
是
那个 第四 实数
流明
和
那个 第五 客体
的
measure
是
那个 第五 实数
流明
和
那个 第四 客体
是
那个 第三 客体
的
part
和
那个 第五 客体
是
那个 第三 客体
的
part
和
那个 第四 客体
不
equal
那个 第五 客体
和
那个 第四 实数
是
greaterThan
那个 第五 实数
和
那个 第四 实数
和
那个 第五 实数
是
greaterThan
那个 第三 实数
No TPTP formula. May not be expressible in strict first order.
Merge.kif 5117-5128
如果
整数
不
equal
0 和 (取
另一个 整数
和
那个 整数
的底整数 和
那个 整数
和
第三 整数
)
equal
那个 另外 整数
,
然后
那个 另外 整数
模除
那个 整数
equal
那个 第三 整数
No TPTP formula. May not be expressible in strict first order.
FinancialOntology.kif 538-548
如果
实数
测量单位
是
金融账户
的
principal
总额 和
另一个 实数
是
那个 金融账户
的
fixed
固定利息 和
那个 金融账户
是 对于
时距
的
simple
利息
第三 实数
那个 测量单位
和
那个 另外 实数
-Decimal
equal
那个 另外 实数
和 100,
然后
那个 第三 实数
equal
那个 实数
和
那个 另外 实数
-Decimal
No TPTP formula. May not be expressible in strict first order.
FinancialOntology.kif 587-597
如果
金融账户
是 对于
时距
的
simple
利息
实数
测量单位
和
另一个 实数
那个 测量单位
是
那个 金融账户
的
principal
总额 和
第三 实数
-Decimal
equal
那个 实数
和
那个 另外 实数
和
那个 第三 实数
equal
那个 第三 实数
-Decimal 和 100.0,
然后
那个 金融账户
是 对于
那个 时距
每周期
那个 第三 实数
的
interest
速率
consequent
No TPTP formula. May not be expressible in strict first order.
People.kif 82-97
年
是
整数
year
的
instance
和
地缘政治区域
和
那个 年
每一千的
births
equal
实数
若且唯若
那个 地缘政治区域
的
population
和 1000
equal
另一个 实数
和
另一个 整数
equal
符号串
所描述的类别
instance
的数量 和
那个 另外 整数
和
那个 另外 实数
equal
那个 实数
No TPTP formula. May not be expressible in strict first order.
People.kif 118-133
年
是
整数
year
的
instance
和
地缘政治区域
和
那个 年
每一千里的
deaths
equal
实数
若且唯若
那个 地缘政治区域
的
population
和 1000
equal
另一个 实数
和
另一个 整数
equal
符号串
所描述的类别
instance
的数量 和
那个 另外 整数
和
那个 另外 实数
equal
那个 实数
No TPTP formula. May not be expressible in strict first order.
People.kif 238-264
年
是
整数
year
的
instance
和
地缘政治区域
和
那个 年
每一千个生存出生里的
deaths
equal
实数
若且唯若
另一个 整数
equal
符号串
所描述的类别
instance
的数量 和
那个 另外 整数
和 1000
equal
另一个 实数
和
第三 整数
equal
另一个 符号串
所描述的类别
instance
的数量 和
那个 第三 整数
和
那个 另外 实数
equal
那个 实数
No TPTP formula. May not be expressible in strict first order.
People.kif 156-187
年
是
整数
year
的
instance
和
地缘政治区域
和
那个 年
每一千的
migrants
equal
实数
若且唯若 (
那个 整数
和
另一个 整数
)
equal
1 和
实体
是
那个 另外 整数
year
的
instance
和
那个 地缘政治区域
的
population
equal
另一个 实数
在
那个 年
holdsDuring
和
那个 另外 实数
和 1000
equal
第三 实数
和
第三 整数
equal
符号串
所描述的类别
instance
的数量 和
第四 整数
equal
那个 符号串
所描述的类别
instance
的数量 和 (
那个 第三 整数
和
那个 第四 整数
)
equal
第四 实数
和
那个 第四 实数
和
那个 第三 实数
equal
那个 实数
No TPTP formula. May not be expressible in strict first order.
People.kif 52-64
年
是
整数
year
的
instance
和
地缘政治区域
和
那个 年
的
population
成长
equal
实数
若且唯若 (
那个 整数
和
那个 整数
P)
equal
1 和
时间位置
是
那个 整数
P
year
的
instance
和
那个 地缘政治区域
的
population
equal
另一个 实数
在
那个 年
holdsDuring
和
那个 地缘政治区域
的
population
equal
第三 实数
在
那个 时间位置
holdsDuring
和
那个 另外 实数
和
那个 第三 实数
equal
第四 实数
和 (
那个 第四 实数
和 1)
equal
那个 实数
No TPTP formula. May not be expressible in strict first order.
People.kif 272-293
实数
是
串列
的
average
若且唯若 有存在
另一个 串列
和
正整数
这样
那个 另外 串列
的长度
equal
那个 串列
的长度 和
那个 另外 串列
的第 1 几个元素
equal
那个 串列
的第 1 几个元素 和 对所有
另一个 正整数
如果
那个 另外 正整数
是
那个 另外 串列
的
member
,
然后 有存在
另一个 实数
,
那个 另外 实数
MINUSONE,, ,
第三 正整数
, and 和
第四 正整数
这样
那个 另外 实数
是
greaterThan
1 和
那个 另外 实数
是
lessThanOrEqualTo
那个 另外 串列
的长度 和
那个 另外 串列
的第
那个 另外 正整数
几个元素
equal
那个 另外 实数
和
那个 第三 正整数
是
那个 串列
的
member
和
那个 另外 实数
equal
那个 串列
的第
那个 第三 正整数
几个元素 和
那个 第四 正整数
是
那个 另外 串列
的
member
和
那个 另外 实数
MINUSONE
equal
(
那个 另外 实数
和 1) 和
那个 另外 实数
MINUSONE
equal
那个 另外 串列
的第
那个 第四 正整数
几个元素 和
那个 另外 正整数
equal
(
那个 第三 正整数
和
那个 第四 正整数
)
和
那个 正整数
equal
那个 另外 串列
的长度 和
那个 实数
equal
那个 另外 串列
的第
那个 正整数
几个元素 和
那个 正整数
No TPTP formula. May not be expressible in strict first order.
People.kif 1528-1539
百分之
实数
在
信仰团体
的人相信
那个 信仰团体
若且唯若 有存在
群体
,
另一个 群体
,, ,
物理
,, ,
那个 物理
2,, ,
那个 实数
1, and 和
那个 实数
2 这样
那个 物理
是
located
在
地理区域
和
那个 物理
是
那个 信仰团体
的
member
和
那个 物理
是
那个 群体
的
member
和
那个 实数
1 是
那个 群体
的
member
计数 和
那个 物理
2 是
located
在
那个 地理区域
和
那个 物理
2 是
那个 另外 群体
的
member
和
那个 实数
2 是
那个 另外 群体
的
member
计数 和
那个 实数
和 100
equal
那个 实数
1 和
那个 实数
2
No TPTP formula. May not be expressible in strict first order.
Cars.kif 1928-1933
compressionRatio
发动机
and
实数
若且唯若
minCylinderVolume
那个 发动机
and
另一个 实数
测量单位
和
maxCylinderVolume
那个 发动机
and
那个 测量单位
AX
那个 测量单位
和
那个 实数
equal
那个 另外 实数
和
那个 测量单位
AX
No TPTP formula. May not be expressible in strict first order.
People.kif 206-223
地缘政治区域
的
male
对母性比率
equal
实数
若且唯若
整数
equal
符号串
所描述的类别
instance
的数量 和
另一个 整数
equal
另一个 符号串
所描述的类别
instance
的数量 和
那个 整数
和
那个 另外 整数
equal
那个 实数
No TPTP formula. May not be expressible in strict first order.
People.kif 1547-1558
实数
percent
的人在
地理区域
是
民族群组
若且唯若 有存在
群体
,
另一个 群体
,, ,
物理
,, ,
那个 物理
2,, ,
那个 实数
1, and 和
那个 实数
2 这样
那个 物理
是
located
在
那个 地理区域
和
那个 物理
是
那个 民族群组
的
member
和
那个 物理
是
那个 群体
的
member
和
那个 实数
1 是
那个 群体
的
member
计数 和
那个 物理
2 是
located
在
那个 地理区域
和
那个 物理
2 是
那个 另外 群体
的
member
和
那个 实数
2 是
那个 另外 群体
的
member
计数 和
那个 实数
和 100
equal
那个 实数
1 和
那个 实数
2
No TPTP formula. May not be expressible in strict first order.
People.kif 1566-1577
百分之
实数
的人在
地理区域
speak
语言
若且唯若 有存在
群体
,
另一个 群体
,, ,
有感知的主事
,, ,
那个 有感知的主事
2,, ,
那个 实数
1, and 和
那个 实数
2 这样
那个 有感知的主事
是
located
在
那个 地理区域
和
那个 有感知的主事
是
那个 群体
的
member
和
那个 语言
是
那个 有感知的主事
的
speaks
语言 和
那个 实数
1 是
那个 群体
的
member
计数 和
那个 有感知的主事
2 是
located
在
那个 地理区域
和
那个 有感知的主事
2 是
那个 另外 群体
的
member
和
那个 实数
2 是
那个 另外 群体
的
member
计数 和
那个 实数
和 100
equal
那个 实数
1 和
那个 实数
2
No TPTP formula. May not be expressible in strict first order.
Mid-level-ontology.kif 13326-13331
物理
的
measure
是
实数
OunceMass
若且唯若
那个 物理
的
measure
是
那个 实数
和 16.0
磅质量
No TPTP formula. May not be expressible in strict first order.
Merge.kif 5104-5115
如果
整数
模除
另一个 整数
equal
第三 整数
和
那个 另外 整数
不
equal
0,
然后 (取
那个 整数
和
那个 另外 整数
的底整数 和
那个 另外 整数
和
那个 第三 整数
)
equal
那个 整数
No TPTP formula. May not be expressible in strict first order.
Merge.kif 3277-3284
如果
实数
equal
AverageFn
串列
和
那个 串列
的长度 是
greaterThan
0,
然后
那个 实数
equal
ListSumFn
那个 串列
和
那个 串列
的长度
No TPTP formula. May not be expressible in strict first order.
Weather.kif 1475-1484
如果
实数
equal
方差函数
串列
和
另一个 实数
equal
AverageFn
那个 串列
,
然后
那个 实数
equal
方差均差函数
那个 另外 实数
and
那个 串列
和
那个 串列
的长度
No TPTP formula. May not be expressible in strict first order.
Cars.kif 4081-4113
如果
客体
是
BimetalTemperatureSensor
的
instance
和
另一个 客体
是
金属
的
instance
和
第三 客体
是
金属
的
instance
和
那个 另外 客体
不
equal
那个 第三 客体
和
那个 另外 客体
是
那个 客体
的
part
和
那个 第三 客体
是
那个 客体
的
part
和
实体
是
温度测量
的
instance
和
另一个 实体
是
温度测量
的
instance
和
实数
是
长度测量
的
instance
和
另一个 实数
是
长度测量
的
instance
和
第三 实数
是
长度测量
的
instance
和
第四 实数
是
长度测量
的
instance
和
那个 实体
不
equal
那个 另外 实体
和
时间位置
不
equal
另一个 时间位置
和
那个 客体
的
measure
是
那个 实体
和
那个 另外 客体
的
measure
是
那个 实数
和
那个 第三 客体
的
measure
是
那个 另外 实数
在
那个 时间位置
holdsDuring
和
那个 客体
的
measure
是
那个 另外 实体
和
那个 另外 客体
的
measure
是
那个 第三 实数
和
那个 第三 客体
的
measure
是
那个 第四 实数
在
那个 另外 时间位置
holdsDuring
,
然后
那个 实数
和
那个 另外 实数
不
equal
那个 第三 实数
和
那个 第四 实数
No TPTP formula. May not be expressible in strict first order.
UXExperimentalTerms.kif 3239-3259
如果
群体
是
群体
的
instance
和
实数
是
货币测量
的
instance
和
整数
是
实数
的
instance
和
那个 实数
equal
那个 群体
的
value
和
那个 整数
equal
符号串
所描述的类别
instance
的数量,
然后
那个 群体
的
average
price
equal
那个 实数
和
那个 整数
No TPTP formula. May not be expressible in strict first order.
UXExperimentalTerms.kif 2845-2870
如果
群体
是
群体
的
instance
和 对所有
物理
如果
那个 物理
是
那个 群体
的
member
,
然后
那个 物理
是
WebListing
的
instance
,
然后 有存在
实体
,
另一个 实体
, and 和
第三 实体
这样
那个 实体
所描述的类别
instance
的数量 和
那个 群体
instance
的数量
equal
在
那个 群体
的
bids
數字
No TPTP formula. May not be expressible in strict first order.
Cars.kif 1314-1348
如果
实体
是
EngineChoke
的
instance
和
设备上
是
那个 实体
的
attribute
在
过程
holdsDuring
和
设备关闭
是
那个 实体
的
attribute
在
另一个 过程
holdsDuring
和
自身连接物体
是
EngineCylinder
的
instance
和
恒量
是
那个 自身连接物体
的
capacity
和
那个 过程
是
FourStrokeCompression
的
instance
和
那个 另外 过程
是
FourStrokeCompression
的
instance
和
那个 过程
是
located
在
那个 自身连接物体
和
那个 另外 过程
是
located
在
那个 自身连接物体
和
客体
是
空气
的
instance
和
另一个 客体
是
汽油
的
instance
和
那个 客体
是
那个 恒量
IX1 的
part
和
那个 另外 客体
是
那个 恒量
IX1 的
part
和
那个 恒量
IX1 的
measure
是
那个 恒量
和
第四 客体
是
空气
的
instance
和
第五 客体
是
汽油
的
instance
和
那个 第四 客体
是
那个 恒量
IX2 的
part
和
那个 第五 客体
是
那个 恒量
IX2 的
part
和
那个 恒量
IX2 的
measure
是
那个 恒量
和
测量单位
是
测量单位
的
instance
和
那个 客体
的
measure
是
那个 客体
M
那个 测量单位
和
那个 第四 客体
的
measure
是
那个 第四 客体
M
那个 测量单位
和
那个 另外 客体
的
measure
是
那个 另外 客体
M
那个 测量单位
和
那个 第五 客体
的
measure
是
那个 第五 客体
M
那个 测量单位
,
然后
那个 第四 客体
M 和
那个 第五 客体
M 是
greaterThan
那个 客体
M 和
那个 另外 客体
M
No TPTP formula. May not be expressible in strict first order.
UXExperimentalTerms.kif 3095-3114
如果
试验
是
试验
的
instance
和
时距
是
时距
的
instance
,
然后
符号串
所描述的类别
instance
的数量 和
另一个 符号串
所描述的类别
instance
的数量
equal
purchases
per
user
在
那个 试验
期间
那个 时距
No TPTP formula. May not be expressible in strict first order.
UXExperimentalTerms.kif 3056-3073
如果
试验
是
试验
的
instance
和
实体
是
时距
的
instance
,
然后
符号串
所描述的类别
instance
的数量 和
另一个 符号串
所描述的类别
instance
的数量
equal
purchases
per
user
在
那个 试验
No TPTP formula. May not be expressible in strict first order.
Medicine.kif 5915-5924
如果
人类
是
人类成人
的
instance
和
那个 人类
的
measure
是
实数
Pounds
,
然后
bloodVolume
那个 人类
and
那个 实数
2
升
和
那个 实数
2
equal
那个 实数
和 0.07 和 2.33
No TPTP formula. May not be expressible in strict first order.
UXExperimentalTerms.kif 3721-3739
如果
SearchResultsPage
是
SearchResultsPage
的
instance
和
串列
是
SRPResults
的
instance
和
那个 串列
是
那个 SearchResultsPage
的
component
,
然后
符号串
所描述的类别
instance
的数量 和
那个 串列
的长度
equal
qualifying
clicks
在
那个 SearchResultsPage
No TPTP formula. May not be expressible in strict first order.
UXExperimentalTerms.kif 4563-4571
如果
实数
是
数量
的
instance
和
另一个 实数
是
数量
的
instance
,
然后
那个 实数
的
financial
improvement
百分比 在
那个 另外 实数
之上
equal
(
那个 实数
和
那个 另外 实数
) 和
那个 另外 实数
No TPTP formula. May not be expressible in strict first order.
ComputingBrands.kif 1570-1577
如果
辐射
是
辐射电磁
的
instance
和
那个 辐射
载波的频率是
实数
赫兹
和
那个 辐射
的
wavelength
是
另一个 实数
仪表
,
然后
那个 另外 实数
仪表
equal
299792458 和
那个 实数
仪表
Display limited to 25 items.
Show next 25
Display limited to 25 items.
Show next 25
statement
No TPTP formula. May not be expressible in strict first order.
Merge.kif 7367-7369
实数
圆周角度
equal
那个 实数
和
圆周率
和 180.0
弧度
No TPTP formula. May not be expressible in strict first order.
Merge.kif 7012-7014
实数
摄氏度
equal
(
那个 实数
和 32.0) 和 1.8
华氏度
No TPTP formula. May not be expressible in strict first order.
Merge.kif 7239-7241
实数
杯子
equal
那个 实数
和 2
品脱
No TPTP formula. May not be expressible in strict first order.
Merge.kif 7248-7250
实数
盎司
equal
那个 实数
和 8
杯子
No TPTP formula. May not be expressible in strict first order.
Merge.kif 7230-7232
实数
品脱
equal
那个 实数
和 2
夸脱
No TPTP formula. May not be expressible in strict first order.
Merge.kif 7221-7223
实数
夸脱
equal
那个 实数
和 4
美国加仑
No TPTP formula. May not be expressible in strict first order.
Mid-level-ontology.kif 13333-13336
对所有
实数
那个 实数
OunceMass
equal
那个 实数
和 16.0
磅质量
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