| appearance as argument number 1 |
|
| No TPTP formula. May not be expressible in strict first order. | chinese_format.kif 3784-3785 | |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 16906-16908 | |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 16904-16904 | 一贯 的 1 数量 是 命题 的 instance |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 16905-16905 | 一贯 的 2 数量 是 命题 的 instance |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 16902-16902 | 一贯 是 二元谓语 的 instance |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 16903-16903 | 一贯 是 对称关系 的 instance |
| appearance as argument number 2 |
|
|
| No TPTP formula. May not be expressible in strict first order. | domainEnglishFormat.kif 536-536 | |
| No TPTP formula. May not be expressible in strict first order. | domainEnglishFormat.kif 535-535 | |
| No TPTP formula. May not be expressible in strict first order. | domainEnglishFormat.kif 534-534 | |
| No TPTP formula. May not be expressible in strict first order. | domainEnglishFormat.kif 16698-16698 | |
| No TPTP formula. May not be expressible in strict first order. | domainEnglishFormat.kif 16697-16697 | |
| No TPTP formula. May not be expressible in strict first order. | domainEnglishFormat.kif 16696-16696 |
| antecedent |
|
|
| No TPTP formula. May not be expressible in strict first order. | Mid-level-ontology.kif 14149-14163 |
|
| consequent |
|
|
| No TPTP formula. May not be expressible in strict first order. | Mid-level-ontology.kif 13850-13857 | 公式 的声明 has 合法 的语气 若且唯若 不存在 另一个 公式 这样 那个 另外 公式 的声明 has 法 的语气 和 那个 另外 公式 不 是 那个 公式 的 consistent |
| No TPTP formula. May not be expressible in strict first order. | MilitaryProcesses.kif 2244-2252 | |
| No TPTP formula. May not be expressible in strict first order. | Mid-level-ontology.kif 13862-13869 | |
| No TPTP formula. May not be expressible in strict first order. | Mid-level-ontology.kif 29691-29703 |
|
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 13157-13170 |
|
|
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