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 1945-1946 | |
No TPTP formula. May not be expressible in strict first order. | japanese_format.kif 354-354 | |
No TPTP formula. May not be expressible in strict first order. | pictureList.kif 11641-11641 | |
No TPTP formula. May not be expressible in strict first order. | pictureList.kif 10197-10197 | |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 1943-1943 | 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 5076-5076 | Number e is an instance of positive real number |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 5070-5070 | Pi is an instance of positive real number |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 2006-2006 | 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 | Positive integer is a subclass of positive real number |
No TPTP formula. May not be expressible in strict first order. | english_format.kif 930-930 | Positive integer is a subclass of positive real number |
No TPTP formula. May not be expressible in strict first order. | french_format.kif 540-540 | Positive integer is a subclass of positive real number |
No TPTP formula. May not be expressible in strict first order. | terms-hindi.txt 70-70 | Positive integer is a subclass of positive real number |
No TPTP formula. May not be expressible in strict first order. | terms-it.txt 73-73 | Positive integer is a subclass of positive real number |
No TPTP formula. May not be expressible in strict first order. | japanese_format.kif 2225-2225 | Positive integer is a subclass of positive real number |
No TPTP formula. May not be expressible in strict first order. | portuguese_format.kif 492-492 | Positive integer is a subclass of positive real number |
No TPTP formula. May not be expressible in strict first order. | terms-cz.txt 107-107 | Positive integer is a subclass of positive real number |
No TPTP formula. May not be expressible in strict first order. | terms-de.txt 366-366 | Positive integer is a subclass of positive real number |
No TPTP formula. May not be expressible in strict first order. | relations-ro.kif 561-561 | Positive integer is a subclass of positive real number |
No TPTP formula. May not be expressible in strict first order. | terms-tg.txt 74-74 | Positive integer is a subclass of positive real number |
appearance as argument number 3 |
![]() |
No TPTP formula. May not be expressible in strict first order. | Geography.kif 815-815 | 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 2777-2777 | 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 2761-2761 | 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 3067-3067 | 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 3051-3051 | 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 1144-1144 | 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 1948-1952 | A real number is an instance of positive real number if and only if the real number is greater than 0 and the real number is an instance of real number |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 5229-5231 |
|
consequent |
![]() |
No TPTP formula. May not be expressible in strict first order. | Geography.kif 2507-2509 |
|
![]() |
![]() |