| appearance as argument number 1 |
|
| No TPTP formula. May not be expressible in strict first order. | chinese_format.kif 2224-2225 | |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 4765-4766 | |
| No TPTP formula. May not be expressible in strict first order. | japanese_format.kif 888-889 | |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 4762-4762 | 绝对值函数 的 1 数量 是 实数 的 instance |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 4761-4761 | 绝对值函数 是 总值关系 的 instance |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 4760-4760 | 绝对值函数 是 一元函数 的 instance |
| No TPTP formula. May not be expressible in strict first order. | engineering.kif 134-134 | |
| No TPTP formula. May not be expressible in strict first order. | engineering.kif 135-135 | |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 4763-4763 | 绝对值函数 的 range 是 非负实数 的实例 |
| appearance as argument number 2 |
|
|
| No TPTP formula. May not be expressible in strict first order. | chinese_format.kif 688-688 | |
| No TPTP formula. May not be expressible in strict first order. | english_format.kif 690-690 | |
| No TPTP formula. May not be expressible in strict first order. | french_format.kif 417-417 | |
| No TPTP formula. May not be expressible in strict first order. | relations-it.txt 18-18 | |
| No TPTP formula. May not be expressible in strict first order. | japanese_format.kif 2134-2134 | |
| No TPTP formula. May not be expressible in strict first order. | portuguese_format.kif 369-369 | |
| No TPTP formula. May not be expressible in strict first order. | relations-de.txt 895-895 | |
| No TPTP formula. May not be expressible in strict first order. | relations-hindi.txt 63-63 | |
| No TPTP formula. May not be expressible in strict first order. | relations-ro.kif 439-439 | |
| No TPTP formula. May not be expressible in strict first order. | relations-sv.txt 461-461 | |
| No TPTP formula. May not be expressible in strict first order. | relations-cb.txt 52-52 | |
| No TPTP formula. May not be expressible in strict first order. | domainEnglishFormat.kif 5154-5154 | |
| No TPTP formula. May not be expressible in strict first order. | chinese_format.kif 689-689 | |
| No TPTP formula. May not be expressible in strict first order. | domainEnglishFormat.kif 5153-5153 | |
| No TPTP formula. May not be expressible in strict first order. | domainEnglishFormat.kif 5152-5152 | |
| No TPTP formula. May not be expressible in strict first order. | relations-tg.txt 53-53 |
| antecedent |
|
|
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 4768-4779 | 实数 的绝对值 equal 非负实数 和 那个 实数 是 实数 的 instance 和 那个 非负实数 是 实数 的 instance 若且唯若 那个 实数 是 非负实数 的 instance 和 那个 实数 equal 那个 非负实数 或 那个 实数 是 负实数 的 instance 和 那个 非负实数 equal (0.0 和 那个 实数) |
|
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