and

-------------------------


No TPTP formula. May not be expressible in strict first order. Merge.kif 7780-7788 客体 larger 另一个 客体 若且唯若 对所有 实数另一个 实数, and 和 测量单位
No TPTP formula. May not be expressible in strict first order. Transportation.kif 182-189 长度测量 地理区域 的轨道 length 若且唯若 符号串 所描述的类别 的 length那个 长度测量
No TPTP formula. May not be expressible in strict first order. Transportation.kif 712-719 长度测量 地理区域 的原油管线 length 若且唯若 符号串 所描述的类别 的 length那个 长度测量
No TPTP formula. May not be expressible in strict first order. Transportation.kif 210-217 长度测量 地理区域 的双轨规格 length 若且唯若 符号串 所描述的类别 的 length那个 长度测量
No TPTP formula. May not be expressible in strict first order. Transportation.kif 126-133 长度测量 地理区域 的电场轨道 length 若且唯若 符号串 所描述的类别 的 length那个 长度测量
No TPTP formula. May not be expressible in strict first order. Transportation.kif 568-575 长度测量 地理区域 的高速公路系统 length 若且唯若 符号串 所描述的类别 的 length那个 长度测量
No TPTP formula. May not be expressible in strict first order. Transportation.kif 154-161 长度测量 地理区域 的多轨铁路 length 若且唯若 符号串 所描述的类别 的 length那个 长度测量
No TPTP formula. May not be expressible in strict first order. Transportation.kif 237-244 长度测量 地理区域 的短规格铁路的 length 若且唯若 符号串 所描述的类别 的 length那个 长度测量
No TPTP formula. May not be expressible in strict first order. Transportation.kif 735-742 长度测量 地理区域 的 天然瓦斯管线的 length 若且唯若 符号串 所描述的类别 的 length那个 长度测量
No TPTP formula. May not be expressible in strict first order. Transportation.kif 542-549 长度测量 地理区域 的铺设铁路 length 若且唯若 符号串 所描述的类别 的 length那个 长度测量
No TPTP formula. May not be expressible in strict first order. Transportation.kif 758-765 长度测量 地理区域 的石油产品管线 length 若且唯若 符号串 所描述的类别 的 length那个 长度测量
No TPTP formula. May not be expressible in strict first order. Transportation.kif 265-272 长度测量 地理区域 的 标准规格管线 length 若且唯若 符号串 所描述的类别 的 length那个 长度测量
No TPTP formula. May not be expressible in strict first order. Transportation.kif 294-306 长度测量 地理区域 的未分类规格轨道 length 若且唯若 符号串 所描述的类别 的 length那个 长度测量
No TPTP formula. May not be expressible in strict first order. Transportation.kif 601-608 长度测量 地理区域 的未铺设高速公路 length 若且唯若 符号串 所描述的类别 的 length那个 长度测量
No TPTP formula. May not be expressible in strict first order. Economy.kif 1233-1238 地缘政治区域 对于 有点 时距 在周期 实数lowest 平分家庭收入 若且唯若 有存在 时间位置 这样 那个 时间位置 有点 时距instance那个 实数那个 地缘政治区域 lowest 平分家庭收入 在 那个 时间位置 holdsDuring
No TPTP formula. May not be expressible in strict first order. Mid-level-ontology.kif 30284-30298 过程 是以 Harmless 的形式发生 若且唯若 那个 过程 不 是 损坏instance 和 不存在 那个 过程2 这样 那个 过程2 是 损坏instance那个 过程2%n是那个 过程subProcess 和 不存在 那个 过程2 这样 那个 过程2 是 损坏instance那个 过程 causes 那个 过程2
No TPTP formula. May not be expressible in strict first order. Military.kif 1019-1024 地缘政治区域 是 对于 时距 在周期 实数military 部分GDP支出 若且唯若 有存在 时间位置 这样 那个 时间位置那个 时距instance那个 实数那个 地缘政治区域military 部分GDP支出 在 那个 时间位置 holdsDuring
No TPTP formula. May not be expressible in strict first order. Military.kif 980-985 地缘政治区域 是 对于 时距 在周期 货币测量military 美元花费 若且唯若 有存在 时间位置 这样 那个 时间位置那个 时距instance那个 货币测量那个 地缘政治区域military 在美元的花费 在 那个 时间位置 holdsDuring
No TPTP formula. May not be expressible in strict first order. Mid-level-ontology.kif 13849-13856 公式 的声明 has 合法 的语气 若且唯若 不存在 另一个 公式 这样 那个 另外 公式 的声明 has 的语气 和 那个 另外 公式 不 是 那个 公式consistent
No TPTP formula. May not be expressible in strict first order. FinancialOntology.kif 3283-3288 人类monthly income 货币测量 若且唯若 有存在 时距 这样 那个 时距instance那个 人类 对于 那个 时距 income 那个 货币测量
No TPTP formula. May not be expressible in strict first order. Mid-level-ontology.kif 23108-23113 人类nephew 若且唯若 有存在 生物 这样 那个 生物那个 人类sibling那个 人那个 生物son
No TPTP formula. May not be expressible in strict first order. Mid-level-ontology.kif 23122-23127 女人 人类niece 若且唯若 有存在 生物 这样 那个 生物那个 人类sibling那个 女人那个 生物daughter
No TPTP formula. May not be expressible in strict first order. Geography.kif 3653-3657 客体另一个 客体东北 若且唯若 那个 客体那个 另外 客体那个 客体那个 另外 客体
No TPTP formula. May not be expressible in strict first order. Geography.kif 3688-3692 客体另一个 客体西北 若且唯若 那个 客体那个 另外 客体那个 客体那个 另外 客体西方
No TPTP formula. May not be expressible in strict first order. Geography.kif 3664-3668 客体另一个 客体东南 若且唯若 那个 客体那个 另外 客体那个 客体那个 另外 客体

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