| appearance as argument number 1 |
|
| No TPTP formula. May not be expressible in strict first order. | chinese_format.kif 3841-3845 | |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 17254-17259 | |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 17251-17251 | 域 相對時間, 1 and TimePosition |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 17252-17252 | 域 相對時間, 2 and TimeZone |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 17248-17248 | 例 相對時間 and BinaryFunction |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 17249-17249 | 例 相對時間 and TemporalRelation |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 17250-17250 | 例 相對時間 and TotalValuedRelation |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 17253-17253 | 範圍 相對時間 and TimePosition |
| appearance as argument number 2 |
|
|
| No TPTP formula. May not be expressible in strict first order. | chinese_format.kif 596-596 | |
| No TPTP formula. May not be expressible in strict first order. | english_format.kif 599-599 | |
| No TPTP formula. May not be expressible in strict first order. | french_format.kif 358-358 | |
| No TPTP formula. May not be expressible in strict first order. | relations-it.txt 251-251 | |
| No TPTP formula. May not be expressible in strict first order. | japanese_format.kif 2101-2101 | |
| No TPTP formula. May not be expressible in strict first order. | portuguese_format.kif 310-310 | |
| No TPTP formula. May not be expressible in strict first order. | relations-de.txt 782-782 | |
| No TPTP formula. May not be expressible in strict first order. | relations-ro.kif 380-380 | |
| No TPTP formula. May not be expressible in strict first order. | relations-sv.txt 399-399 | |
| No TPTP formula. May not be expressible in strict first order. | domainEnglishFormat.kif 49346-49346 | |
| No TPTP formula. May not be expressible in strict first order. | chinese_format.kif 597-597 | |
| No TPTP formula. May not be expressible in strict first order. | domainEnglishFormat.kif 49345-49345 | |
| No TPTP formula. May not be expressible in strict first order. | domainEnglishFormat.kif 49344-49344 |
| antecedent |
|
|
|
Show full definition with tree view
Show simplified definition (without tree view)
Show simplified definition (with tree view)
|
|
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