| appearance as argument number 1 |
|
| No TPTP formula. May not be expressible in strict first order. | Mid-level-ontology.kif 23373-23373 | 伴侣 和 国内的合作伙伴 是 disjoint 关系 |
| No TPTP formula. May not be expressible in strict first order. | chinese_format.kif 3713-3713 | |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 16564-16565 | |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 16562-16562 | 伴侣 的 1 数量 是 人类 的 instance |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 16563-16563 | 伴侣 的 2 数量 是 人类 的 instance |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 16559-16559 | 伴侣 是 非自反关系 的 instance |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 16561-16561 | 伴侣 是 部分值关系 的 instance |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 16560-16560 | 伴侣 是 对称关系 的 instance |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 16558-16558 | 伴侣 是 法律关系 的 subrelation |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 16556-16556 | 伴侣 是 相识熟人 的 subrelation |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 16322-16322 | 伴侣 是 相对的 的 subrelation |
| appearance as argument number 2 |
|
|
| No TPTP formula. May not be expressible in strict first order. | domainEnglishFormat.kif 4594-4594 | |
| No TPTP formula. May not be expressible in strict first order. | domainEnglishFormat.kif 4593-4593 | |
| No TPTP formula. May not be expressible in strict first order. | domainEnglishFormat.kif 4592-4592 | |
| No TPTP formula. May not be expressible in strict first order. | domainEnglishFormat.kif 54798-54798 | |
| No TPTP formula. May not be expressible in strict first order. | domainEnglishFormat.kif 54797-54797 | |
| No TPTP formula. May not be expressible in strict first order. | domainEnglishFormat.kif 54796-54796 |
| antecedent |
|
|
| No TPTP formula. May not be expressible in strict first order. | Mid-level-ontology.kif 7972-7982 | |
| No TPTP formula. May not be expressible in strict first order. | Biography.kif 307-317 | |
| No TPTP formula. May not be expressible in strict first order. | Mid-level-ontology.kif 23186-23202 |
|
| consequent |
|
|
| No TPTP formula. May not be expressible in strict first order. | Mid-level-ontology.kif 23152-23159 | 人 是 人类 的 stepfather 若且唯若 有存在 另一个 人类 这样 那个 另外 人类 是 那个 人类 的 mother 和 那个 人 是 那个 另外 人类 的 spouse 和 那个 人 不 是 那个 人类 father |
| No TPTP formula. May not be expressible in strict first order. | Mid-level-ontology.kif 23169-23176 | 女人 是 人类 的 stepfather 若且唯若 有存在 另一个 人类 这样 那个 另外 人类 是 那个 人类 father 和 那个 女人 是 那个 另外 人类 的 spouse 和 那个 女人 不 是 那个 人类 的 mother |
| No TPTP formula. May not be expressible in strict first order. | Government.kif 1426-1431 | |
| No TPTP formula. May not be expressible in strict first order. | Government.kif 1415-1420 | |
| No TPTP formula. May not be expressible in strict first order. | Mid-level-ontology.kif 22307-22321 | |
| No TPTP formula. May not be expressible in strict first order. | Mid-level-ontology.kif 1025-1034 | |
| No TPTP formula. May not be expressible in strict first order. | Mid-level-ontology.kif 7965-7970 | |
| No TPTP formula. May not be expressible in strict first order. | Mid-level-ontology.kif 14170-14176 |
|
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