| appearance as argument number 1 |
|
| No TPTP formula. May not be expressible in strict first order. | chinese_format.kif 2832-2833 | |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 9639-9641 | |
| No TPTP formula. May not be expressible in strict first order. | japanese_format.kif 1576-1577 | |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 9643-9643 | 域 部分重疊, 1 and Object |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 9644-9644 | 域 部分重疊, 2 and Object |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 9631-9631 | 例 部分重疊 and BinaryPredicate |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 9634-9634 | 例 部分重疊 and IrreflexiveRelation |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 9633-9633 | 例 部分重疊 and PartialValuedRelation |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 9632-9632 | 例 部分重疊 and SymmetricRelation |
| appearance as argument number 2 |
|
|
| No TPTP formula. May not be expressible in strict first order. | chinese_format.kif 369-369 | |
| No TPTP formula. May not be expressible in strict first order. | english_format.kif 370-370 | |
| No TPTP formula. May not be expressible in strict first order. | french_format.kif 213-213 | |
| No TPTP formula. May not be expressible in strict first order. | relations-it.txt 206-206 | |
| No TPTP formula. May not be expressible in strict first order. | japanese_format.kif 2019-2019 | |
| No TPTP formula. May not be expressible in strict first order. | portuguese_format.kif 165-165 | |
| No TPTP formula. May not be expressible in strict first order. | relations-cz.txt 220-220 | |
| No TPTP formula. May not be expressible in strict first order. | relations-de.txt 492-492 | |
| No TPTP formula. May not be expressible in strict first order. | relations-hindi.txt 244-244 | |
| No TPTP formula. May not be expressible in strict first order. | relations-ro.kif 233-233 | |
| No TPTP formula. May not be expressible in strict first order. | relations-sv.txt 230-230 | |
| No TPTP formula. May not be expressible in strict first order. | relations-tg.txt 394-394 | |
| No TPTP formula. May not be expressible in strict first order. | chinese_format.kif 370-370 | |
| No TPTP formula. May not be expressible in strict first order. | domainEnglishFormat.kif 43775-43775 | |
| No TPTP formula. May not be expressible in strict first order. | domainEnglishFormat.kif 43774-43774 | |
| No TPTP formula. May not be expressible in strict first order. | relations-tg.txt 395-395 |
| antecedent |
|
|
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 9646-9654 | |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 9665-9667 |
| consequent |
|
|
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 9656-9663 |
|
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