No TPTP formula. May not be expressible in strict first order.	Music.kif 408-419	如果 DemoRecording 是 客体 的 attribute 和 那个 客体 是 Recording 的 instance， 然后 那个 客体 的 目的 是 有存在 实体， 另一个 实体， and 和 那个 客体USIC 这样 那个 实体 是 示范 的 instance 和 那个 客体 是个 那个 客体USIC 的 record 和 那个 客体USIC 是 那个 实体 的 patient 和 那个 实体 在 那个 另外 实体 结束 和 那个 另外 实体 是 一群人 的 instance
No TPTP formula. May not be expressible in strict first order.	Music.kif 378-385	如果 LiveRecording 是 有内用物体 的 attribute 和 那个 有内用物体 是 Recording 的 instance， 然后 有存在 物理 这样 那个 物理 是 性能 的 instance 和 那个 有内用物体 是个 那个 物理 的 record
No TPTP formula. May not be expressible in strict first order.	Music.kif 426-436	如果 MashupRecording 是 客体 的 attribute 和 那个 客体 是 Recording 的 instance， 然后 有存在 那个 客体1， 那个 客体2,， ， 音乐， and 和 另一个 音乐 这样 那个 客体1 是 那个 音乐 的 recording 和 那个 客体2 是 那个 另外 音乐 的 recording 和 那个 音乐 不 equal 那个 另外 音乐 和 那个 客体1 是 那个 客体 的 part 和 那个 客体2 是 那个 客体 的 part
No TPTP formula. May not be expressible in strict first order.	Music.kif 392-400	如果 StudioRecording 是 有内用物体 的 attribute 和 那个 有内用物体 是 Recording 的 instance， 然后 有存在 过程 和 客体 这样 那个 有内用物体 是个 那个 过程 的 record 和 那个 过程 是 located 在 那个 客体 和 那个 客体 是 RecordingStudio 的 instance
No TPTP formula. May not be expressible in strict first order.	Music.kif 457-470	如果 CoverRecording 是 音乐录音 的 attribute 和 那个 音乐录音 是 音乐录音 的 instance 和 有认知的主事 是 performer 在 那个 音乐录音 和 那个 音乐录音 是 音乐 的 recording 和 那个 音乐录音 是个 那个 音乐M 的 record ， 然后 有存在 另一个 音乐录音， 那个 有认知的主事RTIST， and 和 那个 音乐USIC 这样 那个 另外 音乐录音 是 那个 音乐 的 recording 和 那个 有认知的主事RTIST 是 performer 在 那个 另外 音乐录音 和 那个 有认知的主事 不 equal 那个 有认知的主事RTIST 和 那个 另外 音乐录音 是个 那个 音乐USIC 的 record 和 那个 音乐USIC 出现 的 time%n在那个 音乐M 出现 的 timebefore发生
No TPTP formula. May not be expressible in strict first order.	Mid-level-ontology.kif 12536-12546	如果 属性 是 客体 的 attribute 和 那个 属性 是 指纹 的 instance 和 那个 客体 不 是 手指 的 instance， 然后 有存在 那个 属性R 和 另一个 客体 这样 那个 另外 客体 是导致 那个 属性R 的 instrument 和 那个 另外 客体 是 手指 的 instance 和 那个 属性 是 那个 另外 客体 的 attribute 和 那个 客体 是 那个 属性R 的 patient
No TPTP formula. May not be expressible in strict first order.	Merge.kif 17354-17367	如果 属性 是 客体 的 attribute 和 那个 属性 是 主观评价属性 的 instance， 然后 有存在 时间位置， 过程， and 和 施事体 这样 那个 过程 是 判断 的 instance 和 那个 施事体 是 那个 过程 的 agent 和 那个 客体 是 那个 过程 的 patient 和 那个 属性 是 那个 客体 的 attribute 是 那个 过程 的 result 和 那个 施事体 believes 那个 客体 有 那个 属性 的 attribute 在 那个 时间位置 holdsDuring
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.	FinancialOntology.kif 2008-2029	如果 限价订单 是 金融交易 的 attribute 和 协议 是 那个 金融交易 的 party 协议 和 经纪人 是 那个 协议 的 attribute 和 那个 金融交易 是 對於 安全 的 order 购买 和 那个 安全 的 measure 是 物理量 和 实数 测量单位 是 那个 金融交易 的 limit 价格 和 那个 测量单位 是 UnitOfCurrency 的 instance 和 施事体 为了 那个 安全 asks 另一个 实数 那个 测量单位 和 那个 另外 实数 是 lessThanOrEqualTo 那个 实数， 然后 那个 协议 有义务执行 符号串 所描述的类别 的任务
No TPTP formula. May not be expressible in strict first order.	FinancialOntology.kif 2031-2052	如果 限价订单 是 金融交易 的 attribute 和 协议 是 那个 金融交易 的 party 协议 和 经纪人 是 那个 协议 的 attribute 和 那个 金融交易 是 對於 安全 的 order 出售 和 那个 安全 的 measure 是 物理量 和 实数 测量单位 是 那个 金融交易 的 limit 价格 和 施事体 bids 另一个 实数 那个 测量单位 對於 那个 安全 和 那个 测量单位 是 UnitOfCurrency 的 instance 和 那个 另外 实数 是 greaterThanOrEqualTo 那个 实数， 然后 那个 协议 有义务执行 符号串 所描述的类别 的任务
No TPTP formula. May not be expressible in strict first order.	FinancialOntology.kif 1981-1990	如果 市场秩序 是 金融交易 的 attribute 和 经纪人 是 协议 的 attribute 和 那个 协议 是 那个 金融交易 的 party 协议 和 那个 金融交易 是 對於 安全 的 order 另一个 有点 金融交易 ， 然后 那个 协议 有义务执行 符号串 所描述的类别 的任务
No TPTP formula. May not be expressible in strict first order.	Mid-level-ontology.kif 18727-18736	如果 大学新生 是 地位 的 attribute 和 人类 在 机构 任职 那个 地位， 然后 有存在 实数 这样 那个 人类 是 那个 机构 的 student 在 那个 实数 年持续时间 holdsDuring 和 那个 实数 是 lessThan 1
No TPTP formula. May not be expressible in strict first order.	Mid-level-ontology.kif 18742-18752	如果 大学三年级 是 地位 的 attribute 和 人类 在 机构 任职 那个 地位， 然后 有存在 实数 这样 那个 人类 是 那个 机构 的 student 在 那个 实数 年持续时间 holdsDuring 和 那个 实数 是 greaterThanOrEqualTo 2 和 那个 实数 是 lessThan 3
No TPTP formula. May not be expressible in strict first order.	Mid-level-ontology.kif 18758-18768	如果 大学高年级 是 地位 的 attribute 和 人类 在 机构 任职 那个 地位， 然后 有存在 实数 这样 那个 人类 是 那个 机构 的 student 在 那个 实数 年持续时间 holdsDuring 和 那个 实数 是 greaterThanOrEqualTo 3 和 那个 实数 是 lessThan 4
No TPTP formula. May not be expressible in strict first order.	Mid-level-ontology.kif 18774-18784	如果 大学二年级学生 是 地位 的 attribute 和 人类 在 机构 任职 那个 地位， 然后 有存在 实数 这样 那个 人类 是 那个 机构 的 student 在 那个 实数 年持续时间 holdsDuring 和 那个 实数 是 greaterThanOrEqualTo 1 和 那个 实数 是 lessThan 2
No TPTP formula. May not be expressible in strict first order.	ArabicCulture.kif 134-143	如果 穆斯林 是 客体 的 attribute 和 那个 客体 能够担当 主事 的角色做 朝觐， 然后 有存在 实体 这样 那个 实体 是 朝觐 的 instance 和 那个 客体 是 那个 实体 的 agent 的声明 has 义务 的语气
No TPTP formula. May not be expressible in strict first order.	Mid-level-ontology.kif 21023-21029	如果 教授 是 人类 的 attribute 和 那个 人类 在 教育机构 任职 教授， 然后 那个 人类 是个 teacher 在 那个 教育机构 和 那个 教育机构 是 中学后 的 instance
No TPTP formula. May not be expressible in strict first order.	Hotel.kif 1186-1201	如果 Oversized 是 客体 的 attribute 和 那个 客体 是 类 的 immediateInstance 和 那个 类 是 HotelUnit 的 subclass， 然后 有存在 物理， 实数,， ， 另一个 实数， and 和 测量单位 这样 那个 物理 是 那个 类 的 immediateInstance 和 那个 测量单位 是 UnitOfArea 的 instance 和 那个 物理 的 measure 是 那个 实数 那个 测量单位 和 那个 客体 的 measure 是 那个 另外 实数 那个 测量单位 和 那个 实数 是 面积测量 的 instance 和 那个 另外 实数 是 面积测量 的 instance 和 那个 另外 实数 是 greaterThan 那个 实数
No TPTP formula. May not be expressible in strict first order.	Mid-level-ontology.kif 19442-19452	如果 强调 是 客体 的 attribute 和 另一个 客体 是 字词 的 instance 和 那个 客体 是 那个 另外 客体 的 part， 然后 不存在 那个 客体2 这样 那个 客体2 是 音节 的 instance 和 那个 客体2 是 那个 另外 客体 的 part 和 强调 是 那个 客体2 的 attribute 和 那个 客体2 不 equal 那个 客体
No TPTP formula. May not be expressible in strict first order.	Mid-level-ontology.kif 30092-30100	如果 Uninhabited 是 客体 的 attribute 和 那个 客体 是 地区 的 instance， 然后 不存在 生物 这样 那个 生物 是 人类 的 instance 和 那个 生物 住在 那个 客体
No TPTP formula. May not be expressible in strict first order.	Mid-level-ontology.kif 26548-26555	如果 属性 是 客体 的 attribute 和 那个 属性 是 HemisphereFigure 的 instance， 然后 有存在 另一个 客体 这样 那个 另外 客体 是 球 的 instance 和 那个 客体 是 那个 另外 客体 的 half
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 和 那个 第四 客体 接上 那个 另外 客体
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