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
equal
Sigma KEE - equal
equal
appearance as argument number 1
No TPTP formula. May not be expressible in strict first order.
chinese_format.kif 1391-1392
No TPTP formula. May not be expressible in strict first order.
japanese_format.kif 48-49
No TPTP formula. May not be expressible in strict first order.
spanish_format.kif 53-54
appearance as argument number 2
No TPTP formula. May not be expressible in strict first order.
chinese_format.kif 297-297
No TPTP formula. May not be expressible in strict first order.
english_format.kif 302-302
No TPTP formula. May not be expressible in strict first order.
french_format.kif 171-171
No TPTP formula. May not be expressible in strict first order.
relations-it.txt 96-96
No TPTP formula. May not be expressible in strict first order.
japanese_format.kif 1991-1991
No TPTP formula. May not be expressible in strict first order.
portuguese_format.kif 123-123
No TPTP formula. May not be expressible in strict first order.
relations-cz.txt 179-179
No TPTP formula. May not be expressible in strict first order.
relations-de.txt 387-387
No TPTP formula. May not be expressible in strict first order.
relations-hindi.txt 136-136
No TPTP formula. May not be expressible in strict first order.
relations-ro.kif 191-191
No TPTP formula. May not be expressible in strict first order.
relations-sv.txt 178-178
No TPTP formula. May not be expressible in strict first order.
relations-tg.txt 205-205
No TPTP formula. May not be expressible in strict first order.
chinese_format.kif 298-298
No TPTP formula. May not be expressible in strict first order.
domainEnglishFormat.kif 22317-22317
No TPTP formula. May not be expressible in strict first order.
domainEnglishFormat.kif 22316-22316
No TPTP formula. May not be expressible in strict first order.
relations-tg.txt 206-206
antecedent
No TPTP formula. May not be expressible in strict first order.
Merge.kif 4769-4780
实数
的绝对值
equal
非负实数
和
那个 实数
是
实数
的
instance
和
那个 非负实数
是
实数
的
instance
若且唯若
那个 实数
是
非负实数
的
instance
和
那个 实数
equal
那个 非负实数
或
那个 实数
是
负实数
的
instance
和
那个 非负实数
equal
(0.0 和
那个 实数
)
No TPTP formula. May not be expressible in strict first order.
FinancialOntology.kif 2321-2326
金融账户
是
金融账户
的
instance
和
有认知的主事
possesses
金融资产
和
那个 金融账户
equal
那个 金融资产
的帐号 若且唯若
那个 有认知的主事
持有
account
那个 金融账户
No TPTP formula. May not be expressible in strict first order.
People.kif 357-390
年
是
那个 年
EAR
year
的
instance
和
地缘政治区域
和
那个 年
的
male
出生估计寿命
equal
实数
若且唯若 有存在
串列
,
另一个 整数
,, ,
符号串
,, ,
实体
,, ,
另一个 实体
, and 和
第三 实体
这样
那个 串列
是
串列
的
instance
和
那个 串列
的长度 是
那个 另外 整数
的
instance
和 对所有
那个 串列
ITEM
如果
那个 串列
ITEM 是
那个 串列
的
member
,
然后
那个 串列
ITEM 是
那个 符号串
的
instance
和 不存在
第五 实体
这样
那个 第五 实体
是
那个 符号串
的
instance
和
那个 第五 实体
不 是
那个 串列
的
member
和
那个 另外 整数
equal
那个 符号串
所描述的类别
instance
的数量
和
那个 实数
是
那个 串列
的
average
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 403-436
年
是
整数
year
的
instance
和
地缘政治区域
和
那个 年
的
female
出生预期寿命
equal
实数
若且唯若 有存在
串列
,
另一个 整数
,, ,
符号串
,, ,
实体
,, ,
另一个 实体
, and 和
第三 实体
这样
那个 串列
是
串列
的
instance
和
那个 串列
的长度 是
那个 另外 整数
的
instance
和 对所有
那个 串列
ITEM
如果
那个 串列
ITEM 是
那个 串列
的
member
,
然后
那个 串列
ITEM 是
那个 符号串
的
instance
和 不存在
第五 实体
这样
那个 第五 实体
是
那个 符号串
的
instance
和
那个 第五 实体
不 是
那个 串列
的
member
和
那个 另外 整数
equal
那个 符号串
所描述的类别
instance
的数量
和
那个 实数
是
那个 串列
的
average
No TPTP formula. May not be expressible in strict first order.
People.kif 310-342
年
是
整数
year
的
instance
和
地缘政治区域
和
那个 年
的出生预期
life
equal
实数
若且唯若 有存在
串列
,
另一个 整数
,, ,
符号串
,, ,
实体
,, ,
另一个 实体
, and 和
第三 实体
这样
那个 串列
是
串列
的
instance
和
那个 串列
的长度 是
那个 另外 整数
的
instance
和 对所有
那个 串列
ITEM
如果
那个 串列
ITEM 是
那个 串列
的
member
,
然后
那个 串列
ITEM 是
那个 符号串
的
instance
和 不存在
第五 实体
这样
那个 第五 实体
是
那个 符号串
的
instance
和
那个 第五 实体
不 是
那个 串列
的
member
和
那个 另外 整数
equal
那个 符号串
所描述的类别
instance
的数量
和
那个 实数
是
那个 串列
的
average
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 206-223
地缘政治区域
的
male
对母性比率
equal
实数
若且唯若
整数
equal
符号串
所描述的类别
instance
的数量 和
另一个 整数
equal
另一个 符号串
所描述的类别
instance
的数量 和
那个 整数
和
那个 另外 整数
equal
那个 实数
No TPTP formula. May not be expressible in strict first order.
Weather.kif 1492-1497
实数
equal
标准偏差
串列
若且唯若
那个 实数
equal
方差函数
那个 串列
平方根
No TPTP formula. May not be expressible in strict first order.
Weather.kif 1685-1691
函数量
equal
实数
英里每小時
若且唯若
那个 函数量
equal
那个 实数
英里
除以 1
小时
No TPTP formula. May not be expressible in strict first order.
FinancialOntology.kif 3034-3042
有存在
金融工具
,
那个 金融工具
Price, and 和
另一个 货币测量
这样
协议
是
选项
的
instance
和
那个 金融工具
是
那个 协议
的
underlier
和
那个 金融工具
是 对于
施事体
的
price
那个 金融工具
Price 和
那个 另外 货币测量
是
那个 协议
的
strike
价钱 和
那个 金融工具
Price
equal
那个 另外 货币测量
若且唯若
那个 施事体
是
那个 协议
at
的钱
No TPTP formula. May not be expressible in strict first order.
Mid-level-ontology.kif 14106-14116
如果
有认知的主事
有义务去做在
协议
的
命题
道义属性
和
那个 道义属性
equal
义务
或
那个 道义属性
equal
诺言
,
然后 有存在
实体
这样
那个 实体
表示
那个 命题
的内容 和
那个 有认知的主事
是
那个 实体
的
agent
的声明 has
容易
的语气
No TPTP formula. May not be expressible in strict first order.
Geography.kif 2080-2090
如果
实数
测量单位
是
地理区域
的
arable
土地 和
那个 实数
是
greaterThanOrEqualTo
0.0 和
另一个 实数
那个 测量单位
是
那个 地理区域
的
total
區域 和
那个 另外 实数
是
面积测量
的
instance
和
第三 实数
equal
那个 实数
和
那个 另外 实数
,
然后
那个 第三 实数
那个 测量单位
是
那个 地理区域
的
arable
土地
No TPTP formula. May not be expressible in strict first order.
Medicine.kif 172-187
如果
Anemia
是
客体
的
attribute
和
另一个 客体
是
血液
的
instance
和
那个 另外 客体
是
那个 客体
的
part
和
女
是
那个 客体
的
attribute
和
那个 另外 客体
的
measure
是 0.1
升
和
那个 客体
E 是
Hemoglobin
的
instance
和
那个 客体
E 是
那个 另外 客体
的
part
和
那个 客体
E2 不 是
Hemoglobin
的
instance
和
那个 客体
E 不
equal
那个 客体
E2 和
那个 客体
2 是
那个 另外 客体
的
part
和
那个 客体
E 的
measure
是
实数
公克
,
然后
那个 实数
是
lessThan
12
No TPTP formula. May not be expressible in strict first order.
Medicine.kif 155-170
如果
Anemia
是
客体
的
attribute
和
另一个 客体
是
血液
的
instance
和
那个 另外 客体
是
那个 客体
的
part
和
男
是
那个 客体
的
attribute
和
那个 另外 客体
的
measure
是 0.1
升
和
那个 客体
E 是
Hemoglobin
的
instance
和
那个 客体
E 是
那个 另外 客体
的
part
和
那个 客体
E2 不 是
Hemoglobin
的
instance
和
那个 客体
E 不
equal
那个 客体
E2 和
那个 客体
2 是
那个 另外 客体
的
part
和
那个 客体
E 的
measure
是
实数
公克
,
然后
那个 实数
是
lessThan
13
No TPTP formula. May not be expressible in strict first order.
ArabicCulture.kif 204-223
如果
穆斯林
是
施事体
的
attribute
和 属于
那个 施事体
的资产值
equal
货币测量
,
然后 有存在
实体
,
另一个 实体
,, ,
第三 实体
,, ,
第四 实体
, and 和
第五 实体
这样
那个 实体
是
天课
的
instance
和
那个 第四 实体
是
年
的
instance
和
那个 第四 实体
在
那个 施事体
出现 的
time
时段内发生 和
完全成型
是
那个 施事体
的
attribute
在
那个 第四 实体
holdsDuring
和
那个 施事体
是
那个 实体
的
agent
和
那个 另外 实体
是
那个 实体
的
patient
和
那个 另外 实体
的价值 是
那个 第五 实体
那个 第三 实体
和
那个 第三 实体
是
UnitOfCurrency
的
instance
和
那个 第五 实体
是
greaterThan
那个 货币测量
和 0.025 的声明 has
义务
的语气
No TPTP formula. May not be expressible in strict first order.
Medicine.kif 3984-4004
如果
ADHD
是
施事体
的
attribute
和
ADHD
不 是
另一个 施事体
的
attribute
和
那个 施事体
不
equal
那个 另外 施事体
和
过程
是
类
的
instance
和
另一个 过程
是
那个 类
的
instance
和
那个 类
是
有意图的心理过程
的
subclass
和
那个 施事体
是
那个 过程
的
agent
和
那个 另外 施事体
是
那个 另外 过程
的
agent
和
那个 过程
出现 的
time
的
duration
是
持续时间
和
那个 另外 过程
出现 的
time
的
duration
是
另一个 持续时间
,
然后
那个 另外 持续时间
是
greaterThan
那个 持续时间
的声明 has
容易
的语气
No TPTP formula. May not be expressible in strict first order.
ComputingBrands.kif 2693-2704
如果
凹
是
自身连接物体
的
attribute
和
那个 自身连接物体
是
另一个 自身连接物体
的
surface
和
客体
是
那个 另外 自身连接物体
的
part
和
另一个 客体
是
那个 另外 自身连接物体
的
part
和
第三 客体
equal
那个 客体
和
那个 另外 客体
之间线路 和
那个 客体
不
equal
那个 另外 客体
和
第四 客体
是
那个 第三 客体
的
part
,
然后
那个 第四 客体
在
那个 自身连接物体
的
外
No TPTP formula. May not be expressible in strict first order.
ComputingBrands.kif 2665-2676
如果
凸
是
自身连接物体
的
attribute
和
那个 自身连接物体
是
另一个 自身连接物体
的
surface
和
客体
是
那个 另外 自身连接物体
的
part
和
另一个 客体
是
那个 另外 自身连接物体
的
part
和
第三 客体
equal
那个 客体
和
那个 另外 客体
之间线路 和
那个 客体
不
equal
那个 另外 客体
和
第四 客体
是
那个 第三 客体
的
part
,
然后
那个 第四 客体
在
那个 自身连接物体
的
内
No TPTP formula. May not be expressible in strict first order.
Mid-level-ontology.kif 4071-4088
如果
几何图
是
客体
的
attribute
和
那个 客体
是
FourPosterBed
的
instance
和
那个 几何图
是
四边形
的
instance
和
那个 几何图
的
side
是
一维图
和
那个 几何图
的
side
是
另一个 一维图
和
那个 一维图
不
equal
那个 另外 一维图
,
然后 有存在
另一个 客体
,
第三 客体
,, ,
几何点
, and 和
第四 客体
这样
那个 另外 客体
是
那个 客体
的
part
和
那个 第三 客体
是
地板
的
instance
和
那个 客体
在
那个 第三 客体
的
上
和
那个 另外 客体
在
那个 第三 客体
的
垂直
和
那个 一维图
是 对于
那个 几何点
的 交接点
那个 另外 一维图
和
那个 几何点
是
那个 第四 客体
的
attribute
和
那个 第四 客体
接上
那个 另外 客体
No TPTP formula. May not be expressible in strict first order.
Merge.kif 8122-8130
如果
时距
的开始%n在
另一个 时距
的开始
before
发生 和
那个 时距
的结束
equal
那个 另外 时距
的结束,
然后
那个 另外 时距
finishes
了才到
那个 时距
No TPTP formula. May not be expressible in strict first order.
Media.kif 2889-2895
如果
符号串
在
ISO-4217-A
denotes
UnitOfCurrency
和
另一个 符号串
在
ISO-3166-1-alpha-2
denotes
地缘政治区域
和
那个 地缘政治区域
是
地缘政治区域
的
instance
和
那个 另外 符号串
equal
那个 符号串
的
sub
-string 从 0 对于 2 ,
然后
那个 UnitOfCurrency
是
那个 地缘政治区域
的
currency
类别
Display limited to 25 items.
Show next 25
Display limited to 25 items.
Show next 25
consequent
No TPTP formula. May not be expressible in strict first order.
Merge.kif 4769-4780
实数
的绝对值
equal
非负实数
和
那个 实数
是
实数
的
instance
和
那个 非负实数
是
实数
的
instance
若且唯若
那个 实数
是
非负实数
的
instance
和
那个 实数
equal
那个 非负实数
或
那个 实数
是
负实数
的
instance
和
那个 非负实数
equal
(0.0 和
那个 实数
)
No TPTP formula. May not be expressible in strict first order.
Mid-level-ontology.kif 26362-26373
过程
是
Photocopying
的
instance
和
内容承载物理
是
那个 过程
的
patient
和
那个 内容承载物理
是
VisualContentBearingObject
的
instance
和
那个 内容承载物理
contains
命题
的资料 若且唯若 有存在
另一个 内容承载物理
和
另一个 命题
这样
那个 另外 内容承载物理
是
那个 过程
的
result
和
那个 另外 内容承载物理
是
VisualContentBearingObject
的
instance
和
那个 另外 内容承载物理
contains
那个 另外 命题
的资料 和
那个 命题
equal
那个 另外 命题
No TPTP formula. May not be expressible in strict first order.
People.kif 357-390
年
是
那个 年
EAR
year
的
instance
和
地缘政治区域
和
那个 年
的
male
出生估计寿命
equal
实数
若且唯若 有存在
串列
,
另一个 整数
,, ,
符号串
,, ,
实体
,, ,
另一个 实体
, and 和
第三 实体
这样
那个 串列
是
串列
的
instance
和
那个 串列
的长度 是
那个 另外 整数
的
instance
和 对所有
那个 串列
ITEM
如果
那个 串列
ITEM 是
那个 串列
的
member
,
然后
那个 串列
ITEM 是
那个 符号串
的
instance
和 不存在
第五 实体
这样
那个 第五 实体
是
那个 符号串
的
instance
和
那个 第五 实体
不 是
那个 串列
的
member
和
那个 另外 整数
equal
那个 符号串
所描述的类别
instance
的数量
和
那个 实数
是
那个 串列
的
average
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 403-436
年
是
整数
year
的
instance
和
地缘政治区域
和
那个 年
的
female
出生预期寿命
equal
实数
若且唯若 有存在
串列
,
另一个 整数
,, ,
符号串
,, ,
实体
,, ,
另一个 实体
, and 和
第三 实体
这样
那个 串列
是
串列
的
instance
和
那个 串列
的长度 是
那个 另外 整数
的
instance
和 对所有
那个 串列
ITEM
如果
那个 串列
ITEM 是
那个 串列
的
member
,
然后
那个 串列
ITEM 是
那个 符号串
的
instance
和 不存在
第五 实体
这样
那个 第五 实体
是
那个 符号串
的
instance
和
那个 第五 实体
不 是
那个 串列
的
member
和
那个 另外 整数
equal
那个 符号串
所描述的类别
instance
的数量
和
那个 实数
是
那个 串列
的
average
No TPTP formula. May not be expressible in strict first order.
People.kif 310-342
年
是
整数
year
的
instance
和
地缘政治区域
和
那个 年
的出生预期
life
equal
实数
若且唯若 有存在
串列
,
另一个 整数
,, ,
符号串
,, ,
实体
,, ,
另一个 实体
, and 和
第三 实体
这样
那个 串列
是
串列
的
instance
和
那个 串列
的长度 是
那个 另外 整数
的
instance
和 对所有
那个 串列
ITEM
如果
那个 串列
ITEM 是
那个 串列
的
member
,
然后
那个 串列
ITEM 是
那个 符号串
的
instance
和 不存在
第五 实体
这样
那个 第五 实体
是
那个 符号串
的
instance
和
那个 第五 实体
不 是
那个 串列
的
member
和
那个 另外 整数
equal
那个 符号串
所描述的类别
instance
的数量
和
那个 实数
是
那个 串列
的
average
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.
Mid-level-ontology.kif 744-755
和弦音乐
是
客体
的
attribute
若且唯若 有存在
过程
和
另一个 过程
这样
那个 客体
是
制作音乐
的
instance
和
那个 过程
是
制作音乐
的
instance
和
那个 另外 过程
是
制作音乐
的
instance
和
那个 过程
%n是
那个 客体
的
subProcess
和
那个 另外 过程
%n是
那个 客体
的
subProcess
和
那个 过程
不
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 1911-1916
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.
Weather.kif 1492-1497
实数
equal
标准偏差
串列
若且唯若
那个 实数
equal
方差函数
那个 串列
平方根
No TPTP formula. May not be expressible in strict first order.
Weather.kif 1685-1691
函数量
equal
实数
英里每小時
若且唯若
那个 函数量
equal
那个 实数
英里
除以 1
小时
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.
Merge.kif 1885-1889
实数
是
greaterThanOrEqualTo
另一个 实数
若且唯若
那个 实数
equal
那个 另外 实数
或
那个 实数
是
greaterThan
那个 另外 实数
No TPTP formula. May not be expressible in strict first order.
Mid-level-ontology.kif 30247-30260
Alone
是
实体
的
attribute
在
时距
holdsDuring
若且唯若 不存在
那个 实体
2 和
过程
这样
那个 实体
不
equal
那个 实体
2 和
那个 实体
2 是
施事体
的
instance
和
那个 过程
是
社交
的
instance
和
那个 过程
出现 的
time
在
那个 时距
时段内发生 和
那个 实体
是事件
那个 过程
的
involved
和
那个 实体
2 是事件
那个 过程
的
involved
No TPTP formula. May not be expressible in strict first order.
Geography.kif 3504-3513
实体
是
大陆
的
instance
若且唯若
非洲
equal
那个 实体
或
北美
equal
那个 实体
或
南美洲
equal
那个 实体
或
南极洲
equal
那个 实体
或
欧洲
equal
那个 实体
或
亚洲
equal
那个 实体
或
大洋洲
equal
那个 实体
No TPTP formula. May not be expressible in strict first order.
Mid-level-ontology.kif 6472-6482
实体
是
共轭物质
的
instance
若且唯若 有存在
客体
,
另一个 客体
, and 和
过程
这样
那个 客体
是
复合物质
的
instance
和
那个 另外 客体
是
复合物质
的
instance
和
那个 客体
不
equal
那个 另外 客体
和
那个 过程
是
化学合成
的
instance
和
那个 客体
是
那个 过程
的
resource
和
那个 另外 客体
是
那个 过程
的
resource
和
那个 实体
是
那个 过程
的
result
No TPTP formula. May not be expressible in strict first order.
Geography.kif 3488-3494
实体
是
半球
的
instance
若且唯若
那个 实体
equal
北半球
或
那个 实体
equal
南半球
或
那个 实体
equal
东半球
或
那个 实体
equal
西半球
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.
Merge.kif 1867-1871
实数
是
lessThanOrEqualTo
另一个 实数
若且唯若
那个 实数
equal
那个 另外 实数
或
那个 实数
是
lessThan
那个 另外 实数
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.
People.kif 456-469
年
是
整数
year
的
instance
和
地缘政治区域
和
那个 年
每个女人生的
children
equal
符号串
所描述的类别
instance
的数量
No TPTP formula. May not be expressible in strict first order.
Military.kif 924-937
地缘政治区域
和
年
每年的
reaching
军事男性年龄
equal
符号串
所描述的类别
instance
的数量
No TPTP formula. May not be expressible in strict first order.
Mid-level-ontology.kif 13360-13363
对所有
实数
那个 实数
OunceMass
equal
那个 实数
和 16.0
磅质量
No TPTP formula. May not be expressible in strict first order.
Merge.kif 4737-4738
对所有
整数
(
那个 整数
+2)
equal
(
那个 整数
和 1)
No TPTP formula. May not be expressible in strict first order.
Merge.kif 4721-4722
对所有
整数
(
那个 整数
+1)
equal
(
那个 整数
和 1)
No TPTP formula. May not be expressible in strict first order.
Merge.kif 3038-3041
对所有 @ROW 和
另一个 实体
(@ROW 和
那个 另外 实体
) 的长度
equal
((@ROW) 的长度+1)
No TPTP formula. May not be expressible in strict first order.
Merge.kif 3043-3047
对所有 @ROW 和
另一个 实体
(@ROW 和
那个 另外 实体
) 的第 (@ROW 和
那个 另外 实体
) 的长度 几个元素
equal
那个 另外 实体
No TPTP formula. May not be expressible in strict first order.
Government.kif 2879-2879
大六
不
equal
6人组
appearance as argument number 0
No TPTP formula. May not be expressible in strict first order.
Merge.kif 5266-5266
ArcCosineFn
实数
的馀弦
equal
那个 实数
No TPTP formula. May not be expressible in strict first order.
Merge.kif 5276-5276
ArcSineFn
实数
的正弦
equal
那个 实数
No TPTP formula. May not be expressible in strict first order.
Merge.kif 5256-5256
ArcTangentFn
实数
的正切
equal
那个 实数
No TPTP formula. May not be expressible in strict first order.
Military.kif 863-872
地缘政治区域
的
available
军事服务男性
equal
符号串
所描述的类别
instance
的数量
No TPTP formula. May not be expressible in strict first order.
Mid-level-ontology.kif 4888-4891
符号串
所描述的类别
instance
的数量
equal
3
No TPTP formula. May not be expressible in strict first order.
Merge.kif 14228-14228
大陆
instance
的数量
equal
7
No TPTP formula. May not be expressible in strict first order.
Media.kif 2003-2003
NativityMagi
instance
的数量
equal
3
No TPTP formula. May not be expressible in strict first order.
Military.kif 886-897
地缘政治区域
的
fit
对于军服务男性
equal
符号串
所描述的类别
instance
的数量
No TPTP formula. May not be expressible in strict first order.
Economy.kif 2008-2008
1
千瓦时
equal
3.6
焦耳
的一百万倍
No TPTP formula. May not be expressible in strict first order.
Economy.kif 2009-2009
1
千瓦时
equal
3600000.0
焦耳
No TPTP formula. May not be expressible in strict first order.
Merge.kif 7113-7115
1
周持续时间
equal
7
一天长度
No TPTP formula. May not be expressible in strict first order.
Merge.kif 7140-7142
1
年持续时间
equal
365
一天长度
No TPTP formula. May not be expressible in strict first order.
Geography.kif 382-382
1.0
圆周角度
equal
60.0
弧分
No TPTP formula. May not be expressible in strict first order.
Geography.kif 401-401
1.0
弧分
equal
60.0
弧秒
No TPTP formula. May not be expressible in strict first order.
Geography.kif 3842-3842
1.0
推测
equal
6.0
脚长
No TPTP formula. May not be expressible in strict first order.
Mid-level-ontology.kif 13628-13630
1.0
公吨
equal
2205.0
磅质量
No TPTP formula. May not be expressible in strict first order.
Geography.kif 3865-3867
1.0
海里
equal
1852.0
仪表
No TPTP formula. May not be expressible in strict first order.
Geography.kif 3861-3863
1.0
海里
equal
6076.1
脚长
No TPTP formula. May not be expressible in strict first order.
Mid-level-ontology.kif 13723-13727
1.0
平方英里
equal
1.0
英里
是 1.0
英里
的
per
No TPTP formula. May not be expressible in strict first order.
Mid-level-ontology.kif 13733-13737
1.0
方码
equal
1.0
院子长度
是 1.0
院子长度
的
per
No TPTP formula. May not be expressible in strict first order.
Geography.kif 402-402
实数
弧分
equal
60.0 和
那个 实数
弧秒
No TPTP formula. May not be expressible in strict first order.
Geography.kif 383-383
实数
圆周角度
equal
60.0 和
那个 实数
弧分
No TPTP formula. May not be expressible in strict first order.
Merge.kif 7152-7154
实数
amu
equal
那个 实数
和 1.6605402E-24
公克
No TPTP formula. May not be expressible in strict first order.
Merge.kif 7174-7176
实数
埃
equal
那个 实数
和 1.0E-10
仪表
No TPTP formula. May not be expressible in strict first order.
Merge.kif 7368-7370
实数
圆周角度
equal
那个 实数
和
圆周率
和 180.0
弧度
Display limited to 25 items.
Show next 25
Display limited to 25 items.
Show next 25
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