| 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 and RealNumber |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 4761-4761 | 例 絕對值 and TotalValuedRelation |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 4760-4760 | 例 絕對值 and UnaryFunction |
| 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 | 範圍 絕對值 and NonnegativeRealNumber |
| 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 | 等於 絕對值 RealNumber and NonnegativeRealNumber 例 RealNumber and RealNumber 例 NonnegativeRealNumber and RealNumber 例 RealNumber and NonnegativeRealNumber 等於 RealNumber and NonnegativeRealNumber 例 RealNumber and NegativeRealNumber 等於 NonnegativeRealNumber and 減法 0.0 and RealNumber |
|
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