| appearance as argument number 1 |
|
| No TPTP formula. May not be expressible in strict first order. | chinese_format.kif 2769-2774 | |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 8643-8650 | |
| No TPTP formula. May not be expressible in strict first order. | japanese_format.kif 1499-1504 | |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 8639-8639 | 域 分, 1 and NonnegativeInteger |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 8640-8640 | 域子類 分, 2 and Hour |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 8637-8637 | 例 分 and BinaryFunction |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 8638-8638 | 例 分 and PartialValuedRelation |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 8636-8636 | 例 分 and TemporalRelation |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 8641-8641 | 範圍子類 分 and Minute |
| appearance as argument number 2 |
|
|
| No TPTP formula. May not be expressible in strict first order. | chinese_format.kif 473-473 | |
| No TPTP formula. May not be expressible in strict first order. | english_format.kif 479-479 | |
| No TPTP formula. May not be expressible in strict first order. | french_format.kif 273-273 | |
| No TPTP formula. May not be expressible in strict first order. | relations-it.txt 191-191 | |
| No TPTP formula. May not be expressible in strict first order. | japanese_format.kif 2063-2063 | |
| No TPTP formula. May not be expressible in strict first order. | portuguese_format.kif 225-225 | |
| No TPTP formula. May not be expressible in strict first order. | relations-cz.txt 279-279 | |
| No TPTP formula. May not be expressible in strict first order. | relations-de.txt 616-616 | |
| No TPTP formula. May not be expressible in strict first order. | relations-hindi.txt 229-229 | |
| No TPTP formula. May not be expressible in strict first order. | relations-ro.kif 294-294 | |
| No TPTP formula. May not be expressible in strict first order. | relations-sv.txt 300-300 | |
| No TPTP formula. May not be expressible in strict first order. | relations-tg.txt 368-368 | |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 9351-9351 | 相關的內部概念 Minute and 分 |
| No TPTP formula. May not be expressible in strict first order. | domainEnglishFormat.kif 37955-37955 | |
| No TPTP formula. May not be expressible in strict first order. | chinese_format.kif 474-474 | |
| No TPTP formula. May not be expressible in strict first order. | domainEnglishFormat.kif 37954-37954 | |
| No TPTP formula. May not be expressible in strict first order. | domainEnglishFormat.kif 37953-37953 | |
| No TPTP formula. May not be expressible in strict first order. | relations-tg.txt 369-369 |
| antecedent |
|
|
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 8656-8661 |
|
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 8652-8654 |
|
| statement |
|
|
| No TPTP formula. May not be expressible in strict first order. | QoSontology.kif 2143-2143 | 等於 unix時代 and 第二 0 and 分 0 and 小時 0 and 天 1 and 月 January and 年 1970 |
|
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