| appearance as argument number 1 |
|
| No TPTP formula. May not be expressible in strict first order. | chinese_format.kif 2263-2266 | |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 5073-5080 | |
| No TPTP formula. May not be expressible in strict first order. | japanese_format.kif 927-931 | |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 5070-5070 | The number 1 argument of 互相 is an instance of real number |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 5069-5069 | 互相 is an instance of total valued relation |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 5067-5067 | 互相 is an instance of unary function |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 5071-5071 | The range of 互相 is an instance of real number |
| appearance as argument number 2 |
|
|
| No TPTP formula. May not be expressible in strict first order. | chinese_format.kif 720-720 | |
| No TPTP formula. May not be expressible in strict first order. | english_format.kif 722-722 | |
| No TPTP formula. May not be expressible in strict first order. | french_format.kif 433-433 | |
| No TPTP formula. May not be expressible in strict first order. | relations-it.txt 244-244 | |
| No TPTP formula. May not be expressible in strict first order. | japanese_format.kif 2150-2150 | |
| No TPTP formula. May not be expressible in strict first order. | portuguese_format.kif 385-385 | |
| No TPTP formula. May not be expressible in strict first order. | relations-de.txt 933-933 | |
| No TPTP formula. May not be expressible in strict first order. | relations-hindi.txt 282-282 | |
| No TPTP formula. May not be expressible in strict first order. | relations-ro.kif 455-455 | |
| No TPTP formula. May not be expressible in strict first order. | relations-sv.txt 493-493 | |
| No TPTP formula. May not be expressible in strict first order. | domainEnglishFormat.kif 48962-48962 | |
| No TPTP formula. May not be expressible in strict first order. | chinese_format.kif 721-721 | |
| No TPTP formula. May not be expressible in strict first order. | domainEnglishFormat.kif 48961-48961 | |
| No TPTP formula. May not be expressible in strict first order. | domainEnglishFormat.kif 48960-48960 |
| consequent |
|
|
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 5086-5091 |
|
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 5082-5084 |
|
|
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