TimePoint(时点) |
appearance as argument number 1 |
No TPTP formula. May not be expressible in strict first order. | chinese_format.kif 1787-1789 | |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 2093-2098 | |
No TPTP formula. May not be expressible in strict first order. | japanese_format.kif 402-405 | |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 2091-2091 | 时点 是 时间位置 的 subclass |
appearance as argument number 2 |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 7882-7882 | 负无穷大 是 时点 的 instance |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 7864-7864 | 正无穷大 是 时点 的 instance |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 7983-7983 | 开始函数 的 range 是 时点 的实例 |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 8011-8011 | 结束函数 的 range 是 时点 的实例 |
No TPTP formula. May not be expressible in strict first order. | QoSontology.kif 2135-2135 | 时代 是 时点 的 subclass |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 8780-8780 | Midnight 是 时点 的 subclass |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 8854-8854 | Noon 是 时点 的 subclass |
No TPTP formula. May not be expressible in strict first order. | chinese_format.kif 881-881 | |
No TPTP formula. May not be expressible in strict first order. | english_format.kif 964-964 | |
No TPTP formula. May not be expressible in strict first order. | french_format.kif 557-557 | |
No TPTP formula. May not be expressible in strict first order. | terms-hindi.txt 87-87 | |
No TPTP formula. May not be expressible in strict first order. | terms-it.txt 90-90 | |
No TPTP formula. May not be expressible in strict first order. | japanese_format.kif 2242-2242 | |
No TPTP formula. May not be expressible in strict first order. | portuguese_format.kif 509-509 | |
No TPTP formula. May not be expressible in strict first order. | terms-cb.txt 92-92 | |
No TPTP formula. May not be expressible in strict first order. | terms-cz.txt 124-124 | |
No TPTP formula. May not be expressible in strict first order. | relations-ro.kif 578-578 | |
No TPTP formula. May not be expressible in strict first order. | terms-tg.txt 91-91 |
appearance as argument number 3 |
No TPTP formula. May not be expressible in strict first order. | UXExperimentalTerms.kif 1022-1022 | SellersOtherItemsFn 的 4 数量 是 时点 的 instance |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 8411-8411 | 时段函数 的 1 数量 是 时点 的 instance |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 8412-8412 | 时段函数 的 2 数量 是 时点 的 instance |
No TPTP formula. May not be expressible in strict first order. | Mid-level-ontology.kif 14036-14036 | TimePeriodFn 的 1 数量 是 时点 的 instance |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 4223-4223 | 表示位置的函数 的 2 数量 是 时点 的 instance |
No TPTP formula. May not be expressible in strict first order. | Mid-level-ontology.kif 14025-14025 | 协议生效日期 的 2 数量 是 时点 的 instance |
No TPTP formula. May not be expressible in strict first order. | Mid-level-ontology.kif 14050-14050 | 截止日期 的 2 数量 是 时点 的 instance |
No TPTP formula. May not be expressible in strict first order. | Music.kif 259-259 | albumRelease 的 2 数量 是 时点 的 instance |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 8101-8101 | 之前 的 1 数量 是 时点 的 instance |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 8102-8102 | 之前 的 2 数量 是 时点 的 instance |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 8139-8139 | 之前或同时 的 1 数量 是 时点 的 instance |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 8140-8140 | 之前或同时 的 2 数量 是 时点 的 instance |
No TPTP formula. May not be expressible in strict first order. | Hotel.kif 682-682 | checkOutTime 的 2 数量 是 时点 的 instance |
No TPTP formula. May not be expressible in strict first order. | Mid-level-ontology.kif 30689-30689 | firstInstanceCreated 的 2 数量 是 时点 的 instance |
No TPTP formula. May not be expressible in strict first order. | Music.kif 94-94 | producedOn 的 2 数量 是 时点 的 instance |
No TPTP formula. May not be expressible in strict first order. | Music.kif 1480-1480 | releaseForConsumption 的 3 数量 是 时点 的 instance |
No TPTP formula. May not be expressible in strict first order. | Dining.kif 708-708 | reservationEnd 的 1 数量 是 时点 的 instance |
No TPTP formula. May not be expressible in strict first order. | Dining.kif 701-701 | reservationStart 的 1 数量 是 时点 的 instance |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 8161-8161 | 在两个时间之间 的 1 数量 是 时点 的 instance |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 8162-8162 | 在两个时间之间 的 2 数量 是 时点 的 instance |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 8163-8163 | 在两个时间之间 的 3 数量 是 时点 的 instance |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 8185-8185 | 在两个时间之间或同时 的 1 数量 是 时点 的 instance |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 8186-8186 | 在两个时间之间或同时 的 2 数量 是 时点 的 instance |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 8187-8187 | 在两个时间之间或同时 的 3 数量 是 时点 的 instance |
No TPTP formula. May not be expressible in strict first order. | Hotel.kif 665-665 | checkInTime 的 2 数量 是 时点 的 subclass |
Display limited to 25 items. Show next 25 | ||
Display limited to 25 items. Show next 25 |
antecedent |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 8281-8288 | |
No TPTP formula. May not be expressible in strict first order. | UXExperimentalTerms.kif 1033-1060 |
|
No TPTP formula. May not be expressible in strict first order. | Weather.kif 1598-1608 | |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 7887-7891 | |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 7893-7898 | |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 7869-7873 | |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 7875-7880 | |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 8420-8428 | |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 8430-8439 | |
No TPTP formula. May not be expressible in strict first order. | Mid-level-ontology.kif 14040-14046 | |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 7524-7528 | |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 8206-8210 | |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 7940-7945 |
|
consequent |
No TPTP formula. May not be expressible in strict first order. | Mid-level-ontology.kif 30030-30060 |
|
No TPTP formula. May not be expressible in strict first order. | Merge.kif 9447-9457 | |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 7947-7952 |
|
No TPTP formula. May not be expressible in strict first order. | Merge.kif 8110-8122 | |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 8212-8221 |