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
or
Sigma KEE - or
or
appearance as argument number 2
No TPTP formula. May not be expressible in strict first order.
domainEnglishFormat.kif 42384-42384
No TPTP formula. May not be expressible in strict first order.
domainEnglishFormat.kif 42383-42383
No TPTP formula. May not be expressible in strict first order.
domainEnglishFormat.kif 42382-42382
antecedent
No TPTP formula. May not be expressible in strict first order.
Mid-level-ontology.kif 24713-24720
PostalPlace
是
located
在
地缘政治区域
和
那个 PostalPlace
是
PostalPlace
的
instance
和
那个 地缘政治区域
是
国家
的
instance
或
那个 地缘政治区域
是
依赖或特殊主权领域
的
instance
若且唯若
那个 PostalPlace
是在
那个 地缘政治区域
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.
Mid-level-ontology.kif 26159-26171
如果
WheelchairAccessible
是
客体
的
attribute
和
那个 客体
是
建筑物
的
instance
或
那个 客体
是
房间
的
instance
,
然后 有存在
实体
和
另一个 实体
这样
那个 实体
是
运动
的
instance
和
那个 另外 实体
是导致
那个 实体
的
instrument
和
那个 另外 实体
是
Wheelchair
的
instance
和
那个 实体
是
located
在
那个 客体
的声明 has
可能性
的语气
No TPTP formula. May not be expressible in strict first order.
Biography.kif 730-740
如果
作家
是
施事体
的
attribute
和
实体
是
有点 有内用物体
的
instance
和
有点 有内用物体
是
文本
的
subclass
或
那个 有点 有内用物体
是
Document
的
subclass
和
过程
是
写作
的
instance
和
那个 施事体
是
那个 过程
的
agent
和
那个 实体
是
那个 过程
的
result
,
然后
那个 施事体
是
那个 有点 有内用物体
的
authors
No TPTP formula. May not be expressible in strict first order.
Medicine.kif 367-385
如果
breathingRate
施事体
,
时距
and
整数
和
那个 时距
是
分钟
的
instance
和 不存在
那个 整数
这样
那个 整数
是
娱乐或锻炼
的
instance
和
那个 施事体
是
那个 整数
的
agent
和
那个 时距
在
那个 整数
出现 的
time
时段内发生 和
人类成人
是
那个 施事体
的
attribute
在
那个 时距
holdsDuring
和
那个 整数
是
greaterThan
16 或
那个 整数
是
lessThan
12,
然后
Healthy
不 是
那个 施事体
的
attribute
在
那个 时距
holdsDuring
No TPTP formula. May not be expressible in strict first order.
Economy.kif 2112-2121
如果
地缘政治区域
是 对于
有点 时距
在其间
物理量
的
electricity
消耗 和
有点 时距
是
年
的
subclass
或
那个 有点 时距
是
那个 地缘政治区域
的
fiscal
年 的
subclass
,
然后 有存在
时间位置
这样
那个 时间位置
是
那个 有点 时距
的
instance
和
那个 物理量
是
那个 地缘政治区域
的
annual
电力消耗 在
那个 时间位置
holdsDuring
No TPTP formula. May not be expressible in strict first order.
Economy.kif 2156-2165
如果
地缘政治区域
是 对于
有点 时距
在周期
物理量
的
electricity
输出 和
有点 时距
是
年
的
subclass
或
那个 有点 时距
是
那个 地缘政治区域
的
fiscal
年 的
subclass
,
然后 有存在
时间位置
这样
那个 时间位置
是
那个 有点 时距
的
instance
和
那个 物理量
是
那个 地缘政治区域
的
annual
电力输出 在
那个 时间位置
holdsDuring
No TPTP formula. May not be expressible in strict first order.
Economy.kif 2202-2211
如果
地缘政治区域
是 对于
有点 时距
在周期
物理量
的
electricity
输出 和
有点 时距
是
年
的
subclass
或
那个 有点 时距
是
那个 地缘政治区域
的
fiscal
年 的
subclass
,
然后 有存在
时间位置
这样
那个 时间位置
是
那个 有点 时距
的
instance
和
那个 物理量
是
那个 地缘政治区域
annual
的电力输入 在
那个 时间位置
holdsDuring
No TPTP formula. May not be expressible in strict first order.
Economy.kif 1980-1989
如果
地缘政治区域
是 对于
有点 时距
在周期
物理量
的
electricity
生产 和
有点 时距
是
年
的
subclass
或
那个 有点 时距
是
那个 地缘政治区域
的
fiscal
年 的
subclass
,
然后 有存在
时间位置
这样
那个 时间位置
是
那个 有点 时距
的
instance
和
那个 物理量
是
那个 地缘政治区域
的
annual
电力生产 在
那个 时间位置
holdsDuring
No TPTP formula. May not be expressible in strict first order.
Merge.kif 5993-6006
如果
图路径
的值
equal
实数
和
图弧
是
那个 图路径
的
part
和
另一个 图弧
是
那个 图路径
的
part
和
那个 图弧
的值 是
另一个 实数
和
那个 另外 图弧
的值 是
第三 实数
和 对所有
图元素
如果
那个 图元素
是
那个 图路径
的
part
,
然后
那个 图元素
equal
那个 图弧
或
那个 图元素
equal
那个 另外 图弧
,
然后
那个 图路径
的值
equal
(
那个 另外 实数
和
那个 第三 实数
)
No TPTP formula. May not be expressible in strict first order.
Merge.kif 5979-5991
如果
图路径
的值
equal
实数
和
另一个 图路径
是
那个 图路径
的
subGraph
和
图弧
是
那个 图路径
的
part
和
那个 图弧
的值 是
另一个 实数
和 对所有
图元素
如果
那个 图元素
是
那个 图路径
的
part
,
然后
那个 图元素
是
那个 另外 图路径
的
part
或
那个 图元素
equal
那个 图弧
,
然后
那个 实数
equal
(
那个 另外 图路径
的值 和
那个 另外 实数
)
No TPTP formula. May not be expressible in strict first order.
Economy.kif 4532-4543
如果
有点 客体
equal
OrganicObjectFn
另一个 有点 客体
和
有点 客体
是
OilFromPlant
的
subclass
和
另一个 有点 客体
是
种子
的
subclass
或
那个 另外 有点 客体
是
水果
的
subclass
,
然后 有存在
第三 有点 客体
这样
第三 有点 客体
是
开花植物
的
subclass
和 %每个
那个 另外 有点 客体
是
那个 第三 有点 客体
的
initially
part
No TPTP formula. May not be expressible in strict first order.
Economy.kif 2277-2286
如果
地缘政治区域
对于
有点 时距
在周期
货币测量
export
全部 和
有点 时距
是
年
的
subclass
或
那个 有点 时距
是
那个 地缘政治区域
的
fiscal
年 的
subclass
,
然后 有存在
时间位置
这样
那个 时间位置
是
那个 有点 时距
的
instance
和
那个 货币测量
是
那个 地缘政治区域
的
annual
总共输出 在
那个 时间位置
holdsDuring
No TPTP formula. May not be expressible in strict first order.
Hotel.kif 841-862
如果
有点 物理
是
free
对于顾客出租
有点 HotelFunctionRoom
和
实体
是
有点 HotelFunctionRoom
的
instance
和
那个 实体
是
施事体
的财产 的
element
和
过程
是
租
的
instance
和
那个 实体
是
那个 过程
的
patient
和
那个 过程
在
有认知的主事
结束 和
客体
是
有点 物理
的
instance
和
那个 施事体
possesses
那个 客体
和
那个 施事体
是
那个 有认知的主事
的
customer
和
那个 客体
是
过程
的
instance
和
那个 有认知的主事
是
那个 客体
的
agent
或
那个 有认知的主事
经历了
那个 客体
或
那个 施事体
possesses
那个 客体
和
那个 客体
是
客体
的
instance
和
那个 有认知的主事
uses
那个 客体
,
然后
那个 客体
是 对于
那个 施事体
的
price
0
美国美元
No TPTP formula. May not be expressible in strict first order.
Hotel.kif 546-561
如果
有点 物理
的使用是对于
施事体
免费 和
过程
是
有点 物理
的
instance
和
那个 施事体
是
有认知的主事
的
customer
和
那个 过程
是
过程
的
instance
和
那个 有认知的主事
是
那个 过程
的
agent
或
那个 有认知的主事
经历了
那个 过程
或
那个 施事体
possesses
那个 过程
和
那个 过程
是
客体
的
instance
和
那个 有认知的主事
uses
那个 过程
,
然后
那个 过程
是 对于
那个 施事体
的
price
0
美国美元
No TPTP formula. May not be expressible in strict first order.
Hotel.kif 346-361
如果
有点 物理
的使用是对于
有点 HotelUnit
免费 和
有点 物理
是
客体
的
subclass
和
暂住
是
有点 HotelUnit
的
instance
和
人类
stays
在
那个 暂住
和
那个 暂住
是
施事体
的财产 的
element
和
客体
是
那个 有点 物理
的
instance
和
那个 客体
是
located
在
那个 暂住
和
过程
是
过程
的
instance
和
那个 人类
是
那个 过程
的
agent
和
那个 客体
是
那个 过程
的
patient
或
那个 客体
是导致
那个 过程
的
instrument
或
那个 客体
是
那个 过程
的
resource
,
然后
那个 客体
是 对于
那个 人类
的
price
0
美国美元
No TPTP formula. May not be expressible in strict first order.
Hotel.kif 364-378
如果
有点 物理
的使用是对于
有点 HotelUnit
免费 和
有点 物理
是
过程
的
subclass
和
暂住
是
有点 HotelUnit
的
instance
和
人类
stays
在
那个 暂住
和
那个 暂住
是
施事体
的财产 的
element
和
那个 人类
是
过程
的
patient
和
那个 过程
是
那个 有点 物理
的
instance
或
另一个 过程
是
那个 有点 物理
的
instance
和
那个 过程
%n是
那个 另外 过程
的
subProcess
和
那个 过程
是
located
在
那个 暂住
,
然后
那个 过程
是 对于
那个 人类
的
price
0.0
美国美元
No TPTP formula. May not be expressible in strict first order.
Anatomy.kif 1838-1860
如果
LateralRecumbant
是
客体
的
attribute
和
那个 客体
在
另一个 客体
的
上
在
时间位置
holdsDuring
和
第三 客体
是
LeftArm
的
instance
和
那个 第三 客体
是
那个 客体
的
part
和
第四 客体
是
RightArm
的
instance
和
那个 第四 客体
是
那个 客体
的
part
和
第五 客体
是
LeftLeg
的
instance
和
那个 第五 客体
是
那个 客体
的
part
和
第六 客体
是
RightLeg
的
instance
和
那个 第六 客体
是
那个 客体
的
part
和
那个 第三 客体
接上
那个 另外 客体
或
那个 第五 客体
接上
那个 另外 客体
,
然后
那个 第四 客体
不 接上
那个 另外 客体
和
那个 第六 客体
不 接上
那个 另外 客体
在
那个 时间位置
holdsDuring
No TPTP formula. May not be expressible in strict first order.
Anatomy.kif 1862-1884
如果
LateralRecumbant
是
客体
的
attribute
和
那个 客体
在
另一个 客体
的
上
在
时间位置
holdsDuring
和
第三 客体
是
LeftArm
的
instance
和
那个 第三 客体
是
那个 客体
的
part
和
第四 客体
是
RightArm
的
instance
和
那个 第四 客体
是
那个 客体
的
part
和
第五 客体
是
LeftLeg
的
instance
和
那个 第五 客体
是
那个 客体
的
part
和
第六 客体
是
RightLeg
的
instance
和
那个 第六 客体
是
那个 客体
的
part
和
那个 第四 客体
接上
那个 另外 客体
或
那个 第六 客体
接上
那个 另外 客体
,
然后
那个 第三 客体
不 接上
那个 另外 客体
和
那个 第五 客体
不 接上
那个 另外 客体
在
那个 时间位置
holdsDuring
No TPTP formula. May not be expressible in strict first order.
Economy.kif 2123-2130
如果
物理量
是
地缘政治区域
的
annual
电力消耗 在
时间位置
holdsDuring
和
那个 时间位置
是
有点 时距
的
instance
和
有点 时距
是
年
的
subclass
或
那个 有点 时距
是
那个 地缘政治区域
的
fiscal
年 的
subclass
,
然后
那个 地缘政治区域
是 对于
那个 有点 时距
在其间
那个 物理量
的
electricity
消耗
No TPTP formula. May not be expressible in strict first order.
Economy.kif 2167-2174
如果
物理量
是
地缘政治区域
的
annual
电力输出 在
时间位置
holdsDuring
和
那个 时间位置
是
有点 时距
的
instance
和
有点 时距
是
年
的
subclass
或
那个 有点 时距
是
那个 地缘政治区域
的
fiscal
年 的
subclass
,
然后
那个 地缘政治区域
是 对于
那个 有点 时距
在周期
那个 物理量
的
electricity
输出
No TPTP formula. May not be expressible in strict first order.
Economy.kif 2213-2220
如果
物理量
是
地缘政治区域
annual
的电力输入 在
时间位置
holdsDuring
和
那个 时间位置
是
有点 时距
的
instance
和
有点 时距
是
年
的
subclass
或
那个 有点 时距
是
那个 地缘政治区域
的
fiscal
年 的
subclass
,
然后
那个 地缘政治区域
是 对于
那个 有点 时距
在周期
那个 物理量
的
electricity
输出
No TPTP formula. May not be expressible in strict first order.
Economy.kif 1991-1998
如果
物理量
是
地缘政治区域
的
annual
电力生产 在
时间位置
holdsDuring
和
那个 时间位置
是
有点 时距
的
instance
和
有点 时距
是
年
的
subclass
或
那个 有点 时距
是
那个 地缘政治区域
的
fiscal
年 的
subclass
,
然后
那个 地缘政治区域
是 对于
那个 有点 时距
在周期
那个 物理量
的
electricity
生产
No TPTP formula. May not be expressible in strict first order.
Economy.kif 2288-2295
如果
货币测量
是
地缘政治区域
的
annual
总共输出 在
时间位置
holdsDuring
和
那个 时间位置
是
有点 时距
的
instance
和
有点 时距
是
年
的
subclass
或
那个 有点 时距
是
那个 地缘政治区域
的
fiscal
年 的
subclass
,
然后
那个 地缘政治区域
对于
那个 有点 时距
在周期
那个 货币测量
export
全部
No TPTP formula. May not be expressible in strict first order.
Economy.kif 2594-2601
如果
货币测量
是
地缘政治区域
的
annual
总共输入 在
时间位置
holdsDuring
和
那个 时间位置
是
有点 时距
的
instance
和
有点 时距
是
年
的
subclass
或
那个 有点 时距
是
那个 地缘政治区域
的
fiscal
年 的
subclass
,
然后
那个 地缘政治区域
对于
那个 有点 时距
在周期
那个 货币测量
import
全部
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.
Government.kif 1400-1404
女王
是
客体
的
attribute
若且唯若
QueenRegnant
是
那个 客体
的
attribute
或
QueenConsort
是
那个 客体
的
attribute
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.
Merge.kif 1601-1607
LegalAgent
是
实体
的
attribute
在
时间位置
holdsDuring
若且唯若
那个 实体
能够担当
主事
的角色做
法律诉讼
或
那个 实体
能够担当
受事
的角色做
法律诉讼
在
那个 时间位置
holdsDuring
No TPTP formula. May not be expressible in strict first order.
Mid-level-ontology.kif 11682-11689
客体
是
骨骼
的
instance
若且唯若 有存在
另一个 客体
这样
那个 另外 客体
是
骨架
的
instance
或
那个 另外 客体
是
外骨骼
的
instance
和
那个 客体
是
那个 另外 客体
的
part
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.
Geography.kif 3488-3494
实体
是
半球
的
instance
若且唯若
那个 实体
equal
北半球
或
那个 实体
equal
南半球
或
那个 实体
equal
东半球
或
那个 实体
equal
西半球
No TPTP formula. May not be expressible in strict first order.
Government.kif 108-115
机构
是
政府组织
的
instance
若且唯若
那个 机构
是
政府
的
instance
或 有存在
另一个 机构
这样
那个 另外 机构
是
政府
的
instance
和
那个 机构
是
那个 另外 机构
Organization
的一部分
No TPTP formula. May not be expressible in strict first order.
Merge.kif 1867-1871
实数
是
lessThanOrEqualTo
另一个 实数
若且唯若
那个 实数
equal
那个 另外 实数
或
那个 实数
是
lessThan
那个 另外 实数
No TPTP formula. May not be expressible in strict first order.
Merge.kif 17103-17107
客体
在
另一个 客体
的
邻
若且唯若
那个 客体
在
那个 另外 客体
的
近
或
那个 客体
和
那个 另外 客体
是
connected
No TPTP formula. May not be expressible in strict first order.
Merge.kif 17091-17095
客体
在
另一个 客体
的
下面
若且唯若
那个 另外 客体
在
那个 客体
的
上
或
那个 另外 客体
在
那个 客体
的
以上
No TPTP formula. May not be expressible in strict first order.
Government.kif 738-753
如果
命题
agreement
对于
另一个 命题
的修改日期
有点 时间位置
,
然后 有存在
另一个 时间位置
这样
那个 另外 时间位置
是
有点 时间位置
的
instance
和
那个 另外 命题
不 是
那个 命题
的
subProposition
在 紧接
那个 另外 时间位置
before
holdsDuring
和
那个 另外 命题
是
那个 命题
的
subProposition
在 紧接
那个 另外 时间位置
after
holdsDuring
或
那个 另外 命题
是
那个 命题
的
subProposition
在 紧接
那个 另外 时间位置
before
holdsDuring
和
那个 另外 命题
不 是
那个 命题
的
subProposition
在 紧接
那个 另外 时间位置
after
holdsDuring
No TPTP formula. May not be expressible in strict first order.
FinancialOntology.kif 655-667
如果
金融账户
对于
时间位置
到期的
amount
货币测量
和
有认知的主事
持有
account
那个 金融账户
,
然后
那个 有认知的主事
有义务执行
符号串
所描述的类别 的任务
No TPTP formula. May not be expressible in strict first order.
Mid-level-ontology.kif 31387-31394
如果
applicableRelation
客体
and
关系
和
那个 客体
是
那个 客体
C 的
instance
和
那个 关系
的 1 数量 是
另一个 类
的
instance
,
然后
那个 客体
C
equal
那个 另外 类
或
那个 客体
C 是
那个 另外 类
的
subclass
No TPTP formula. May not be expressible in strict first order.
Military.kif 286-297
如果
属性
是
施事体
的
attribute
和
那个 属性
是
委任军官级别
的
instance
,
然后 有存在
过程
和
客体
这样
那个 过程
是
管理
的
instance
和
那个 施事体
是
那个 过程
的
agent
和
那个 客体
是
那个 过程
的
patient
和
那个 客体
是
军事组织
的
instance
或
士兵
是
那个 客体
的
attribute
No TPTP formula. May not be expressible in strict first order.
FinancialOntology.kif 2881-2897
如果
FOK订单
是
协议
的
attribute
和
时距
是
那个 协议
的
agreement
週期,
然后 有存在
过程
和
另一个 时距
这样
那个 过程
是
填写订单
的
instance
和
那个 协议
是
那个 过程
的
patient
和
那个 过程
出现 的
time
equal
那个 另外 时距
和
那个 另外 时距
starts
了才到
那个 时距
或 有存在
另一个 过程
和
第三 时距
这样
那个 另外 过程
是
取消订单
的
instance
和
那个 协议
是
那个 另外 过程
的
patient
和
那个 另外 过程
出现 的
time
equal
那个 第三 时距
和
那个 第三 时距
starts
了才到
那个 时距
No TPTP formula. May not be expressible in strict first order.
FinancialOntology.kif 2917-2933
如果
GTC订单
是
协议
的
attribute
和
时距
是
那个 协议
的
agreement
週期,
然后 有存在
过程
和
另一个 时距
这样
那个 过程
是
填写订单
的
instance
和
那个 协议
是
那个 过程
的
patient
和
那个 过程
出现 的
time
equal
那个 另外 时距
和
那个 时距
时段 和
那个 另外 时距
重叠 或 有存在
另一个 过程
和
第三 时距
这样
那个 另外 过程
是
取消订单
的
instance
和
那个 协议
是
那个 另外 过程
的
patient
和
那个 另外 过程
出现 的
time
equal
那个 第三 时距
和
那个 第三 时距
finishes
了才到
那个 时距
No TPTP formula. May not be expressible in strict first order.
FinancialOntology.kif 2854-2870
如果
国际奥委会订单
是
协议
的
attribute
和
时距
是
那个 协议
的
agreement
週期,
然后 有存在
过程
和
另一个 时距
这样
那个 过程
是
填写订单
的
instance
和
那个 协议
是
那个 过程
的
patient
和
那个 过程
出现 的
time
equal
那个 另外 时距
和
那个 另外 时距
starts
了才到
那个 时距
或 有存在
另一个 过程
和
第三 时距
这样
那个 另外 过程
是
取消订单
的
instance
和
那个 协议
是
那个 另外 过程
的
patient
和
那个 另外 过程
出现 的
time
equal
那个 第三 时距
和
那个 第三 时距
starts
了才到
那个 时距
No TPTP formula. May not be expressible in strict first order.
Mid-level-ontology.kif 25748-25761
如果
Multilingual
是
施事体
的
attribute
和
过程
是
说话
的
instance
和
那个 施事体
是
那个 过程
的
agent
,
然后 有存在
实体
和
另一个 实体
这样
那个 实体
是
口语人类语言
的
instance
和
那个 另外 实体
是
口语人类语言
的
instance
和
那个 实体
不
equal
那个 另外 实体
和
那个 实体
是
那个 过程
的
patient
或
那个 另外 实体
是
那个 过程
的
patient
的声明 has
可能性
的语气
No TPTP formula. May not be expressible in strict first order.
Merge.kif 13841-13854
如果
实数
测量单位
是
有点 純物质
的
boiling
点 和
实体
是
有点 純物质
的
instance
和
那个 实体
的
measure
是
另一个 实数
那个 测量单位
在
时距
holdsDuring
和
那个 测量单位
是
UnitOfTemperature
的
instance
和
那个 另外 实数
是
greaterThanOrEqualTo
那个 实数
,
然后
加油站
是
那个 实体
的
attribute
在
那个 时距
holdsDuring
或 有存在
过程
这样
那个 时距
时段 和
那个 过程
出现 的
time
重叠 和
那个 过程
是
沸腾
的
instance
和
那个 实体
是
那个 过程
的
patient
No TPTP formula. May not be expressible in strict first order.
Hotel.kif 2392-2407
如果
施事体
是
有认知的主事
的
customer
和
那个 施事体
employs
另一个 有认知的主事
和
旅客住宿
是
那个 施事体
的
attribute
和
Porter
是
那个 另外 有认知的主事
的
attribute
和
那个 有认知的主事
possesses
客体
和
那个 客体
是
旅行集装箱
的
instance
,
然后 有存在
另一个 客体
和
过程
这样
那个 另外 客体
是
HotelUnit
的
instance
和
那个 过程
是
携带
的
instance
和
那个 另外 有认知的主事
是
那个 过程
的
agent
和
那个 过程
在
那个 另外 客体
结束 或
那个 另外 客体
是
那个 过程
的源头
No TPTP formula. May not be expressible in strict first order.
Hotel.kif 504-520
如果
施事体
是
有认知的主事
的
customer
和
那个 施事体
有
有点 物理
和
有点 物理
是
客体
的
subclass
和
实体
是
那个 有点 物理
的
instance
,
然后
那个 施事体
允许
那个 有认知的主事
执行 有存在
另一个 实体
这样
那个 另外 实体
是
过程
的
instance
和
那个 实体
是
那个 另外 实体
的
resource
或
那个 实体
是导致
那个 另外 实体
的
instrument
或
那个 实体
是
那个 另外 实体
的
patient
和
那个 有认知的主事
是
那个 另外 实体
的
agent
或
那个 有认知的主事
经历了
那个 另外 实体
的任务
No TPTP formula. May not be expressible in strict first order.
Hotel.kif 522-538
如果
施事体
是
有认知的主事
的
customer
和
那个 施事体
有
有点 物理
和
有点 物理
是
过程
的
subclass
,
然后 有存在
实体
,
另一个 实体
, and 和
第三 实体
这样
那个 另外 实体
是
那个 施事体
的财产 的
element
和
那个 施事体
是
那个 实体
的
agent
和
那个 有认知的主事
是
那个 实体
的
patient
和
那个 实体
是
那个 有点 物理
的
instance
或
那个 第三 实体
是
那个 有点 物理
的
instance
和
那个 实体
%n是
那个 第三 实体
的
subProcess
和
那个 实体
是
located
在
那个 另外 实体
的声明 has
可能性
的语气
No TPTP formula. May not be expressible in strict first order.
Merge.kif 221-227
如果
关系
的
正整数
数量 是
类
的
instance
和
那个 关系
的
那个 正整数
数量 是
另一个 类
的
instance
,
然后
那个 类
是
那个 另外 类
的
subclass
或
那个 另外 类
是
那个 类
的
subclass
No TPTP formula. May not be expressible in strict first order.
Merge.kif 244-250
如果
关系
的
正整数
数量 是
类
的
subclass
和
那个 关系
的
那个 正整数
数量 是
另一个 类
的
subclass
,
然后
那个 类
是
那个 另外 类
的
subclass
或
那个 另外 类
是
那个 类
的
subclass
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.
Military.kif 933-946
地缘政治区域
和
年
每年的
reaching
军事男性年龄
equal
符号串
所描述的类别
instance
的数量
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