| appearance as argument number 1 |
|
| No TPTP formula. May not be expressible in strict first order. | chinese_format.kif 2275-2275 | |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 5223-5224 | |
| No TPTP formula. May not be expressible in strict first order. | japanese_format.kif 941-942 | |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 5220-5220 | The number 1 argument of square root is an instance of real number |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 5219-5219 | Square root is an instance of unary function |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 5221-5221 | The range of square root is an instance of real number |
| appearance as argument number 2 |
|
|
| No TPTP formula. May not be expressible in strict first order. | chinese_format.kif 730-730 | |
| No TPTP formula. May not be expressible in strict first order. | english_format.kif 732-732 | |
| No TPTP formula. May not be expressible in strict first order. | french_format.kif 438-438 | |
| No TPTP formula. May not be expressible in strict first order. | relations-it.txt 268-268 | |
| No TPTP formula. May not be expressible in strict first order. | japanese_format.kif 2155-2155 | |
| No TPTP formula. May not be expressible in strict first order. | portuguese_format.kif 390-390 | |
| No TPTP formula. May not be expressible in strict first order. | relations-de.txt 943-943 | |
| No TPTP formula. May not be expressible in strict first order. | relations-hindi.txt 305-305 | |
| No TPTP formula. May not be expressible in strict first order. | relations-ro.kif 460-460 | |
| No TPTP formula. May not be expressible in strict first order. | relations-sv.txt 500-500 | |
| No TPTP formula. May not be expressible in strict first order. | domainEnglishFormat.kif 54890-54890 | |
| No TPTP formula. May not be expressible in strict first order. | chinese_format.kif 731-731 | |
| No TPTP formula. May not be expressible in strict first order. | domainEnglishFormat.kif 54889-54889 | |
| No TPTP formula. May not be expressible in strict first order. | domainEnglishFormat.kif 54888-54888 |
| antecedent |
|
|
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 5226-5228 |
|
| consequent |
|
|
| No TPTP formula. May not be expressible in strict first order. | Weather.kif 1492-1497 | A real number is equal to The StandardDeviationFn of a list if and only if the real number is equal to the squareRoot of The VarianceFn the list |
|
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