No TPTP formula. May not be expressible in strict first order.	Cars.kif 3117-3133	如果 coilCount WireCoil and 整数， 然后 有存在 群体 这样 那个 群体 是 群体 的 instance 和 那个 整数 是 那个 群体 的 member 计数 和 对所有 客体 如果 那个 客体 是 那个 群体 的 member， 然后 封闭的二维图 是 那个 客体 的 attribute 和 那个 客体 是 那个 WireCoil 的 part 和 不存在 那个 客体2 这样 那个 客体2 和 那个 客体 重叠 和 那个 客体2 是 那个 群体 的 member
No TPTP formula. May not be expressible in strict first order.	Merge.kif 10039-10044	如果 客体 完全 fills 洞， 然后 对所有 另一个 客体 如果 那个 另外 客体 和 那个 洞 是 connected， 然后 那个 另外 客体 和 那个 客体 是 connected
No TPTP formula. May not be expressible in strict first order.	Merge.kif 3855-3860	如果 客体 是和 另一个 客体 完全相同的 copy， 然后 对所有 属性 如果 那个 属性 是 那个 客体 的 attribute， 然后 那个 属性 是 那个 另外 客体 的 attribute
No TPTP formula. May not be expressible in strict first order.	Music.kif 243-249	如果 人类 有 discography Discography ， 然后 对所有 音乐录音 如果 那个 音乐录音 是 那个 Discography 的 member， 然后 有存在 有点 制作音乐 这样 那个 人类 表演了 那个 音乐录音
No TPTP formula. May not be expressible in strict first order.	Merge.kif 2950-2955	如果 类 分拆成不相交的 @ROW， 然后 对所有 第三 类 如果 那个 第三 类 是 (@ROW) 的 member， 然后 那个 第三 类 是 那个 类 的 subclass
No TPTP formula. May not be expressible in strict first order.	Merge.kif 2957-2966	如果 类 分拆成不相交的 @ROW， 然后 对所有 第三 类 和 第四 类 如果 那个 第三 类 是 (@ROW) 的 member 和 那个 第四 类 是 (@ROW) 的 member 和 那个 第三 类 不 equal 那个 第四 类， 然后 那个 第三 类 和 % 2 是 disjoint
No TPTP formula. May not be expressible in strict first order.	Dining.kif 492-505	如果 施事体 要求顾客去穿 AmbienceAttribute ， 然后 有存在 实体 和 另一个 实体 这样 那个 实体 是 Outfit 的 instance 和 那个 施事体 believes 那个 实体 是 那个 AmbienceAttribute 和 对所有 第三 实体 和 第四 实体 那个 施事体 是 那个 第三 实体 的 customer 和 那个 第三 实体 对于 那个 施事体 在时间 那个 另外 实体 located 和 那个 第四 实体 是 那个 实体 的 member 和 那个 第三 实体 wears 那个 第四 实体 在 那个 另外 实体 holdsDuring 的声明 has 义务 的语气
No TPTP formula. May not be expressible in strict first order.	Merge.kif 7998-8005	如果 时距 的开始 equal 时点， 然后 对所有 另一个 时点 如果 那个 另外 时点 时段 是 那个 时距 时段 的一 part 和 那个 另外 时点 不 equal 那个 时点， 然后 那个 时点%n在那个 另外 时点before发生
No TPTP formula. May not be expressible in strict first order.	Merge.kif 8016-8023	如果 时距 的结束 equal 时点， 然后 对所有 另一个 时点 如果 那个 另外 时点 时段 是 那个 时距 时段 的一 part 和 那个 另外 时点 不 equal 那个 时点， 然后 那个 另外 时点%n在那个 时点before发生
No TPTP formula. May not be expressible in strict first order.	Merge.kif 16291-16299	如果 人类 的 immediate 家庭 equal 家族群组， 然后 对所有 生物 如果 那个 生物 是 那个 家族群组 的 member， 然后 有存在 另一个 生物 这样 那个 另外 生物 是 那个 生物 的 parent 或 那个 生物 是 那个 另外 生物 的 parent
No TPTP formula. May not be expressible in strict first order.	Merge.kif 6091-6097	如果 把 图 分成另外两个图的最短路径 Set equal 有点 图路径， 然后 有存在 正整数 这样 对所有 另一个 图路径 如果 那个 另外 图路径 是 有点 图路径 的 instance， 然后 那个 另外 图路径 的 length 是 那个 正整数
No TPTP formula. May not be expressible in strict first order.	Merge.kif 9447-9457	如果 分拆 时距 为 的 那个 时距TYPE equal 第三 有点 时距， 然后 对所有 时间位置 如果 那个 时间位置 是 时点 的 instance 和 那个 时间位置 时段 是 那个 时距 时段 的一 part， 然后 有存在 另一个 时间位置 这样 那个 另外 时间位置 是 第三 有点 时距 的 instance 和 那个 时间位置 时段 是 那个 另外 时间位置 时段 的一 part
No TPTP formula. May not be expressible in strict first order.	Merge.kif 9395-9407	如果 分拆 时距 为 的 那个 时距TYPE equal 第三 有点 时距， 然后 对所有 第四 时距 和 第五 时距 如果 那个 第四 时距 是 第三 有点 时距 的 instance 和 那个 第五 时距 是 那个 第三 有点 时距 的 instance 和 那个 第四 时距 不 equal 那个 第五 时距， 然后 那个 第四 时距 接着 那个 第五 时距 或 那个 第五 时距 接着 那个 第四 时距 或 那个 第四 时距 比那个 第五 时距发生的earlier 或 那个 第五 时距 比那个 第四 时距发生的earlier
No TPTP formula. May not be expressible in strict first order.	Merge.kif 9383-9393	如果 分拆 时距 为 的 那个 时距TYPE equal 第三 有点 时距， 然后 对所有 第四 时距 和 第五 时距 如果 那个 第四 时距 是 那个 时距TYPE 的 instance 和 那个 第五 时距 是 第三 有点 时距 的 instance， 然后 有存在 持续时间 这样 那个 第四 时距 的 duration 是 那个 持续时间 和 那个 第五 时距 的 duration 是 那个 持续时间
No TPTP formula. May not be expressible in strict first order.	Merge.kif 9423-9433	如果 分拆 时距 为 的 那个 时距TYPE equal 第三 有点 时距， 然后 对所有 第四 时距 如果 那个 第四 时距 是 第三 有点 时距 的 instance 和 那个 第四 时距 不 finishes了才到 那个 时距， 然后 有存在 第五 时距 这样 那个 第五 时距 是 那个 第三 有点 时距 的 instance 和 那个 第四 时距 接着 那个 第五 时距
No TPTP formula. May not be expressible in strict first order.	Merge.kif 9435-9445	如果 分拆 时距 为 的 那个 时距TYPE equal 第三 有点 时距， 然后 对所有 第四 时距 如果 那个 第四 时距 是 第三 有点 时距 的 instance 和 那个 第四 时距 不 starts了才到 那个 时距 ， 然后 有存在 第五 时距 这样 那个 第五 时距 是 那个 第三 有点 时距 的 instance 和 那个 第五 时距 接着 那个 第四 时距
No TPTP formula. May not be expressible in strict first order.	Merge.kif 267-272	如果 属性 equal 另一个 属性， 然后 对所有 实体 那个 实体 有 那个 属性 的 attribute 若且唯若 那个 实体 有 那个 另外 属性 的 attribute
No TPTP formula. May not be expressible in strict first order.	Merge.kif 281-286	如果 类 equal 另一个 类， 然后 对所有 实体 那个 实体 是 那个 类 的 instance 若且唯若 那个 实体 是 那个 另外 类 的 instance
No TPTP formula. May not be expressible in strict first order.	Merge.kif 9837-9846	如果 客体 equal 包括 另一个 客体 和 第三 客体 差异的部分， 然后 对所有 第四 客体 那个 第四 客体 是 那个 客体 的 properPart 若且唯若 那个 第四 客体 是 那个 另外 客体 的 properPart 和 那个 第四 客体 不 是 那个 第三 客体 的 properPart
No TPTP formula. May not be expressible in strict first order.	Merge.kif 9817-9824	如果 客体 equal 包括 另一个 客体 和 第三 客体 相交的部分， 然后 对所有 第四 客体 那个 第四 客体 是 那个 客体 的 part 若且唯若 那个 第四 客体 是 那个 另外 客体 的 part 和 那个 第四 客体 是 那个 第三 客体 的 part
No TPTP formula. May not be expressible in strict first order.	Merge.kif 9796-9803	如果 客体 equal 包括属于 另一个 客体 或 第三 客体 的部分， 然后 对所有 第四 客体 那个 第四 客体 是 那个 客体 的 part 若且唯若 那个 第四 客体 是 那个 第三 客体 的 part 或 那个 第四 客体 是 那个 另外 客体 的 part
No TPTP formula. May not be expressible in strict first order.	Merge.kif 260-265	如果 实体 equal 另一个 实体， 然后 对所有 属性 那个 实体 有 那个 属性 的 attribute 若且唯若 那个 另外 实体 有 那个 属性 的 attribute
No TPTP formula. May not be expressible in strict first order.	Merge.kif 274-279	如果 实体 equal 另一个 实体， 然后 对所有 类 那个 实体 是 那个 类 的 instance 若且唯若 那个 另外 实体 是 那个 类 的 instance
No TPTP formula. May not be expressible in strict first order.	Merge.kif 4127-4132	如果 过程 是 located 在 客体 ， 然后 对所有 另一个 过程 如果 那个 另外 过程%n是那个 过程的subProcess， 然后 那个 另外 过程 是 located 在 那个 客体
No TPTP formula. May not be expressible in strict first order.	Merge.kif 509-517	如果 @ROW 是所有的 另一个 有点 属性 的 attributes ， 然后 对所有 实体 如果 那个 实体 是 另一个 有点 属性 的 instance， 然后 有存在 另一个 实体 这样 那个 另外 实体 是 (@ROW) 的 member 和 那个 实体 equal 那个 另外 实体
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