No TPTP formula. May not be expressible in strict first order.	Anatomy.kif 32-46	如果 connectedBodyPartTypes 有点 身体部位, 另一个 有点 身体部位 and 有点 生物 和 有点 生物C 是 那个 有点 生物 的 instance 和 疾病或综合症 不 是 另一个 客体 的 attribute， 然后 有存在 第三 客体 和 第四 客体 这样 那个 第三 客体 是 有点 身体部位 的 instance 和 那个 第四 客体 是 另一个 有点 身体部位 的 instance 和 那个 第三 客体 不 equal 那个 第四 客体 和 那个 第三 客体 是 那个 有点 生物C 的 part 和 那个 第四 客体 是 那个 有点 生物C 的 part 和 那个 第三 客体 和 那个 第四 客体 是 connected
No TPTP formula. May not be expressible in strict first order.	Dining.kif 130-150	如果 施事体 是 有认知的主事 的 customer 和 那个 施事体 对 货币测量 收费 在 corkage 为了 有点 客体 和 另一个 客体 是 有点 客体 的 instance 和 不存在 过程 这样 那个 过程 是 购买 的 instance 和 那个 另外 客体 是 那个 过程 的 patient 和 那个 过程 在 那个 有认知的主事 结束 和 那个 施事体 是 那个 过程 的源头 和 另一个 过程 是 饮 的 instance 和 那个 有认知的主事 是 那个 另外 过程 的 agent 和 那个 另外 客体 是 那个 另外 过程 的 resource， 然后 有存在 第三 过程 这样 那个 第三 过程 是 Corkage 的 instance 和 那个 有认知的主事 是 那个 第三 过程 的 agent 和 那个 第三 过程 提到 那个 另外 客体 和 那个 第三 过程 在 那个 施事体 结束
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.	Mid-level-ontology.kif 13535-13544	如果 有点 客体 的 maximum 预期价值是 实数 测量单位 和 那个 测量单位 是 CompositeUnitOfMeasure 的 instance， 然后 有存在 实体 和 那个 实数UANTITY 这样 那个 实体 是 有点 客体 的 instance 和 那个 实体 的 measure 是 那个 实数UANTITY 那个 测量单位 和 那个 实数UANTITY 是 greaterThan 那个 实数 的声明 has 较不可能 的语气
No TPTP formula. May not be expressible in strict first order.	Mid-level-ontology.kif 13546-13557	如果 有点 客体 的 maximum 预期价值是 实数 测量单位 和 类 是 NonCompositeUnitOfMeasure 的 subclass 和 那个 测量单位 是 那个 类 的 instance， 然后 有存在 实体， 那个 实数UANTITY， and 和 第三 实体 这样 那个 实体 是 有点 客体 的 instance 和 那个 实体 的 measure 是 那个 实数UANTITY 那个 第三 实体 和 那个 第三 实体 是 那个 类 的 instance 和 那个 实数UANTITY 那个 第三 实体 是 greaterThan 那个 实数 那个 测量单位 的声明 has 较不可能 的语气
No TPTP formula. May not be expressible in strict first order.	Mid-level-ontology.kif 13485-13496	如果 有点 客体 的 maximum 預期半径是 实数 测量单位 和 另一个 客体 是 有点 客体 的 instance 和 球 是 那个 另外 客体 的 attribute， 然后 有存在 那个 实数ADIUS 这样 那个 另外 客体 的 radius 是 那个 实数ADIUS 那个 测量单位 和 那个 实数ADIUS 是 greaterThan 那个 实数 的声明 has 较不可能 的语气
No TPTP formula. May not be expressible in strict first order.	Mid-level-ontology.kif 13565-13574	如果 有点 客体 的预期 value 是 实数 测量单位 和 那个 测量单位 是 CompositeUnitOfMeasure 的 instance， 然后 有存在 实体 和 那个 实数UANTITY 这样 那个 实体 是 有点 客体 的 instance 和 那个 实体 的 measure 是 那个 实数UANTITY 那个 测量单位 和 那个 实数UANTITY 是 greaterThan 那个 实数 和 1.5 的声明 has 较不可能 的语气
No TPTP formula. May not be expressible in strict first order.	Mid-level-ontology.kif 13576-13585	如果 有点 客体 的预期 value 是 实数 测量单位 和 那个 测量单位 是 CompositeUnitOfMeasure 的 instance， 然后 有存在 实体 和 那个 实数UANTITY 这样 那个 实体 是 有点 客体 的 instance 和 那个 实体 的 measure 是 那个 实数UANTITY 那个 测量单位 和 那个 实数UANTITY 是 lessThan 那个 实数 和 .5 的声明 has 较不可能 的语气
No TPTP formula. May not be expressible in strict first order.	Mid-level-ontology.kif 13504-13513	如果 有点 客体 的 minimum 预期价值是 实数 测量单位 和 那个 测量单位 是 CompositeUnitOfMeasure 的 instance， 然后 有存在 实体 和 那个 实数UANTITY 这样 那个 实体 是 有点 客体 的 instance 和 那个 实体 的 measure 是 那个 实数UANTITY 那个 测量单位 和 那个 实数UANTITY 是 lessThan 那个 实数 的声明 has 较不可能 的语气
No TPTP formula. May not be expressible in strict first order.	Mid-level-ontology.kif 13515-13526	如果 有点 客体 的 minimum 预期价值是 实数 测量单位 和 类 是 NonCompositeUnitOfMeasure 的 subclass 和 那个 测量单位 是 那个 类 的 instance， 然后 有存在 实体， 那个 实数UANTITY， and 和 第三 实体 这样 那个 实体 是 有点 客体 的 instance 和 那个 实体 的 measure 是 那个 实数UANTITY 那个 第三 实体 和 那个 第三 实体 是 那个 类 的 instance 和 那个 实数UANTITY 是 lessThan 那个 实数 的声明 has 较不可能 的语气
No TPTP formula. May not be expressible in strict first order.	Mid-level-ontology.kif 13466-13476	如果 有点 客体 的 minimum 预期半径是 实数 测量单位 和 另一个 客体 是 有点 客体 的 instance 和 球 是 那个 另外 客体 的 attribute， 然后 有存在 那个 实数ADIUS 这样 那个 另外 客体 的 radius 是 那个 实数ADIUS 那个 测量单位 和 那个 实数ADIUS 是 lessThan 那个 实数 的声明 has 较不可能 的语气
No TPTP formula. May not be expressible in strict first order.	Law.kif 295-306	如果 defenseLawyer 法律诉讼 and 有认知的主事 和 另一个 有认知的主事 是在 那个 法律诉讼 的 defendant ， 然后 那个 有认知的主事 desires 不存在 实体 这样 那个 实体 是 法律决定 的 instance 和 那个 实体 提到 那个 法律诉讼 和 那个 另外 有认知的主事 doesn't wants 那个 实体
No TPTP formula. May not be expressible in strict first order.	Communications.kif 202-214	如果 过程 在 客体 结束 和 那个 过程 是 讯息 的 instance 和 实体 是 那个 过程 的 patient 和 那个 客体 是 Telex 的 instance， 然后 有存在 另一个 过程 和 另一个 实体 这样 那个 客体 是导致 那个 另外 过程 的 instrument 和 那个 另外 实体 是 那个 另外 过程 的 result 和 那个 另外 实体 表达 那个 实体 和 那个 另外 实体 是 文本 的 instance 和 那个 过程 出现 的 time 的开始%n在那个 另外 过程 出现 的 time 的开始before发生
No TPTP formula. May not be expressible in strict first order.	ComputingBrands.kif 734-743	如果 deviceOS 有点 客体 and 有点 电脑 和 有点 客体I 是 那个 有点 客体 的 instance 和 有点 电脑I 是 那个 有点 电脑 的 instance 和 manufacturer 那个 有点 客体 and 有认知的主事， 然后 那个 有认知的主事 desires 那个 有点 电脑I 是 第三 实体 的执行 program 和 那个 第三 实体 是 running 在 那个 有点 客体I
No TPTP formula. May not be expressible in strict first order.	Government.kif 4648-4657	如果 地缘政治区域 是 对于 %3 的 diplomatic 类别 和 那个 地缘政治区域 是 国家 的 instance 和 施事体 是 地缘政治区域 的 instance， 然后 有存在 机构 这样 那个 机构 是 另一个 有点 机构 的 instance 和 那个 机构 是 located 在 那个 施事体 和 那个 机构 是 那个 地缘政治区域 的 Government Organization 的一部分
No TPTP formula. May not be expressible in strict first order.	Government.kif 4658-4667	如果 机构 是 对于 %3 的 diplomatic 类别 和 那个 机构 是 机构 的 instance 和 施事体 是 地缘政治区域 的 instance， 然后 有存在 另一个 机构 这样 那个 另外 机构 是 第三 有点 机构 的 instance 和 那个 另外 机构 是 located 在 那个 施事体 和 那个 另外 机构 是 那个 机构 Organization 的一部分
No TPTP formula. May not be expressible in strict first order.	Government.kif 4582-4590
No TPTP formula. May not be expressible in strict first order.	Government.kif 4470-4478	如果 地缘政治区域 是 对于 地位 和 施事体 的外交代表在角色 人类 和 那个 地缘政治区域 是 国家 的 instance， 然后 有存在 机构 这样 那个 机构 是 外交组织 的 instance 和 那个 机构 是 那个 地缘政治区域 的 Government Organization 的一部分 和 那个 人类 在 那个 机构 任职 那个 地位
No TPTP formula. May not be expressible in strict first order.	Transportation.kif 2806-2819	如果 公交专用道 的 distance 是 恒量 和 运输系统 是 那个 公交专用道 在系统里的 path 和 地区 是 那个 公交专用道 的 start 和 另一个 地区 是 那个 公交专用道 的 end 和 那个 运输系统 的 abstract counterpart 是 图路径 ， 然后 有存在 图， 图节点， and 和 另一个 图节点 这样 那个 图 是 那个 图路径 的 subGraph 和 那个 图节点 equal 那个 图路径 的开端 和 那个 另外 图节点 equal 那个 图路径 的末端 和 那个 地区 的 abstract counterpart 是 那个 图节点 和 那个 另外 地区 的 abstract counterpart 是 那个 另外 图节点
No TPTP formula. May not be expressible in strict first order.	FinancialOntology.kif 807-816	如果 货币测量 是 贷款 的 down 费用 和 时点 是 那个 贷款 的 agreement 生效日期， 然后 有存在 金融交易 这样 那个 货币测量 是 那个 金融交易 的 transaction 总额 和 那个 金融交易 的 date 是 那个 时点 和 那个 金融交易 在 那个 贷款 的 currency 结束
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
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