| appearance as argument number 1 |
|
| No TPTP formula. May not be expressible in strict first order. | chinese_format.kif 2241-2242 | |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 4911-4912 | |
| No TPTP formula. May not be expressible in strict first order. | japanese_format.kif 905-906 | |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 4908-4908 | The number 1 argument of imaginary part is an instance of complex number |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 4907-4907 | Imaginary part is an instance of total valued relation |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 4906-4906 | Imaginary part is an instance of unary function |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 4909-4909 | The range of imaginary part is an instance of imaginary number |
| appearance as argument number 2 |
|
|
| No TPTP formula. May not be expressible in strict first order. | chinese_format.kif 702-702 | |
| No TPTP formula. May not be expressible in strict first order. | english_format.kif 704-704 | |
| No TPTP formula. May not be expressible in strict first order. | french_format.kif 424-424 | |
| No TPTP formula. May not be expressible in strict first order. | relations-it.txt 136-136 | |
| No TPTP formula. May not be expressible in strict first order. | japanese_format.kif 2141-2141 | |
| No TPTP formula. May not be expressible in strict first order. | portuguese_format.kif 376-376 | |
| No TPTP formula. May not be expressible in strict first order. | relations-de.txt 915-915 | |
| No TPTP formula. May not be expressible in strict first order. | relations-hindi.txt 175-175 | |
| No TPTP formula. May not be expressible in strict first order. | relations-ro.kif 446-446 | |
| No TPTP formula. May not be expressible in strict first order. | relations-sv.txt 475-475 | |
| No TPTP formula. May not be expressible in strict first order. | relations-tg.txt 276-276 | |
| No TPTP formula. May not be expressible in strict first order. | domainEnglishFormat.kif 29319-29319 | |
| No TPTP formula. May not be expressible in strict first order. | chinese_format.kif 703-703 | |
| No TPTP formula. May not be expressible in strict first order. | domainEnglishFormat.kif 29318-29318 | |
| No TPTP formula. May not be expressible in strict first order. | domainEnglishFormat.kif 29317-29317 | |
| No TPTP formula. May not be expressible in strict first order. | relations-tg.txt 277-277 |
|
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