| appearance as argument number 1 |
|
| No TPTP formula. May not be expressible in strict first order. | chinese_format.kif 2880-2884 | |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 10026-10033 | |
| No TPTP formula. May not be expressible in strict first order. | japanese_format.kif 1628-1632 | |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 10023-10023 | 例 完全填滿 and AsymmetricRelation |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 10024-10024 | 子關係 完全填滿 and 部分填補 |
| appearance as argument number 2 |
|
|
| No TPTP formula. May not be expressible in strict first order. | chinese_format.kif 381-381 | |
| No TPTP formula. May not be expressible in strict first order. | english_format.kif 387-387 | |
| No TPTP formula. May not be expressible in strict first order. | french_format.kif 219-219 | |
| No TPTP formula. May not be expressible in strict first order. | relations-it.txt 47-47 | |
| No TPTP formula. May not be expressible in strict first order. | japanese_format.kif 2025-2025 | |
| No TPTP formula. May not be expressible in strict first order. | portuguese_format.kif 171-171 | |
| No TPTP formula. May not be expressible in strict first order. | relations-cb.txt 81-81 | |
| No TPTP formula. May not be expressible in strict first order. | relations-cz.txt 226-226 | |
| No TPTP formula. May not be expressible in strict first order. | relations-de.txt 510-510 | |
| No TPTP formula. May not be expressible in strict first order. | relations-hindi.txt 89-89 | |
| No TPTP formula. May not be expressible in strict first order. | relations-ro.kif 239-239 | |
| No TPTP formula. May not be expressible in strict first order. | relations-sv.txt 236-236 | |
| No TPTP formula. May not be expressible in strict first order. | relations-tg.txt 110-110 | |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 10043-10043 | 子關係 填充 and 完全填滿 |
| No TPTP formula. May not be expressible in strict first order. | chinese_format.kif 382-382 | |
| No TPTP formula. May not be expressible in strict first order. | domainEnglishFormat.kif 16176-16176 | |
| No TPTP formula. May not be expressible in strict first order. | domainEnglishFormat.kif 16175-16175 | |
| No TPTP formula. May not be expressible in strict first order. | domainEnglishFormat.kif 16174-16174 | |
| No TPTP formula. May not be expressible in strict first order. | relations-tg.txt 111-111 |
| antecedent |
|
|
| No TPTP formula. May not be expressible in strict first order. | Mid-level-ontology.kif 25935-25948 |
|
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 10035-10040 |
|
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 10061-10066 |
|
| consequent |
|
|
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 10074-10078 |
|
| No TPTP formula. May not be expressible in strict first order. | Mid-level-ontology.kif 25965-25974 | |
| No TPTP formula. May not be expressible in strict first order. | Mid-level-ontology.kif 3663-3666 |
|
| No TPTP formula. May not be expressible in strict first order. | Mid-level-ontology.kif 1765-1773 |
|
| No TPTP formula. May not be expressible in strict first order. | Mid-level-ontology.kif 25927-25933 | |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 10009-10014 |
|
|
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