and |
![]() |
No TPTP formula. May not be expressible in strict first order. | Geography.kif 3676-3680 | 客体 在 另一个 客体 的 西南 若且唯若 那个 客体 在 那个 另外 客体 的 南 和 那个 客体 在 那个 另外 客体 的 西方 |
No TPTP formula. May not be expressible in strict first order. | Economy.kif 1042-1047 | 地缘政治区域 是 对于 时距 在周期 货币测量 的 per 人头 GDP 若且唯若 有存在 时间位置 这样 那个 时间位置 是 那个 时距 的 instance 和 那个 货币测量 是 那个 地缘政治区域 的 per 人头 GDP 在 那个 时间位置 holdsDuring |
No TPTP formula. May not be expressible in strict first order. | Economy.kif 1184-1189 | 地缘政治区域 对于 有点 时距 在周期 实数 在贫困标准下的 population 部分 若且唯若 有存在 时间位置 这样 那个 时间位置 是 有点 时距 的 instance 和 那个 实数 是 那个 地缘政治区域 在贫困标准下的 population 部分 在 那个 时间位置 holdsDuring |
No TPTP formula. May not be expressible in strict first order. | Mid-level-ontology.kif 13207-13212 | 客体 是 另一个 客体 的 quarter 若且唯若 有存在 第三 客体 这样 那个 第三 客体 是 那个 另外 客体 的 half 和 那个 客体 是 那个 第三 客体 的 half |
No TPTP formula. May not be expressible in strict first order. | Economy.kif 1007-1012 | 地缘政治区域 是 对于 %3 在周期 %2 的 real GDP 的成长速率 若且唯若 有存在 时间位置 这样 那个 时间位置 是 有点 时距 的 instance 和 实数 是 那个 地缘政治区域 的 real GDP 成长速率 在 那个 时间位置 holdsDuring |
No TPTP formula. May not be expressible in strict first order. | Economy.kif 1086-1091 | 地缘政治区域 是 对于 实数 和 有点 时距 在 周期 行业属性 的 GDP sector 组成 若且唯若 有存在 时间位置 这样 那个 时间位置 是 有点 时距 的 instance 和 那个 地缘政治区域 是 对于 那个 实数 的 GDP 那个 行业属性 sector 组成 在 那个 时间位置 holdsDuring |
No TPTP formula. May not be expressible in strict first order. | Economy.kif 1129-1137 | 地缘政治区域 是 实数 测量单位 和 有点 时距 在 周期 行业属性 的 sector GDP 价值 若且唯若 有存在 时间位置 这样 那个 时间位置 是 有点 时距 的 instance 和 那个 地缘政治区域 是 对于 那个 实数 那个 测量单位 的 sector GDP 价值 那个 行业属性 在 那个 时间位置 holdsDuring |
No TPTP formula. May not be expressible in strict first order. | Mid-level-ontology.kif 23151-23158 | 人 是 人类 的 stepfather 若且唯若 有存在 另一个 人类 这样 那个 另外 人类 是 那个 人类 的 mother 和 那个 人 是 那个 另外 人类 的 spouse 和 那个 人 不 是 那个 人类 father |
No TPTP formula. May not be expressible in strict first order. | Mid-level-ontology.kif 23168-23175 | 女人 是 人类 的 stepfather 若且唯若 有存在 另一个 人类 这样 那个 另外 人类 是 那个 人类 father 和 那个 女人 是 那个 另外 人类 的 spouse 和 那个 女人 不 是 那个 人类 的 mother |
No TPTP formula. May not be expressible in strict first order. | Transportation.kif 1277-1287 | 地理区域 是 对于 非负整数 在地区 和 机场有着铺设跑道 对应的 Class 的 total 设施类别 若且唯若 有存在 符号串 和 实体 这样 那个 非负整数 是 那个 符号串 所描述的类别 的 cardinality |
No TPTP formula. May not be expressible in strict first order. | Transportation.kif 1221-1228 | 地理区域 是 对于 非负整数 在地区 类 的 total 设施类别 若且唯若 那个 非负整数 是 符号串 所描述的类别 的 cardinality |
No TPTP formula. May not be expressible in strict first order. | Economy.kif 958-963 | 地缘政治区域 是 对于 有点 时距 在 周期 货币测量 的 totalGDP 若且唯若 有存在 时间位置 这样 那个 时间位置 是 有点 时距 的 instance 和 那个 货币测量 是 那个 地缘政治区域 的 total GDP 在 那个 时间位置 holdsDuring |
No TPTP formula. May not be expressible in strict first order. | Transportation.kif 484-491 | 长度测量 是 地理区域 的 total 高速公路系统长度 若且唯若 符号串 所描述的类别 的 length 是 那个 长度测量 |
No TPTP formula. May not be expressible in strict first order. | Transportation.kif 98-105 | 长度测量 是 地理区域 的 total 铁路系统长度 若且唯若 符号串 所描述的类别 的 length 是 那个 长度测量 |
No TPTP formula. May not be expressible in strict first order. | Transportation.kif 656-663 | 长度测量 是 地理区域 的 total 水路长路 若且唯若 符号串 所描述的类别 的 length 是 那个 长度测量 |
No TPTP formula. May not be expressible in strict first order. | Transportation.kif 685-692 | 长度测量 是 在地区 地理区域 的 total 管线 若且唯若 符号串 所描述的类别 的 length 是 那个 长度测量 |
No TPTP formula. May not be expressible in strict first order. | Mid-level-ontology.kif 23136-23141 | 人类 的 uncle 是 人 若且唯若 有存在 另一个 人类 这样 那个 人 是 那个 另外 人类 的 brother 和 那个 另外 人类 是 那个 人类 的 parent |
No TPTP formula. May not be expressible in strict first order. | Economy.kif 1456-1461 | 地缘政治区域 是 对于 有点 时距 在周期 实数 地区的 unemployment 比例 若且唯若 有存在 时间位置 这样 那个 时间位置 是 有点 时距 的 instance 和 那个 地缘政治区域 是 对于 在地区 那个 实数 的 unemployment 比例 在 那个 时间位置 holdsDuring |
No TPTP formula. May not be expressible in strict first order. | Mid-level-ontology.kif 968-975 | 整数 是 机构 的 year 资金 若且唯若 有存在 过程 和 那个 整数EAR 这样 那个 整数EAR 时段 和 那个 过程 出现 的 time 重叠 和 那个 整数EAR 是 那个 整数 year 的 instance 和 那个 过程 是 创建 的 instance 和 那个 机构 是 那个 过程 的 result |
No TPTP formula. May not be expressible in strict first order. | UXExperimentalTerms.kif 632-640 |
|
No TPTP formula. May not be expressible in strict first order. | Mid-level-ontology.kif 20751-20757 | |
No TPTP formula. May not be expressible in strict first order. | Hotel.kif 599-604 | |
No TPTP formula. May not be expressible in strict first order. | Hotel.kif 939-944 | |
No TPTP formula. May not be expressible in strict first order. | UXExperimentalTerms.kif 193-199 |
|
No TPTP formula. May not be expressible in strict first order. | Government.kif 706-713 | |
Display limited to 25 items. Show next 25 | ||
Display limited to 25 items. Show next 25 |
![]() |