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.	Hotel.kif 1127-1140	如果 客体 是 机构 的财产 的 element 和 AnnexRoom 是 那个 客体 的 attribute 和 那个 客体 是 HotelRoom 的 instance， 然后 有存在 另一个 客体， 第三 客体， and 和 另一个 机构 这样 那个 另外 机构 是 那个 机构 Organization 的一部分 和 那个 另外 机构 是 HotelFrontDesk 的 instance 和 那个 另外 机构 是 located 在 那个 另外 客体 和 那个 另外 客体 是 那个 机构 的财产 的 element 和 那个 第三 客体 是 那个 机构 的财产 的 element 和 那个 客体 是 那个 第三 客体 的 part 和 那个 另外 客体 不 equal 那个 第三 客体
No TPTP formula. May not be expressible in strict first order.	Geography.kif 1922-1930	如果 实数 测量单位 是 自身连接物体 的 elevation 和 那个 测量单位 是 UnitOfLength 的 instance 和 那个 自身连接物体 是 土地形式 的 instance， 然后 有存在 另一个 自身连接物体 这样 那个 另外 自身连接物体 是 那个 自身连接物体 的 top 和 那个 另外 自身连接物体 和 海平面 的 distance 是 那个 实数 那个 测量单位
No TPTP formula. May not be expressible in strict first order.	Hotel.kif 1522-1535	如果 施事体 employs 有认知的主事 和 旅客住宿 是 那个 施事体 的 attribute 和 TennisProfessional 是 那个 有认知的主事 的 attribute 和 另一个 有认知的主事 是在 那个 施事体 的 guest ， 然后 有存在 实体 和 另一个 实体 这样 那个 实体 是 Tennis 的 instance 和 那个 有认知的主事 participates 在 那个 实体 和 那个 另外 有认知的主事 participates 在 那个 实体 和 那个 实体 是 located 在 那个 另外 实体 和 那个 施事体 是 located 在 那个 另外 实体 的声明 has 可能性 的语气
No TPTP formula. May not be expressible in strict first order.	Medicine.kif 3040-3054	如果 施事体 employs 有认知的主事 和 过程 是 DoNetworkMessaging 的 instance 和 客体 是 那个 过程 的 result 和 NSFW 是 那个 客体 的 attribute 和 另一个 过程 是 看 的 instance 和 那个 客体 是 那个 另外 过程 的 patient 和 那个 有认知的主事 是 那个 另外 过程 的 agent， 然后 有存在 实体 这样 那个 另外 过程 causes 那个 实体 和 那个 有认知的主事 suffers 从 那个 实体 的声明 has 可能性 的语气
No TPTP formula. May not be expressible in strict first order.	Medicine.kif 3022-3038	如果 施事体 employs 有认知的主事 和 那个 施事体 employs 另一个 有认知的主事 和 过程 是 DoNetworkMessaging 的 instance 和 客体 是 那个 过程 的 result 和 NSFW 是 那个 客体 的 attribute 和 那个 有认知的主事 是 那个 过程 的 agent 和 另一个 过程 是 看 的 instance 和 那个 客体 是 那个 另外 过程 的 patient 和 那个 另外 有认知的主事 是 那个 另外 过程 的 agent， 然后 有存在 那个 有认知的主事ROC 这样 那个 过程 causes 那个 有认知的主事ROC 和 那个 有认知的主事 suffers 从 那个 有认知的主事ROC 的声明 has 容易 的语气
No TPTP formula. May not be expressible in strict first order.	Hotel.kif 1347-1358	如果 工程组件 是 互联网 的 component 和 另一个 工程组件 是 互联网 的 component 和 那个 工程组件 不 equal 那个 另外 工程组件， 然后 互联网 的 目的 是 有存在 实体 这样 那个 实体 是 沟通 的 instance 和 那个 工程组件 是 那个 实体 的 agent 和 那个 实体 在 那个 另外 工程组件 结束 和 互联网 是导致 那个 实体 的 instrument
No TPTP formula. May not be expressible in strict first order.	Anatomy.kif 1923-1939	如果 ennervates 有点 Nerve and 有点 肌肉 和 客体 是 有点 Nerve 的 instance 和 另一个 客体 是 有点 肌肉 的 instance 和 那个 客体 是 第三 客体 的 part 和 那个 另外 客体 是 那个 第三 客体 的 part 和 Healthy 是 那个 第三 客体 的 attribute 和 那个 第三 客体 是 人类 的 instance， 然后 那个 客体 的 目的 是 有存在 那个 客体F 和 另一个 实体 这样 那个 客体F 是 NerveFiring 的 instance 和 那个 客体 是导致 那个 客体F 的 instrument 和 那个 有点 肌肉 是 MuscleContraction 的 instance 和 那个 另外 客体 是导致 那个 另外 客体V 的 instrument 和 那个 客体F causes 那个 有点 肌肉
No TPTP formula. May not be expressible in strict first order.	Merge.kif 4874-4888	如果 @ROW 的最大公因数 equal 整数 和 那个 整数 不 equal 0， 然后 不存在 另一个 整数 这样 那个 另外 整数 是 greaterThan 那个 整数 和 对所有 第三 整数 如果 那个 第三 整数 是 (@ROW) 的 member， 然后 那个 第三 整数 模除 那个 另外 整数 equal 0
No TPTP formula. May not be expressible in strict first order.	Merge.kif 4958-4972	如果 @ROW 的最小公倍数 equal 整数 和 那个 整数 不 equal 0， 然后 不存在 另一个 整数 这样 那个 另外 整数 是 lessThan 那个 整数 和 对所有 第三 整数 如果 那个 第三 整数 是 (@ROW) 的 member， 然后 那个 另外 整数 模除 那个 第三 整数 equal 0
No TPTP formula. May not be expressible in strict first order.	WMD.kif 823-840	如果 实数 每公斤微克 equal 质量测量 是 另一个 质量测量 的 per 和 那个 另外 质量测量 equal 另一个 实数 公克 的百万分之一 和 那个 质量测量 equal 第三 实数 公克 的一千倍， 然后 有存在 过程， 自身连接物体， and 和 另一个 自身连接物体 这样 那个 过程 是 消化 的 instance 和 那个 自身连接物体 是 生物活性物质 的 instance 和 那个 另外 自身连接物体 是 生物 的 instance 和 那个 自身连接物体 是 那个 过程 的 patient 和 那个 另外 自身连接物体 是 那个 过程 的 agent 和 那个 另外 质量测量 是 那个 自身连接物体 的 weight 和 那个 质量测量 是 那个 另外 自身连接物体 的 weight
No TPTP formula. May not be expressible in strict first order.	Music.kif 936-946	如果 有点 DataStorageDevice equal Album 在 有点 DataStorageDeviceS 的 set 复制 和 第三 DataStorageDevice 是 那个 有点 DataStorageDevice 的 instance， 然后 对所有 客体 如果 那个 客体 是 那个 Album 的 member， 然后 有存在 有内用物体 这样 那个 有内用物体 是和 那个 客体 完全相同的 copy 和 那个 有内用物体 是 stored 在 那个 第三 DataStorageDevice
No TPTP formula. May not be expressible in strict first order.	Economy.kif 3754-3764	如果 时距 equal 施事体 和 有点 年 的 fiscal 开始年分 和 另一个 有点 时距 是 那个 施事体 的 fiscal 年周期 和 那个 时距 是 另一个 有点 时距 的 instance， 然后 有存在 第三 时距 和 时间位置 这样 那个 第三 时距 是 日 的 instance 和 那个 第三 时距 starts了才到 那个 时距 和 那个 时间位置 是 有点 年 的 instance 和 那个 第三 时距 时段 是 那个 时间位置 时段 的一 part
No TPTP formula. May not be expressible in strict first order.	Merge.kif 3083-3102	如果 串列 equal List包含 另一个 串列 和 第三 串列 和 那个 另外 串列 不 equal 空列表 和 那个 第三 串列 不 equal 空列表 和 正整数 是 lessThanOrEqualTo 那个 另外 串列 的长度 和 另一个 正整数 是 lessThanOrEqualTo 那个 第三 串列 的长度 和 那个 正整数 是 正整数 的 instance 和 那个 另外 正整数 是 正整数 的 instance， 然后 那个 串列 的第 那个 正整数 几个元素 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 5267-5276	如果 有点 客体 equal OrganicObjectFn 有点 有机物体 和 有点 客体 是 客体 的 subclass， 然后 有存在 另一个 客体 和 第三 客体 这样 那个 另外 客体 是 一个 dead 有点 有机物体 的 instance 和 那个 另外 客体 是 那个 第三 客体 的 part 和 那个 第三 客体 是 那个 有点 有机物体 的 instance
No TPTP formula. May not be expressible in strict first order.	Music.kif 867-876	如果 歌曲 equal song 构成 音乐作品 和 LyricalContent 和 那个 歌曲 表示 过程 的内容， 然后 有存在 另一个 过程 和 第三 过程 这样 那个 音乐作品 是 那个 另外 过程 的 patient 和 那个 LyricalContent 是 那个 第三 过程 的 patient 和 那个 另外 过程%n是那个 过程的subProcess 和 那个 第三 过程%n是那个 过程的subProcess
No TPTP formula. May not be expressible in strict first order.	Weather.kif 2001-2013	如果 串列 equal 在 时距 时间结束以前， 发生在区域 地理区域 的 Mean3SecondWindSpeedListFn (平均3秒风速表列) 和 函数量 是 那个 串列 的 member， 然后 有存在 那个 时距LIST 和 另一个 时距 这样 那个 时距LIST equal 那个 时距 的 3 第二期 ConsecutiveTimeIntervalList 是在 TimeIntervalListFn(时间间隔表列函数) 和 那个 另外 时距 是 那个 时距LIST 的 member 和 那个 函数量 equal 那个 地理区域地区在那个 另外 时距时段的 Mean3SecondWindSpeedFn
No TPTP formula. May not be expressible in strict first order.	Economy.kif 5235-5244	如果 有点 客体 equal OrganicObjectFn 另一个 有点 客体 和 有点 客体 是 WoodProduct 的 subclass 和 另一个 有点 客体 是 PlantStem 的 subclass， 然后 有存在 第三 有点 客体 这样 第三 有点 客体 是 植物树 的 subclass 和 %每个 那个 另外 有点 客体 是 那个 第三 有点 客体 的 initially part
No TPTP formula. May not be expressible in strict first order.	Merge.kif 1780-1788	如果 有点 客体 equal 另一个 有点 客体 跟 属性 的 attr 和 第三 客体 是 有点 客体 的 instance， 然后 那个 第三 客体 是 另一个 有点 客体 的 instance 和 那个 有点 客体 是 那个 另外 有点 客体 的 subclass 和 那个 属性 是 那个 第三 客体 的 attribute
No TPTP formula. May not be expressible in strict first order.	Media.kif 2093-2103	如果 那只能是 1 values 对于 关系 的参数 正整数 和 那个 关系 是 谓语 的 instance 和 那个 关系 @ARGS 和 另一个 实体 equal (@ARGS) 的第 那个 正整数 几个元素， 然后 不存在 第三 实体 这样 那个 第三 实体 equal (@ARGS) 的第 那个 正整数 几个元素 和 那个 另外 实体 不 equal 那个 第三 实体
No TPTP formula. May not be expressible in strict first order.	Media.kif 2075-2090	如果 那只能是 1 values 对于 关系 的参数 正整数 和 那个 关系 是 谓语 的 instance， 然后 有存在 实体 和 @ARGS 这样 那个 关系 @ARGS 和 那个 实体 equal (@ARGS) 的第 那个 正整数 几个元素 和 不存在 第三 实体 这样 那个 第三 实体 equal (@ARGS) 的第 那个 正整数 几个元素 和 那个 实体 不 equal 那个 第三 实体
No TPTP formula. May not be expressible in strict first order.	Media.kif 2137-2150	如果 那只能是 整数 values 对于 关系 的参数 正整数 和 那个 关系 是 谓语 的 instance， 然后 有存在 类， 实体， and 和 @ARGS 这样 那个 类 是 集或类 的 instance 和 如果 那个 关系 @ARGS 和 那个 实体 equal (@ARGS) 的第 那个 正整数 几个元素， 然后 那个 实体 是 那个 类 的 instance 和 那个 类 instance 的数量 equal 那个 整数
No TPTP formula. May not be expressible in strict first order.	Mid-level-ontology.kif 6356-6363	如果 施事体 经历了 过程 和 那个 施事体 是 PainFn 身体部位 的 instance， 然后 有存在 那个 身体部位ART 这样 那个 身体部位ART 是 那个 过程 的 part 和 那个 身体部位ART 是 located 在 那个 身体部位
No TPTP formula. May not be expressible in strict first order.	Economy.kif 2277-2286	如果 地缘政治区域 对于 有点 时距 在周期 货币测量 export 全部 和 有点 时距 是 年 的 subclass 或 那个 有点 时距 是 那个 地缘政治区域 的 fiscal 年 的 subclass， 然后 有存在 时间位置 这样 那个 时间位置 是 那个 有点 时距 的 instance 和 那个 货币测量 是 那个 地缘政治区域 的 annual 总共输出 在 那个 时间位置 holdsDuring
Display limited to 25 items. Show next 25
Display limited to 25 items. Show next 25

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