ExtensionFn |
appearance as argument number 1 |
No TPTP formula. May not be expressible in strict first order. | chinese_format.kif 1719-1720 | |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 1764-1765 | |
No TPTP formula. May not be expressible in strict first order. | japanese_format.kif 324-325 | |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 1761-1761 | 延伸函数 的 1 数量 是 属性 的 instance |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 1760-1760 | 延伸函数 是 部分值关系 的 instance |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 1759-1759 | 延伸函数 是 一元函数 的 instance |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 1762-1762 | 延伸函数 的 range 是 类 的实例 |
appearance as argument number 2 |
No TPTP formula. May not be expressible in strict first order. | chinese_format.kif 257-257 | |
No TPTP formula. May not be expressible in strict first order. | english_format.kif 262-262 | |
No TPTP formula. May not be expressible in strict first order. | french_format.kif 147-147 | |
No TPTP formula. May not be expressible in strict first order. | relations-it.txt 106-106 | |
No TPTP formula. May not be expressible in strict first order. | japanese_format.kif 1975-1975 | |
No TPTP formula. May not be expressible in strict first order. | portuguese_format.kif 99-99 | |
No TPTP formula. May not be expressible in strict first order. | relations-de.txt 331-331 | |
No TPTP formula. May not be expressible in strict first order. | relations-ro.kif 166-166 | |
No TPTP formula. May not be expressible in strict first order. | relations-sv.txt 153-153 | |
No TPTP formula. May not be expressible in strict first order. | relations-tg.txt 222-222 | |
No TPTP formula. May not be expressible in strict first order. | chinese_format.kif 258-258 | |
No TPTP formula. May not be expressible in strict first order. | domainEnglishFormat.kif 22990-22990 | |
No TPTP formula. May not be expressible in strict first order. | domainEnglishFormat.kif 22989-22989 | |
No TPTP formula. May not be expressible in strict first order. | domainEnglishFormat.kif 22988-22988 | |
No TPTP formula. May not be expressible in strict first order. | terms-de.txt 105-105 | |
No TPTP formula. May not be expressible in strict first order. | relations-tg.txt 223-223 |
antecedent |
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 1482-1491 | |
No TPTP formula. May not be expressible in strict first order. | Transportation.kif 1289-1296 |
consequent |
No TPTP formula. May not be expressible in strict first order. | Transportation.kif 777-783 | |
No TPTP formula. May not be expressible in strict first order. | Transportation.kif 2389-2391 | |
No TPTP formula. May not be expressible in strict first order. | Transportation.kif 2428-2430 |
statement |
No TPTP formula. May not be expressible in strict first order. | Economy.kif 144-144 | 35 是 和 发达国家 对应的 Class 的 cardinality |
No TPTP formula. May not be expressible in strict first order. | Economy.kif 613-613 | 126 是 和 发展中国家 对应的 Class 的 cardinality |
No TPTP formula. May not be expressible in strict first order. | Economy.kif 405-405 | 42 是 和 最不发达国家 对应的 Class 的 cardinality |
No TPTP formula. May not be expressible in strict first order. | Economy.kif 229-229 | 172 是 和 较未发达国家 对应的 Class 的 cardinality |
No TPTP formula. May not be expressible in strict first order. | Geography.kif 5426-5426 | 流动 的 1 数量 是 和 流体 对应的 Class 的 instance |
No TPTP formula. May not be expressible in strict first order. | Geography.kif 5427-5427 | 流动 的 2 数量 是 和 流体 对应的 Class 的 instance |
No TPTP formula. May not be expressible in strict first order. | Weather.kif 11-11 | 大气层 是 和 流体 对应的 Class 的 subclass |