No TPTP formula. May not be expressible in strict first order.	People.kif 1502-1504	道 是 客体 的 attribute 若且唯若 那个 客体 是 道教 的 member
No TPTP formula. May not be expressible in strict first order.	People.kif 1517-1519	拜火教 是 客体 的 attribute 若且唯若 那个 客体 是 拜火教 的 member
No TPTP formula. May not be expressible in strict first order.	Mid-level-ontology.kif 751-762	和弦音乐 是 客体 的 attribute 若且唯若 有存在 过程 和 另一个 过程 这样 那个 客体 是 制作音乐 的 instance 和 那个 过程 是 制作音乐 的 instance 和 那个 另外 过程 是 制作音乐 的 instance 和 那个 过程%n是那个 客体的subProcess 和 那个 另外 过程%n是那个 客体的subProcess 和 那个 过程 不 equal 那个 另外 过程 和 那个 过程 和 那个 客体 同时发生 和 那个 另外 过程 和 那个 客体 同时发生
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.	Geography.kif 4711-4720	公海 是 客体 的 attribute 若且唯若 有存在 物理 和 实数 这样 那个 客体 是 盐水区 的 instance 和 那个 客体 不 是 内陆水域 的 instance 和 那个 物理 和 那个 客体 的 distance 是 那个 实数 海里 和 那个 实数 是 greaterThan 5.0
No TPTP formula. May not be expressible in strict first order.	Mid-level-ontology.kif 30132-30140	Barefoot 是 实体 的 attribute 在 时间位置 holdsDuring 若且唯若 不存在 另一个 实体 这样 那个 另外 实体 是 鞋 的 instance 和 那个 实体 wears 那个 另外 实体 在 那个 时间位置 holdsDuring
No TPTP formula. May not be expressible in strict first order.	Mid-level-ontology.kif 30145-30153	Naked 是 实体 的 attribute 在 时间位置 holdsDuring 若且唯若 不存在 另一个 实体 这样 那个 另外 实体 是 服装 的 instance 和 那个 实体 wears 那个 另外 实体 在 那个 时间位置 holdsDuring
No TPTP formula. May not be expressible in strict first order.	Mid-level-ontology.kif 30223-30236	Alone 是 实体 的 attribute 在 时距 holdsDuring 若且唯若 不存在 那个 实体2 和 过程 这样 那个 实体 不 equal 那个 实体2 和 那个 实体2 是 施事体 的 instance 和 那个 过程 是 社交 的 instance 和 那个 过程 出现 的 time 在 那个 时距 时段内发生 和 那个 实体 是事件 那个 过程 的 involved 和 那个 实体2 是事件 那个 过程 的 involved
No TPTP formula. May not be expressible in strict first order.	Mid-level-ontology.kif 30271-30279	Mute 是 施事体 的 attribute 在 时距 holdsDuring 若且唯若 不存在 过程 这样 那个 过程 是 说话 的 instance 和 那个 过程 出现 的 time 在 那个 时距 时段内发生 和 那个 施事体 是 那个 过程 的 agent
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.	Government.kif 148-152	如果 政体 是 地缘政治区域 的 Government 的 attribute 和 那个 政体 是 政体 的 instance， 然后 %2 是 1% 的 government 类别
No TPTP formula. May not be expressible in strict first order.	Music.kif 478-482	如果 属性 是 客体 的 attribute 和 那个 属性 是 AlbumAttribute 的 instance， 然后 那个 客体 是 Album 的 instance
No TPTP formula. May not be expressible in strict first order.	emotion.kif 374-387	如果 AppraisalAsJustTreatment 是 有认知的主事 的 attribute 和 那个 有认知的主事JT 是 AppraisalProcess 的 instance 和 那个 有认知的主事 是 那个 有认知的主事JT 的 agent， 然后 有存在 另一个 过程 和 那个 有认知的主事2 这样 那个 另外 过程 是 过程 的 instance 和 那个 有认知的主事JT 提到 那个 另外 过程 和 那个 有认知的主事2 是 那个 另外 过程 的 agent 和 那个 有认知的主事 不 equal 那个 有认知的主事2 和 那个 有认知的主事 是 那个 另外 过程 的 patient 和 那个 有认知的主事 wants 那个 另外 过程
No TPTP formula. May not be expressible in strict first order.	emotion.kif 349-363	如果 AppraisalAsUnjustTreatment 是 有认知的主事 的 attribute 和 那个 有认知的主事UJ 是 AppraisalProcess 的 instance 和 那个 有认知的主事 是 那个 有认知的主事UJ 的 agent， 然后 有存在 另一个 过程 和 那个 有认知的主事2 这样 那个 另外 过程 是 过程 的 instance 和 那个 有认知的主事UJ 提到 那个 另外 过程 和 那个 有认知的主事2 是 那个 另外 过程 的 agent 和 那个 有认知的主事 不 equal 那个 有认知的主事2 和 那个 有认知的主事 是 那个 另外 过程 的 patient 和 那个 有认知的主事 doesn't wants 那个 另外 过程
No TPTP formula. May not be expressible in strict first order.	Biography.kif 223-230	如果 Founder 是 施事体 的 attribute 和 那个 施事体 是 人类 的 instance， 然后 有存在 过程 这样 那个 过程 是 创建 的 instance 和 那个 施事体 是 那个 过程 的 agent
No TPTP formula. May not be expressible in strict first order.	ComputingBrands.kif 4373-4382	如果 TwoFactorAuthentication 是 用户帐号 的 attribute 和 loggedInDuring 施事体, 那个 用户帐号 and 时距， 然后 有存在 那个 时距F 这样 那个 时距F 是 TwoFactorLoggingIn 的 instance 和 那个 施事体 是 那个 时距F 的 agent 和 accountUsed 那个 时距F and 那个 用户帐号 和 那个 时距F 出现 的 time 比那个 时距发生的earlier
No TPTP formula. May not be expressible in strict first order.	UXExperimentalTerms.kif 648-652	如果 属性 是 客体 的 attribute 和 那个 属性 是 AccountAttribute 的 instance， 然后 那个 客体 是 用户帐号 的 instance
No TPTP formula. May not be expressible in strict first order.	Biography.kif 757-776	如果 配音演员 是 施事体 的 attribute 和 过程 是 戏剧表演 的 instance 和 那个 施事体 是 那个 过程 的 agent 和 另一个 过程 是 语言交流 的 instance 和 那个 施事体 是 那个 另外 过程 的 agent 和 那个 另外 过程%n是那个 过程的subProcess， 然后 不存在 第三 过程 和 另一个 施事体 这样 那个 第三 过程 是 看 的 instance 和 那个 施事体 是 那个 第三 过程 的 patient 和 那个 另外 施事体 是 那个 第三 过程 的 agent 和 有存在 第四 过程 和 那个 另外 施事体 这样 那个 第四 过程 是 听 的 instance 和 那个 施事体 是 那个 第四 过程 的 patient 和 那个 另外 施事体 是 那个 第四 过程 的 agent
No TPTP formula. May not be expressible in strict first order.	Government.kif 1774-1779	如果 机构 的 member 是 客体 的 attribute 和 那个 客体 是 施事体 的 instance 和 那个 机构 是 机构 的 instance， 然后 那个 客体 是 那个 机构 的 member
No TPTP formula. May not be expressible in strict first order.	Economy.kif 865-869	如果 共产主义国家 是 施事体 的 attribute 和 那个 施事体 是 国家 的 instance， 然后 中央计划经济 是 那个 施事体 的 economy 类别
No TPTP formula. May not be expressible in strict first order.	Geography.kif 1754-1759	如果 平坦的地形 是 客体 的 attribute 和 土地面积 是 那个 客体 的 part 和 非负实数 是 那个 土地面积 的 slope 梯度， 然后 0.005 是 greaterThan 那个 非负实数
No TPTP formula. May not be expressible in strict first order.	Economy.kif 506-510	如果 高收入国家 是 施事体 的 attribute 和 那个 施事体 不 是 石油输出国组织 的 member， 然后 发达国家 是 那个 施事体 的 economy 类别
No TPTP formula. May not be expressible in strict first order.	Geography.kif 1766-1771	如果 低地形 是 客体 的 attribute 和 土地面积 是 那个 客体 的 part 和 非负实数 是 那个 土地面积 的 slope 梯度， 然后 0.03 是 greaterThan 那个 非负实数
No TPTP formula. May not be expressible in strict first order.	Sports.kif 1363-1370	如果 属性 是 施事体 的 attribute 和 那个 属性 是 ProfessionalAthlete 的 instance， 然后 有存在 比赛 这样 那个 比赛 是 运动 的 instance 和 那个 施事体 participates 在 那个 比赛
No TPTP formula. May not be expressible in strict first order.	Sports.kif 1357-1361	如果 属性 是 施事体 的 attribute 和 那个 属性 是 ProfessionalAthlete 的 instance， 然后 那个 施事体 hasSkill 去做 运动
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