| appearance as argument number 1 |
|
| No TPTP formula. May not be expressible in strict first order. | chinese_format.kif 3798-3799 | |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 17014-17015 | |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 17012-17012 | 域 真相, 1 and Sentence |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 17013-17013 | 域 真相, 2 and TruthValue |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 17011-17011 | 例 真相 and BinaryPredicate |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 17010-17010 | 子關係 真相 and 屬性 |
| appearance as argument number 2 |
|
|
| No TPTP formula. May not be expressible in strict first order. | chinese_format.kif 197-197 | |
| No TPTP formula. May not be expressible in strict first order. | english_format.kif 198-198 | |
| No TPTP formula. May not be expressible in strict first order. | japanese_format.kif 1947-1947 | |
| No TPTP formula. May not be expressible in strict first order. | chinese_format.kif 198-198 | |
| No TPTP formula. May not be expressible in strict first order. | domainEnglishFormat.kif 59360-59360 | |
| No TPTP formula. May not be expressible in strict first order. | domainEnglishFormat.kif 59359-59359 | |
| No TPTP formula. May not be expressible in strict first order. | domainEnglishFormat.kif 59358-59358 |
| consequent |
|
|
| No TPTP formula. May not be expressible in strict first order. | Mid-level-ontology.kif 1844-1848 | |
| No TPTP formula. May not be expressible in strict first order. | Mid-level-ontology.kif 1854-1858 | |
| No TPTP formula. May not be expressible in strict first order. | UXExperimentalTerms.kif 549-556 | |
| No TPTP formula. May not be expressible in strict first order. | UXExperimentalTerms.kif 540-547 | |
| No TPTP formula. May not be expressible in strict first order. | Medicine.kif 3449-3460 |
|
| No TPTP formula. May not be expressible in strict first order. | Mid-level-ontology.kif 6428-6438 |
|
| No TPTP formula. May not be expressible in strict first order. | Mid-level-ontology.kif 17896-17901 | |
| No TPTP formula. May not be expressible in strict first order. | Medicine.kif 4195-4210 |
|
| No TPTP formula. May not be expressible in strict first order. | Mid-level-ontology.kif 12976-12981 | |
| No TPTP formula. May not be expressible in strict first order. | Mid-level-ontology.kif 922-929 | |
| No TPTP formula. May not be expressible in strict first order. | UXExperimentalTerms.kif 577-584 | |
| No TPTP formula. May not be expressible in strict first order. | UXExperimentalTerms.kif 586-593 | |
| No TPTP formula. May not be expressible in strict first order. | Law.kif 65-78 |
|
| No TPTP formula. May not be expressible in strict first order. | Mid-level-ontology.kif 19347-19353 |
|
| No TPTP formula. May not be expressible in strict first order. | Mid-level-ontology.kif 14245-14247 | |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 13049-13054 | |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 2838-2840 | |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 17551-17553 | |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 17559-17561 |
|
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