NonnegativeRealNumber
|
|
appearance as argument number 1 |
No TPTP formula. May not be expressible in strict first order. | chinese_format.kif 1745-1745 | |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 1923-1924 | |
No TPTP formula. May not be expressible in strict first order. | japanese_format.kif 353-353 | |
No TPTP formula. May not be expressible in strict first order. | pictureList.kif 11508-11508 | |
No TPTP formula. May not be expressible in strict first order. | pictureList.kif 10149-10149 | |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 1921-1921 | Numero Real nao-negativo e' uma sub-classe de Numero Real |
appearance as argument number 2 |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 4763-4763 | O contra-dominio de AbsoluteValueFn e' uma instancia de Numero Real nao-negativo |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 1976-1976 | Numero Inteiro nao-negativo e' uma sub-classe de Numero Real nao-negativo |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 1932-1932 | Numero Real positivo e' uma sub-classe de Numero Real nao-negativo |
No TPTP formula. May not be expressible in strict first order. | chinese_format.kif 863-863 | |
No TPTP formula. May not be expressible in strict first order. | english_format.kif 928-928 | |
No TPTP formula. May not be expressible in strict first order. | french_format.kif 539-539 | |
No TPTP formula. May not be expressible in strict first order. | terms-hindi.txt 69-69 | |
No TPTP formula. May not be expressible in strict first order. | terms-it.txt 72-72 | |
No TPTP formula. May not be expressible in strict first order. | japanese_format.kif 2224-2224 | |
No TPTP formula. May not be expressible in strict first order. | portuguese_format.kif 491-491 | |
No TPTP formula. May not be expressible in strict first order. | terms-cz.txt 106-106 | |
No TPTP formula. May not be expressible in strict first order. | relations-ro.kif 560-560 | |
No TPTP formula. May not be expressible in strict first order. | terms-tg.txt 73-73 |
appearance as argument number 3 |
No TPTP formula. May not be expressible in strict first order. | Weather.kif 867-867 | O argumento numero 2 de cloudCoverFraction e' uma instancia de Numero Real nao-negativo |
No TPTP formula. May not be expressible in strict first order. | Economy.kif 1306-1306 | O argumento numero 2 de incomeDistributionByGiniIndex e' uma instancia de Numero Real nao-negativo |
No TPTP formula. May not be expressible in strict first order. | Economy.kif 1291-1291 | O argumento numero 2 de incomeDistributionByGiniIndexInPeriod e' uma instancia de Numero Real nao-negativo |
No TPTP formula. May not be expressible in strict first order. | Economy.kif 1366-1366 | O argumento numero 2 de laborForceTotal e' uma instancia de Numero Real nao-negativo |
No TPTP formula. May not be expressible in strict first order. | Economy.kif 1356-1356 | O argumento numero 2 de laborForceTotalInPeriod e' uma instancia de Numero Real nao-negativo |
No TPTP formula. May not be expressible in strict first order. | Weather.kif 950-950 | O argumento numero 3 de overcastDaysInPeriod e' uma instancia de Numero Real nao-negativo |
No TPTP formula. May not be expressible in strict first order. | Weather.kif 1020-1020 | O argumento numero 2 de relativeHumidity e' uma instancia de Numero Real nao-negativo |
No TPTP formula. May not be expressible in strict first order. | Geography.kif 1675-1675 | O argumento numero 2 de slopeGradient e' uma instancia de Numero Real nao-negativo |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 1892-1892 | O conceito Numero Real e' completamente decomposto em Numero Real negativo + Numero Real nao-negativo |
antecedent |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 1926-1930 | Numero Real e' uma instancia de Numero Real nao-negativo Numero Real e' maior ou igual a 0 Numero Real e' uma instancia de Numero Real |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 5195-5199 |
|
consequent |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 4768-4779 | O valor absoluto de Numero Real e' igual a Numero Real nao-negativo Numero Real e' uma instancia de Numero Real Numero Real nao-negativo e' uma instancia de Numero Real Numero Real e' uma instancia de Numero Real nao-negativo Numero Real e' igual a Numero Real nao-negativo Numero Real e' uma instancia de Numero Real negativo Numero Real nao-negativo e' igual a (0.0 + Numero Real) |