| 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 | Le nombre 1 argument de AbsoluteValueFn est une instance de nombre r�el |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 4761-4761 | AbsoluteValueFn est une instance de relation total |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 4760-4760 | AbsoluteValueFn est une instance de function unaire |
| 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 | Le domaine de AbsoluteValueFn est une instance de nombre r�el non n�gatif |
| 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 | La valeur absolue de nombre r�el est nombre r�el non n�gatif nombre r�el est une instance de nombre r�el nombre r�el non n�gatif est une instance de nombre r�el nombre r�el est une instance de nombre r�el non n�gatif nombre r�el est nombre r�el non n�gatif nombre r�el est une instance de nombre r�el n�gatif nombre r�el non n�gatif est nombre r�el) |
|
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