| PositiveRealNumber(positive real number)
| | direct_correlation, fifty_percent, pct, per_centum, percent, percentage, positive, positive_correlation |
| 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 1842-1843 | |
| No TPTP formula. May not be expressible in strict first order. | pictureList.kif 11675-11675 | |
| No TPTP formula. May not be expressible in strict first order. | pictureList.kif 10220-10220 | |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 1840-1840 | 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 4835-4835 | Number e is an instance of positive real number |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 4829-4829 | Pi is an instance of positive real number |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 1903-1903 | 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 | |
| No TPTP formula. May not be expressible in strict first order. | english_format.kif 935-935 |
| 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 1845-1849 | 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 4950-4952 |
|
| consequent |
|
|
| No TPTP formula. May not be expressible in strict first order. | Geography.kif 2292-2294 |
|
|
|
|