| appearance as argument number 1 |
|
| No TPTP formula. May not be expressible in strict first order. | chinese_format.kif 2664-2665 | |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 7777-7778 | |
| No TPTP formula. May not be expressible in strict first order. | japanese_format.kif 1384-1385 | |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 7774-7774 | 域 更大, 1 and Object |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 7775-7775 | 域 更大, 2 and Object |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 7769-7769 | 例 更大 and BinaryPredicate |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 7772-7772 | 例 更大 and IrreflexiveRelation |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 7770-7770 | 例 更大 and SpatialRelation |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 7773-7773 | 例 更大 and TotalValuedRelation |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 7771-7771 | 例 更大 and TransitiveRelation |
| appearance as argument number 2 |
|
|
| No TPTP formula. May not be expressible in strict first order. | chinese_format.kif 623-623 | |
| No TPTP formula. May not be expressible in strict first order. | english_format.kif 626-626 | |
| No TPTP formula. May not be expressible in strict first order. | french_format.kif 376-376 | |
| No TPTP formula. May not be expressible in strict first order. | relations-it.txt 160-160 | |
| No TPTP formula. May not be expressible in strict first order. | japanese_format.kif 2110-2110 | |
| No TPTP formula. May not be expressible in strict first order. | portuguese_format.kif 328-328 | |
| No TPTP formula. May not be expressible in strict first order. | relations-cz.txt 385-385 | |
| No TPTP formula. May not be expressible in strict first order. | relations-de.txt 818-818 | |
| No TPTP formula. May not be expressible in strict first order. | relations-hindi.txt 199-199 | |
| No TPTP formula. May not be expressible in strict first order. | relations-ro.kif 398-398 | |
| No TPTP formula. May not be expressible in strict first order. | relations-sv.txt 418-418 | |
| No TPTP formula. May not be expressible in strict first order. | relations-tg.txt 320-320 | |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 7797-7797 | 逆 較小 and 更大 |
| No TPTP formula. May not be expressible in strict first order. | chinese_format.kif 624-624 | |
| No TPTP formula. May not be expressible in strict first order. | domainEnglishFormat.kif 33366-33366 | |
| No TPTP formula. May not be expressible in strict first order. | domainEnglishFormat.kif 33365-33365 | |
| No TPTP formula. May not be expressible in strict first order. | relations-tg.txt 321-321 |
| antecedent |
|
|
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 7780-7788 | 更大 Object and Object RealNumber RealNumber and UnitOfMeasure
|
| consequent |
|
|
| No TPTP formula. May not be expressible in strict first order. | Geography.kif 5330-5335 | |
| No TPTP formula. May not be expressible in strict first order. | Geography.kif 5270-5274 | |
| No TPTP formula. May not be expressible in strict first order. | Geography.kif 5145-5149 | |
| No TPTP formula. May not be expressible in strict first order. | Geography.kif 4523-4528 | |
| No TPTP formula. May not be expressible in strict first order. | Geography.kif 5305-5310 |
|
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