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
instance
Sigma KEE - instance
instance
appearance as argument number 1
No TPTP formula. May not be expressible in strict first order.
chinese_format.kif 1359-1361
No TPTP formula. May not be expressible in strict first order.
Merge.kif 84-87
No TPTP formula. May not be expressible in strict first order.
japanese_format.kif 17-20
No TPTP formula. May not be expressible in strict first order.
spanish_format.kif 17-20
No TPTP formula. May not be expressible in strict first order.
Merge.kif 81-81
实例
的 1 数量 是
实体
的
instance
No TPTP formula. May not be expressible in strict first order.
Merge.kif 82-82
实例
的 2 数量 是
类
的
instance
No TPTP formula. May not be expressible in strict first order.
Merge.kif 80-80
实例
是
二元谓语
的
instance
appearance as argument number 2
No TPTP formula. May not be expressible in strict first order.
chinese_format.kif 305-305
No TPTP formula. May not be expressible in strict first order.
english_format.kif 310-310
No TPTP formula. May not be expressible in strict first order.
french_format.kif 175-175
No TPTP formula. May not be expressible in strict first order.
relations-it.txt 149-149
No TPTP formula. May not be expressible in strict first order.
japanese_format.kif 1995-1995
No TPTP formula. May not be expressible in strict first order.
portuguese_format.kif 127-127
No TPTP formula. May not be expressible in strict first order.
relations-cz.txt 173-173
No TPTP formula. May not be expressible in strict first order.
relations-de.txt 400-400
No TPTP formula. May not be expressible in strict first order.
relations-hindi.txt 188-188
No TPTP formula. May not be expressible in strict first order.
relations-ro.kif 195-195
No TPTP formula. May not be expressible in strict first order.
relations-sv.txt 184-184
No TPTP formula. May not be expressible in strict first order.
relations-tg.txt 302-302
No TPTP formula. May not be expressible in strict first order.
Merge.kif 1281-1281
组员
和
实例
是 内部相关
No TPTP formula. May not be expressible in strict first order.
Merge.kif 5413-5413
元素
是
实例
的
subrelation
No TPTP formula. May not be expressible in strict first order.
Merge.kif 89-89
直接实例
是
实例
的
subrelation
No TPTP formula. May not be expressible in strict first order.
domainEnglishFormat.kif 30253-30253
No TPTP formula. May not be expressible in strict first order.
chinese_format.kif 306-306
No TPTP formula. May not be expressible in strict first order.
domainEnglishFormat.kif 30252-30252
No TPTP formula. May not be expressible in strict first order.
domainEnglishFormat.kif 30251-30251
No TPTP formula. May not be expressible in strict first order.
relations-tg.txt 303-303
antecedent
No TPTP formula. May not be expressible in strict first order.
FinancialOntology.kif 1018-1022
有认知的主事
持有
account
金融账户
和
那个 有认知的主事
是
法人财团
的
instance
若且唯若
那个 金融账户
是
企业帐户
的
instance
No TPTP formula. May not be expressible in strict first order.
FinancialOntology.kif 996-1000
有认知的主事
持有
account
金融账户
和
那个 有认知的主事
是
人类
的
instance
若且唯若
那个 金融账户
是
个人账户
的
instance
No TPTP formula. May not be expressible in strict first order.
MilitaryDevices.kif 1462-1467
飞机
的
altitude
是
自身连接物体
和
那个 自身连接物体
是
行星地球
的
surface
和
那个 飞机
是
飞机
的
instance
若且唯若
高度测量
是
absolute
那个 飞机
的高度
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 2335-2340
金融账户
是
金融账户
的
instance
和
有认知的主事
possesses
金融资产
和
那个 金融账户
equal
那个 金融资产
的帐号 若且唯若
那个 有认知的主事
持有
account
那个 金融账户
No TPTP formula. May not be expressible in strict first order.
FinancialOntology.kif 1007-1011
实体
是
个人账户
的
instance
和
符号串
所描述的类别
instance
的数量 是
greaterThan
1 若且唯若
那个 实体
是
联名账户
的
instance
No TPTP formula. May not be expressible in strict first order.
Mid-level-ontology.kif 30079-30089
实体
是
身体部位
的
instance
和
Bare
是
那个 实体
的
attribute
在
时间位置
holdsDuring
若且唯若 不存在
另一个 实体
这样
那个 另外 实体
是
服装
的
instance
和
covers
那个 另外 实体
and
那个 实体
在
那个 时间位置
holdsDuring
No TPTP formula. May not be expressible in strict first order.
Merge.kif 12436-12443
过程
是
结合
的
instance
和
客体
是
那个 过程
的
resource
和
实体
是
那个 过程
的
result
若且唯若
那个 客体
不 是
那个 实体
的
part
在
那个 过程
出现 的
time
的开始
holdsDuring
和
那个 客体
是
那个 实体
的
part
在
那个 过程
出现 的
time
的结束
holdsDuring
No TPTP formula. May not be expressible in strict first order.
Mid-level-ontology.kif 26245-26256
过程
是
Photocopying
的
instance
和
内容承载物理
是
那个 过程
的
patient
和
那个 内容承载物理
是
VisualContentBearingObject
的
instance
和
那个 内容承载物理
contains
命题
的资料 若且唯若 有存在
另一个 内容承载物理
和
另一个 命题
这样
那个 另外 内容承载物理
是
那个 过程
的
result
和
那个 另外 内容承载物理
是
VisualContentBearingObject
的
instance
和
那个 另外 内容承载物理
contains
那个 另外 命题
的资料 和
那个 命题
equal
那个 另外 命题
No TPTP formula. May not be expressible in strict first order.
Geography.kif 7502-7508
自身连接物体
是
液体滴
的
instance
和 1 的
approximate
diameter
是 %2 和 500.0 是
lessThan
实数
若且唯若
那个 自身连接物体
是
小滴液体
的
instance
No TPTP formula. May not be expressible in strict first order.
Geography.kif 7418-7429
客体
是
悬浮颗粒
的
instance
和
自身连接物体
是
那个 客体
的
part
和 1 的
approximate
diameter
是 %2 和 10.0 是
greaterThan
实数
和
那个 实数
是
greaterThan
2.5 若且唯若 有存在
那个 客体
10 这样
那个 客体
10 是
粗悬浮颗粒
的
instance
和
那个 客体
10 是
那个 客体
的
part
No TPTP formula. May not be expressible in strict first order.
Geography.kif 7447-7457
客体
是
悬浮颗粒
的
instance
和
自身连接物体
是
那个 客体
的
part
和 1 的
approximate
diameter
是 %2 和
实数
是
greaterThanOrEqualTo
2.5 若且唯若 有存在
那个 客体
25 这样
那个 客体
25 是
细悬浮颗粒
的
instance
和
那个 客体
25 是
那个 客体
的
part
No TPTP formula. May not be expressible in strict first order.
ComputerInput.kif 1789-1793
实体
是
WindowScrolling
的
instance
和
那个 实体
是
UserSignifiedGraphicalAction
的
instance
若且唯若
那个 实体
是
WindowScrollingByUser
的
instance
No TPTP formula. May not be expressible in strict first order.
FinancialOntology.kif 1832-1842
过程
是
退出
的
instance
和
金融账户
是
金融账户
的
instance
和
那个 金融账户
的
currency
是
那个 过程
的源头 和 不存在
另一个 过程
这样
那个 另外 过程
是
罚款
的
instance
和
那个 另外 过程
在
那个 金融账户
的
currency
结束 和
那个 过程
causes
那个 另外 过程
若且唯若
那个 金融账户
的
liqudity
是
高流动性
No TPTP formula. May not be expressible in strict first order.
Weather.kif 2680-2690
实体
是
地区
的
instance
和
那个 实体
有
标准状况
的
attribute
在
时间位置
holdsDuring
若且唯若 298.15
凯文度
是
那个 实体
的
air
温度 和 29.530
英寸汞
是
那个 实体
的
barometric
压力 在
那个 时间位置
holdsDuring
No TPTP formula. May not be expressible in strict first order.
People.kif 383-416
年
是
那个 年
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 108-123
年
是
整数
year
的
instance
和
地缘政治区域
和
那个 年
每一千的
births
equal
实数
若且唯若
那个 地缘政治区域
的
population
和 1000
equal
另一个 实数
和
另一个 整数
equal
符号串
所描述的类别
instance
的数量 和
那个 另外 整数
和
那个 另外 实数
equal
那个 实数
No TPTP formula. May not be expressible in strict first order.
People.kif 144-159
年
是
整数
year
的
instance
和
地缘政治区域
和
那个 年
每一千里的
deaths
equal
实数
若且唯若
那个 地缘政治区域
的
population
和 1000
equal
另一个 实数
和
另一个 整数
equal
符号串
所描述的类别
instance
的数量 和
那个 另外 整数
和
那个 另外 实数
equal
那个 实数
No TPTP formula. May not be expressible in strict first order.
People.kif 264-290
年
是
整数
year
的
instance
和
地缘政治区域
和
那个 年
每一千个生存出生里的
deaths
equal
实数
若且唯若
另一个 整数
equal
符号串
所描述的类别
instance
的数量 和
那个 另外 整数
和 1000
equal
另一个 实数
和
第三 整数
equal
另一个 符号串
所描述的类别
instance
的数量 和
那个 第三 整数
和
那个 另外 实数
equal
那个 实数
No TPTP formula. May not be expressible in strict first order.
People.kif 429-462
年
是
整数
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 336-368
年
是
整数
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 182-213
年
是
整数
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 78-90
年
是
整数
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 24723-24728
PostalPlace
是
located
在
PostcodeArea
和
那个 PostalPlace
是
PostalPlace
的
instance
和
那个 PostcodeArea
是
PostcodeArea
的
instance
若且唯若
那个 PostalPlace
是在
post
code
那个 PostcodeArea
No TPTP formula. May not be expressible in strict first order.
Mid-level-ontology.kif 24696-24701
PostalPlace
是
located
在
城市
和
那个 PostalPlace
是
PostalPlace
的
instance
和
那个 城市
是
城市
的
instance
若且唯若
那个 PostalPlace
是在
那个 城市
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.
FinancialOntology.kif 1018-1022
有认知的主事
持有
account
金融账户
和
那个 有认知的主事
是
法人财团
的
instance
若且唯若
那个 金融账户
是
企业帐户
的
instance
No TPTP formula. May not be expressible in strict first order.
FinancialOntology.kif 996-1000
有认知的主事
持有
account
金融账户
和
那个 有认知的主事
是
人类
的
instance
若且唯若
那个 金融账户
是
个人账户
的
instance
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 1007-1011
实体
是
个人账户
的
instance
和
符号串
所描述的类别
instance
的数量 是
greaterThan
1 若且唯若
那个 实体
是
联名账户
的
instance
No TPTP formula. May not be expressible in strict first order.
Mid-level-ontology.kif 30079-30089
实体
是
身体部位
的
instance
和
Bare
是
那个 实体
的
attribute
在
时间位置
holdsDuring
若且唯若 不存在
另一个 实体
这样
那个 另外 实体
是
服装
的
instance
和
covers
那个 另外 实体
and
那个 实体
在
那个 时间位置
holdsDuring
No TPTP formula. May not be expressible in strict first order.
Mid-level-ontology.kif 26245-26256
过程
是
Photocopying
的
instance
和
内容承载物理
是
那个 过程
的
patient
和
那个 内容承载物理
是
VisualContentBearingObject
的
instance
和
那个 内容承载物理
contains
命题
的资料 若且唯若 有存在
另一个 内容承载物理
和
另一个 命题
这样
那个 另外 内容承载物理
是
那个 过程
的
result
和
那个 另外 内容承载物理
是
VisualContentBearingObject
的
instance
和
那个 另外 内容承载物理
contains
那个 另外 命题
的资料 和
那个 命题
equal
那个 另外 命题
No TPTP formula. May not be expressible in strict first order.
Geography.kif 7502-7508
自身连接物体
是
液体滴
的
instance
和 1 的
approximate
diameter
是 %2 和 500.0 是
lessThan
实数
若且唯若
那个 自身连接物体
是
小滴液体
的
instance
No TPTP formula. May not be expressible in strict first order.
Geography.kif 7418-7429
客体
是
悬浮颗粒
的
instance
和
自身连接物体
是
那个 客体
的
part
和 1 的
approximate
diameter
是 %2 和 10.0 是
greaterThan
实数
和
那个 实数
是
greaterThan
2.5 若且唯若 有存在
那个 客体
10 这样
那个 客体
10 是
粗悬浮颗粒
的
instance
和
那个 客体
10 是
那个 客体
的
part
No TPTP formula. May not be expressible in strict first order.
Geography.kif 7447-7457
客体
是
悬浮颗粒
的
instance
和
自身连接物体
是
那个 客体
的
part
和 1 的
approximate
diameter
是 %2 和
实数
是
greaterThanOrEqualTo
2.5 若且唯若 有存在
那个 客体
25 这样
那个 客体
25 是
细悬浮颗粒
的
instance
和
那个 客体
25 是
那个 客体
的
part
No TPTP formula. May not be expressible in strict first order.
ComputerInput.kif 1789-1793
实体
是
WindowScrolling
的
instance
和
那个 实体
是
UserSignifiedGraphicalAction
的
instance
若且唯若
那个 实体
是
WindowScrollingByUser
的
instance
No TPTP formula. May not be expressible in strict first order.
People.kif 383-416
年
是
那个 年
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 108-123
年
是
整数
year
的
instance
和
地缘政治区域
和
那个 年
每一千的
births
equal
实数
若且唯若
那个 地缘政治区域
的
population
和 1000
equal
另一个 实数
和
另一个 整数
equal
符号串
所描述的类别
instance
的数量 和
那个 另外 整数
和
那个 另外 实数
equal
那个 实数
No TPTP formula. May not be expressible in strict first order.
People.kif 144-159
年
是
整数
year
的
instance
和
地缘政治区域
和
那个 年
每一千里的
deaths
equal
实数
若且唯若
那个 地缘政治区域
的
population
和 1000
equal
另一个 实数
和
另一个 整数
equal
符号串
所描述的类别
instance
的数量 和
那个 另外 整数
和
那个 另外 实数
equal
那个 实数
No TPTP formula. May not be expressible in strict first order.
People.kif 264-290
年
是
整数
year
的
instance
和
地缘政治区域
和
那个 年
每一千个生存出生里的
deaths
equal
实数
若且唯若
另一个 整数
equal
符号串
所描述的类别
instance
的数量 和
那个 另外 整数
和 1000
equal
另一个 实数
和
第三 整数
equal
另一个 符号串
所描述的类别
instance
的数量 和
那个 第三 整数
和
那个 另外 实数
equal
那个 实数
No TPTP formula. May not be expressible in strict first order.
People.kif 429-462
年
是
整数
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 336-368
年
是
整数
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 182-213
年
是
整数
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 78-90
年
是
整数
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.
Economy.kif 1533-1538
1 对于 %3 在周期 %2 的
annual
地区消费 若且唯若 有存在
时间位置
这样
那个 时间位置
是
有点 时距
的
instance
和
货币测量
是
地缘政治区域
在
annual
地区消费 在
那个 时间位置
holdsDuring
No TPTP formula. May not be expressible in strict first order.
Economy.kif 1504-1509
地缘政治区域
annual
对于
有点 时距
在周期
货币测量
的地区收入 若且唯若 有存在
时间位置
这样
那个 时间位置
是
有点 时距
的
instance
和
那个 货币测量
是
那个 地缘政治区域
的
annual
地区收入 在
那个 时间位置
holdsDuring
No TPTP formula. May not be expressible in strict first order.
Mid-level-ontology.kif 723-734
和弦音乐
是
客体
的
attribute
若且唯若 有存在
过程
和
另一个 过程
这样
那个 客体
是
制作音乐
的
instance
和
那个 过程
是
制作音乐
的
instance
和
那个 另外 过程
是
制作音乐
的
instance
和
那个 过程
%n是
那个 客体
的
subProcess
和
那个 另外 过程
%n是
那个 客体
的
subProcess
和
那个 过程
不
equal
那个 另外 过程
和
那个 过程
和
那个 客体
同时发生 和
那个 另外 过程
和
那个 客体
同时发生
No TPTP formula. May not be expressible in strict first order.
Geography.kif 4689-4698
公海
是
客体
的
attribute
若且唯若 有存在
物理
和
实数
这样
那个 客体
是
盐水区
的
instance
和
那个 客体
不 是
内陆水域
的
instance
和
那个 物理
和
那个 客体
的
distance
是
那个 实数
海里
和
那个 实数
是
greaterThan
5.0
No TPTP formula. May not be expressible in strict first order.
FinancialOntology.kif 3956-3961
银行 - 财政组织
是
有点 金融账户
的
bank
帐号 若且唯若 有存在
另一个 金融账户
这样
那个 另外 金融账户
是
有点 金融账户
的
instance
和
那个 另外 金融账户
是被
那个 银行 - 财政组织
held
No TPTP formula. May not be expressible in strict first order.
Economy.kif 1581-1586
地缘政治区域
在周期
货币测量
对于
有点 时距
的
capital
地区支出 若且唯若 有存在
时间位置
这样
那个 时间位置
是
有点 时距
的
instance
和
那个 货币测量
是
那个 地缘政治区域
的
capital
地区支出 在
那个 时间位置
holdsDuring
No TPTP formula. May not be expressible in strict first order.
Economy.kif 3677-3682
有点 时距
是
货币测量
的
currency
交换 每美元 若且唯若 有存在
时间位置
这样
那个 时间位置
是
有点 时距
的
instance
和
那个 货币测量
是
美国美元
的
currency
交换汇率 在
那个 时间位置
holdsDuring
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.
Geography.kif 3193-3193
?D 是 23
Day
的
instance
是
南极条约
的
agreement
生效日期
No TPTP formula. May not be expressible in strict first order.
People.kif 482-495
年
是
整数
year
的
instance
和
地缘政治区域
和
那个 年
每个女人生的
children
equal
符号串
所描述的类别
instance
的数量
No TPTP formula. May not be expressible in strict first order.
Government.kif 1241-1248
对所有 ?AGENT, ?VOTER,, , ?ELECTION, and 和 ?VOTING
如果 ?ELECTION 是 ?AGENT 的
election
的
instance
和 ?VOTING 是 ?ELECTION 的
voting
的
instance
和 ?VOTER 是 ?VOTING 的
agent
,
然后
男
是 ?VOTER 的
attribute
contains
独家男性选举权
的资料
No TPTP formula. May not be expressible in strict first order.
Government.kif 923-931
对所有 ?COUNTRY, ?ELECTION,, , ?VOTING, and 和 ?VOTER
如果 ?COUNTRY 是
国家
的
instance
和 ?ELECTION 是 ?COUNTRY 的
election
的
instance
和 ?VOTING 是 ?ELECTION 的
voting
的
instance
和 ?VOTER 是 ?VOTING 的
agent
,
然后 ?VOTER 是 ?COUNTRY 的
citizen
contains
选民公民身份要求
的资料
No TPTP formula. May not be expressible in strict first order.
Government.kif 1092-1103
对所有 ?POLITY, ?AGENT,, , ?ELECTION,, , ?VOTINGAGE, and 和 ?AGE
如果 ?AGENT 是 ?POLITY 的
citizen
和 ?VOTINGAGE
年持续时间
是 ?POLITY 的
suffrage
最小年纪 和 ?AGENT 的
age
是 ?AGE
年持续时间
和 ?AGE 是
greaterThanOrEqualTo
?VOTINGAGE 和 ?ELECTION 是 ?POLITY 的
election
的
instance
,
然后 ?AGENT 能够担当
主事
的角色做 ?ELECTION 的
voting
contains
普选法
的资料
No TPTP formula. May not be expressible in strict first order.
Government.kif 1160-1174
对所有 ?POLITY, ?VOTER,, , ?ELECTION,, , ?VOTINGAGE, and 和 ?AGE
如果 ?VOTER 是 ?POLITY 的
citizen
和 ?VOTINGAGE
年持续时间
是 ?POLITY 的
suffrage
最小年纪 和 ?VOTER 的
age
是 ?AGE
年持续时间
和 ?AGE 是
greaterThanOrEqualTo
?VOTINGAGE 和 ?ELECTION 是 ?POLITY 的
election
的
instance
,
然后 有存在 ?VOTING 这样 ?VOTING 是 ?ELECTION 的
voting
的
instance
和 ?VOTER 是 ?VOTING 的
agent
contains
强制选举法
的资料
No TPTP formula. May not be expressible in strict first order.
WMD.kif 921-929
?SYMPTOM 是 ?AGENT 的
biochemical
病毒征兆 和 ?AGENT
biochemical
病毒解毒制剂 ?SUBSTANCE 对于 ?PROCESS 和 ?SAMPLE 是 ?SUBSTANCE 的
instance
和 ?THERAPY 是 ?PROCESS 的
instance
和 ?ORGANISM 经历了 ?THERAPY 和 ?SAMPLE 是 ?THERAPY 的
patient
减少 ?SYMPTOM 是 ?ORGANISM 的
attribute
发生的机率
No TPTP formula. May not be expressible in strict first order.
Mid-level-ontology.kif 18150-18167
有存在 ?X, ?CUT,, , ?PAPER,, , ?CBO, and 和 ?INFO 这样 ?X 是
PaperShredder
的
instance
和 ?CUT 是
切开
的
instance
和 ?X 是导致 ?CUT 的
instrument
和 ?PAPER 是
纸
的
instance
和 ?PAPER 是 ?CUT 的
patient
和 ?CBO 是
located
在 ?PAPER 和 ?CBO 是
VisualContentBearingObject
的
instance
和 ?CBO
contains
?INFO 的资料 减少 有存在 ?READ 这样 ?READ 是
解读
的
instance
和 ?INFO 是 ?READ 的
patient
和 ?CUT 出现 的
time
比?READ 出现 的
time
发生的
earlier
发生的机率
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.
Military.kif 895-906
地缘政治区域
的
fit
对于军服务男性
equal
符号串
所描述的类别
instance
的数量
No TPTP formula. May not be expressible in strict first order.
People.kif 49-54
地缘政治区域
的
population
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.
Medicine.kif 4557-4562
有存在
过程
和
实体
这样
那个 过程
是
传播
的
instance
和
Netflix
是
那个 过程
的
agent
和
那个 实体
是
那个 过程
的
patient
和
那个 实体
是
动态映像
的
instance
No TPTP formula. May not be expressible in strict first order.
Medicine.kif 4564-4567
有存在
过程
这样
那个 过程
是
电影制作
的
instance
和
Netflix
是
那个 过程
的
agent
No TPTP formula. May not be expressible in strict first order.
ComputingBrands.kif 2453-2457
有存在
时间位置
这样
那个 时间位置
是 1976
year
的
instance
和
斯蒂夫·沃兹尼亚克
是
史蒂芬·贾伯斯
的
coworker
在
那个 时间位置
holdsDuring
No TPTP formula. May not be expressible in strict first order.
ComputingBrands.kif 2441-2445
有存在
时间位置
这样
那个 时间位置
是 2002
year
的
instance
和
提姆·库克
是
史蒂芬·贾伯斯
的
coworker
在
那个 时间位置
holdsDuring
No TPTP formula. May not be expressible in strict first order.
Merge.kif 825-826
有存在
实体
这样
那个 实体
是
实体
的
instance
No TPTP formula. May not be expressible in strict first order.
Media.kif 1970-1978
有存在
时距
这样
那个 时距
是
时距
的
instance
和
那个 时距
finishes
了才到
JesusOfNazareth
出现 的
time
和
那个 时距
starts
了才到
TwelveApostles
出现 的
time
和 对所有
实体
如果
那个 实体
是
TwelveApostles
的
member
在
那个 时距
holdsDuring
,
然后
那个 实体
是
JesusOfNazareth
的
friend
在
那个 时距
holdsDuring
No TPTP formula. May not be expressible in strict first order.
ComputingBrands.kif 3307-3313
IBookstore
的 目的 是 有存在 ?D 这样 ?D 是
下載
的
instance
和
iBookstore
是导致 ?D 的
instrument
和 ?T 是
文本
的
instance
和
objectTransferred
?D and ?T
No TPTP formula. May not be expressible in strict first order.
Media.kif 2501-2504
Serbia
是
欧洲国家
的
instance
和
时间位置
是 5
day
的
instance
在
那个 时间位置
之后
holdsDuring
No TPTP formula. May not be expressible in strict first order.
Media.kif 2496-2499
Serbia
是
独立国家
的
instance
和
时间位置
是 5
day
的
instance
在
那个 时间位置
之后
holdsDuring
No TPTP formula. May not be expressible in strict first order.
Media.kif 2506-2509
Serbia
的名 是 "Republic of Serbia" 和
时间位置
是 5
day
的
instance
在
那个 时间位置
之后
holdsDuring
No TPTP formula. May not be expressible in strict first order.
Media.kif 2528-2531
时间位置
是 3
day
的
instance
和
Montenegro
是
欧洲国家
的
instance
在
那个 时间位置
之后
holdsDuring
No TPTP formula. May not be expressible in strict first order.
Media.kif 2523-2526
时间位置
是 3
day
的
instance
和
Montenegro
是
独立国家
的
instance
在
那个 时间位置
之后
holdsDuring
No TPTP formula. May not be expressible in strict first order.
Media.kif 2533-2536
时间位置
是 3
day
的
instance
和
Montenegro
的名 是 "Montenegro" 在
那个 时间位置
之后
holdsDuring
Display limited to 25 items.
Show next 25
Display limited to 25 items.
Show next 25
appearance as argument number 0
No TPTP formula. May not be expressible in strict first order.
VirusProteinAndCellPart.kif 663-663
细胞
和
有点 细胞部分
的
cell
部分 是
有点 细胞部分
的
instance
No TPTP formula. May not be expressible in strict first order.
VirusProteinAndCellPart.kif 652-652
病毒
和
有点 病毒部分
的
viral
部分 是
有点 病毒部分
的
instance
No TPTP formula. May not be expressible in strict first order.
FinancialOntology.kif 2534-2534
AAA评级
是
财务评级
的
instance
No TPTP formula. May not be expressible in strict first order.
UXExperimentalTerms.kif 3426-3426
ABPFn
是
一元函数
的
instance
No TPTP formula. May not be expressible in strict first order.
UXExperimentalTerms.kif 4623-4623
ABTest
是
ExperimentAttribute
的
instance
No TPTP formula. May not be expressible in strict first order.
Languages.kif 5379-5379
一种 pucikwar 语言
是
中央伟大的andamanese语言
的
instance
No TPTP formula. May not be expressible in strict first order.
Government.kif 2874-2874
东盟区域论坛
是
国际组织
的
instance
No TPTP formula. May not be expressible in strict first order.
UXExperimentalTerms.kif 3471-3471
ASPFn
是
一元函数
的
instance
No TPTP formula. May not be expressible in strict first order.
ComputingBrands.kif 2122-2122
ATandTCorp
是
法人财团
的
instance
No TPTP formula. May not be expressible in strict first order.
Media.kif 2560-2560
AalandIslands
是
群岛
的
instance
No TPTP formula. May not be expressible in strict first order.
Media.kif 2561-2561
AalandIslands
是
依赖或特殊主权领域
的
instance
No TPTP formula. May not be expressible in strict first order.
Languages.kif 3771-3771
Aariya语言
是
非语言口语
的
instance
No TPTP formula. May not be expressible in strict first order.
Medicine.kif 2964-2964
AbbVie
是
法人财团
的
instance
No TPTP formula. May not be expressible in strict first order.
People.kif 1235-1235
方丈
是
宗教立场
的
instance
No TPTP formula. May not be expressible in strict first order.
Medicine.kif 3849-3849
AbbottLaboratories
是
法人财团
的
instance
No TPTP formula. May not be expressible in strict first order.
Languages.kif 2923-2923
Abinomn语言
是
口语人类语言
的
instance
No TPTP formula. May not be expressible in strict first order.
Languages.kif 3777-3777
Abishira语言
是
非语言口语
的
instance
No TPTP formula. May not be expressible in strict first order.
Languages.kif 14550-14550
AbkhazLanguage
是
北方白种人语言
的
instance
No TPTP formula. May not be expressible in strict first order.
MilitaryProcesses.kif 2410-2410
中止
是
二元函数
的
instance
No TPTP formula. May not be expressible in strict first order.
MilitaryProcesses.kif 2476-2476
中止发射
是
二元函数
的
instance
No TPTP formula. May not be expressible in strict first order.
MilitaryProcesses.kif 2430-2430
任务中止
是
二元函数
的
instance
No TPTP formula. May not be expressible in strict first order.
Merge.kif 17043-17043
以上
是
AntiSymmetricPositionalAttribute
的
instance
No TPTP formula. May not be expressible in strict first order.
Merge.kif 17042-17042
以上
是
位置属性
的
instance
No TPTP formula. May not be expressible in strict first order.
Merge.kif 4761-4761
绝对值函数
是
总值关系
的
instance
No TPTP formula. May not be expressible in strict first order.
Merge.kif 4760-4760
绝对值函数
是
一元函数
的
instance
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