| PositiveRealNumber(positive real number)
| | direct_correlation, fifty_percent, pct, per_centum, percent, percentage, positive, positive_correlation, positive_real_number, 正の実数, 正实数 |
| appearance as argument number 1 |
|
|
| No TPTP formula. May not be expressible in strict first order. | chinese_format.kif 1746-1746 | |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 1841-1842 | |
| No TPTP formula. May not be expressible in strict first order. | pictureList.kif 11675-11675 | "http://upload.wikimedia.org/wikipedia/commons/d/dc/ Reelle_Zahlengerade_mit_Konstanten.png" is a URL depicting positive real number |
| No TPTP formula. May not be expressible in strict first order. | pictureList.kif 10220-10220 | "http://upload.wikimedia.org/wikipedia/commons/f/fd/ Recta_real_entero_o_decimal_exacto.png" is a URL depicting positive real number |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 1839-1839 | Positive real number is a subclass of nonnegative real number |
| appearance as argument number 2 |
|
|
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 4706-4706 | Number e is an instance of positive real number |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 4700-4700 | Pi is an instance of positive real number |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 1902-1902 | Positive integer is a subclass of positive real number |
| No TPTP formula. May not be expressible in strict first order. | chinese_format.kif 864-864 | "正实数" is the printable form of positive real number in ChineseLanguage |
| No TPTP formula. May not be expressible in strict first order. | english_format.kif 935-935 | "positive real number" is the printable form of positive real number in english language |
| appearance as argument number 3 |
|
|
| No TPTP formula. May not be expressible in strict first order. | Geography.kif 648-648 | The number 3 argument of comparative area is an instance of positive real number |
| No TPTP formula. May not be expressible in strict first order. | Economy.kif 2540-2540 | The number 3 argument of export partner by fraction is an instance of positive real number |
| No TPTP formula. May not be expressible in strict first order. | Economy.kif 2524-2524 | The number 3 argument of export partner by fraction in period is an instance of positive real number |
| No TPTP formula. May not be expressible in strict first order. | Economy.kif 2733-2733 | The number 3 argument of import partner by fraction is an instance of positive real number |
| No TPTP formula. May not be expressible in strict first order. | Economy.kif 2717-2717 | The number 3 argument of import partner by fraction in period is an instance of positive real number |
| No TPTP formula. May not be expressible in strict first order. | QoSontology.kif 1040-1040 | The number 2 argument of threshold of is an instance of positive real number |
| antecedent |
|
|
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 1844-1848 | A quantity is an instance of positive real number if and only if the quantity is greater than 0 and the quantity is an instance of real number |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 4821-4823 |
|
| consequent |
|
|
| No TPTP formula. May not be expressible in strict first order. | Geography.kif 2292-2294 |
|
|
|
|