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 4768-4779
实数
的绝对值
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 1508-1513
实数
equal
标准偏差
串列
若且唯若
那个 实数
equal
方差函数
那个 串列
平方根
No TPTP formula. May not be expressible in strict first order.
Weather.kif 1702-1708
函数量
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 14079-14089
如果
有认知的主事
有义务去做在
协议
的
命题
道义属性
和
那个 道义属性
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 4078-4095
如果
几何图
是
客体
的
attribute
和
那个 客体
是
FourPosterBed
的
instance
和
那个 几何图
是
四边形
的
instance
和
那个 几何图
的
side
是
一维图
和
那个 几何图
的
side
是
另一个 一维图
和
那个 一维图
不
equal
那个 另外 一维图
,
然后 有存在
另一个 客体
,
第三 客体
,, ,
几何点
, and 和
第四 客体
这样
那个 另外 客体
是
那个 客体
的
part
和
那个 第三 客体
是
地板
的
instance
和
那个 客体
在
那个 第三 客体
的
上
和
那个 另外 客体
在
那个 第三 客体
的
垂直
和
那个 一维图
是 对于
那个 几何点
的 交接点
那个 另外 一维图
和
那个 几何点
是
那个 第四 客体
的
attribute
和
那个 第四 客体
接上
那个 另外 客体
No TPTP formula. May not be expressible in strict first order.
Merge.kif 8086-8094
如果
时距
的开始%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 4768-4779
实数
的绝对值
equal
非负实数
和
那个 实数
是
实数
的
instance
和
那个 非负实数
是
实数
的
instance
若且唯若
那个 实数
是
非负实数
的
instance
和
那个 实数
equal
那个 非负实数
或
那个 实数
是
负实数
的
instance
和
那个 非负实数
equal
(0.0 和
那个 实数
)
No TPTP formula. May not be expressible in strict first order.
Mid-level-ontology.kif 26329-26340
过程
是
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 751-762
和弦音乐
是
客体
的
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 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.
Weather.kif 1508-1513
实数
equal
标准偏差
串列
若且唯若
那个 实数
equal
方差函数
那个 串列
平方根
No TPTP formula. May not be expressible in strict first order.
Weather.kif 1702-1708
函数量
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 30223-30236
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 6478-6488
实体
是
共轭物质
的
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 933-946
地缘政治区域
和
年
每年的
reaching
军事男性年龄
equal
符号串
所描述的类别
instance
的数量
No TPTP formula. May not be expressible in strict first order.
Mid-level-ontology.kif 13333-13336
对所有
实数
那个 实数
OunceMass
equal
那个 实数
和 16.0
磅质量
No TPTP formula. May not be expressible in strict first order.
Merge.kif 4736-4737
对所有
整数
(
那个 整数
+2)
equal
(
那个 整数
和 1)
No TPTP formula. May not be expressible in strict first order.
Merge.kif 4720-4721
对所有
整数
(
那个 整数
+1)
equal
(
那个 整数
和 1)
No TPTP formula. May not be expressible in strict first order.
Merge.kif 3037-3040
对所有 @ROW 和
另一个 实体
(@ROW 和
那个 另外 实体
) 的长度
equal
((@ROW) 的长度+1)
No TPTP formula. May not be expressible in strict first order.
Merge.kif 3042-3046
对所有 @ROW 和
另一个 实体
(@ROW 和
那个 另外 实体
) 的第 (@ROW 和
那个 另外 实体
) 的长度 几个元素
equal
那个 另外 实体
No TPTP formula. May not be expressible in strict first order.
Government.kif 2915-2915
大六
不
equal
6人组
appearance as argument number 0
No TPTP formula. May not be expressible in strict first order.
Merge.kif 5265-5265
ArcCosineFn
实数
的馀弦
equal
那个 实数
No TPTP formula. May not be expressible in strict first order.
Merge.kif 5275-5275
ArcSineFn
实数
的正弦
equal
那个 实数
No TPTP formula. May not be expressible in strict first order.
Merge.kif 5255-5255
ArcTangentFn
实数
的正切
equal
那个 实数
No TPTP formula. May not be expressible in strict first order.
Military.kif 872-881
地缘政治区域
的
available
军事服务男性
equal
符号串
所描述的类别
instance
的数量
No TPTP formula. May not be expressible in strict first order.
Merge.kif 14182-14182
大陆
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 895-906
地缘政治区域
的
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 7112-7114
1
周持续时间
equal
7
一天长度
No TPTP formula. May not be expressible in strict first order.
Merge.kif 7139-7141
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 13601-13603
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 13696-13700
1.0
平方英里
equal
1.0
英里
是 1.0
英里
的
per
No TPTP formula. May not be expressible in strict first order.
Mid-level-ontology.kif 13706-13710
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 7151-7153
实数
amu
equal
那个 实数
和 1.6605402E-24
公克
No TPTP formula. May not be expressible in strict first order.
Merge.kif 7173-7175
实数
埃
equal
那个 实数
和 1.0E-10
仪表
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 7353-7355
实数
英国热量单位
equal
那个 实数
和 1055.05585262
焦耳
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