PlanetEarth
|
|
appearance as argument number 1 |
No TPTP formula. May not be expressible in strict first order. | Geography.kif 3406-3406 | 行星地球 是 行星 的 instance |
No TPTP formula. May not be expressible in strict first order. | Geography.kif 3407-3407 | 太阳 是 行星地球 的 orbits |
appearance as argument number 2 |
No TPTP formula. May not be expressible in strict first order. | Geography.kif 3399-3399 | 行星地球 是 地球月亮 的 orbits |
No TPTP formula. May not be expressible in strict first order. | domainEnglishFormat.kif 46038-46038 | |
No TPTP formula. May not be expressible in strict first order. | domainEnglishFormat.kif 46037-46037 | |
No TPTP formula. May not be expressible in strict first order. | domainEnglishFormat.kif 46036-46036 |
antecedent |
No TPTP formula. May not be expressible in strict first order. | MilitaryDevices.kif 1462-1467 | 飞机 的 altitude 是 自身连接物体 和 那个 自身连接物体 是 行星地球 的 surface 和 那个 飞机 是 飞机 的 instance 若且唯若 高度测量 是 absolute 那个 飞机 的高度 |
No TPTP formula. May not be expressible in strict first order. | MilitaryDevices.kif 1488-1496 | |
No TPTP formula. May not be expressible in strict first order. | Geography.kif 3999-4010 |
consequent |
No TPTP formula. May not be expressible in strict first order. | Geography.kif 2781-2786 | 客体 是 长度测量 above 地表 若且唯若 有存在 自身连接物体 这样 那个 客体 的 altitude 是 那个 自身连接物体 和 那个 自身连接物体 是 行星地球 的 surface |
No TPTP formula. May not be expressible in strict first order. | Geography.kif 1907-1912 | |
No TPTP formula. May not be expressible in strict first order. | MilitaryDevices.kif 1441-1451 | |
No TPTP formula. May not be expressible in strict first order. | Geography.kif 3515-3517 | |
No TPTP formula. May not be expressible in strict first order. | Geography.kif 3468-3470 | |
No TPTP formula. May not be expressible in strict first order. | Geography.kif 3429-3433 | |
No TPTP formula. May not be expressible in strict first order. | Geography.kif 3991-3997 |