No TPTP formula. May not be expressible in strict first order. |
UXExperimentalTerms.kif 3049-3049 |
The range of qualifying purchases per user is an instance of real number |
No TPTP formula. May not be expressible in strict first order. |
Merge.kif 5973-5973 |
The range of path weight is an instance of real number |
No TPTP formula. May not be expressible in strict first order. |
People.kif 38-38 |
The range of population growth is an instance of real number |
No TPTP formula. May not be expressible in strict first order. |
Merge.kif 2574-2574 |
The range of probability is an instance of real number |
No TPTP formula. May not be expressible in strict first order. |
Merge.kif 5062-5062 |
The range of real number is an instance of real number |
No TPTP formula. May not be expressible in strict first order. |
Merge.kif 5071-5071 |
The range of 互相 is an instance of real number |
No TPTP formula. May not be expressible in strict first order. |
Merge.kif 5171-5171 |
The range of round is an instance of real number |
No TPTP formula. May not be expressible in strict first order. |
UXExperimentalTerms.kif 3713-3713 |
The range of SRP Engagement is an instance of real number |
No TPTP formula. May not be expressible in strict first order. |
Merge.kif 5212-5212 |
The range of sine is an instance of real number |
No TPTP formula. May not be expressible in strict first order. |
Merge.kif 5220-5220 |
The range of square root is an instance of real number |
No TPTP formula. May not be expressible in strict first order. |
Merge.kif 4728-4728 |
The range of subtraction is an instance of real number |
No TPTP formula. May not be expressible in strict first order. |
Merge.kif 5232-5232 |
The range of tangent is an instance of real number |
No TPTP formula. May not be expressible in strict first order. |
Merge.kif 2003-2003 |
Binary number is a subclass of real number |
No TPTP formula. May not be expressible in strict first order. |
Merge.kif 1916-1916 |
Irrational number is a subclass of real number |
No TPTP formula. May not be expressible in strict first order. |
Merge.kif 1943-1943 |
Negative real number is a subclass of real number |
No TPTP formula. May not be expressible in strict first order. |
Merge.kif 1921-1921 |
Nonnegative real number is a subclass of real number |
No TPTP formula. May not be expressible in strict first order. |
Merge.kif 1911-1911 |
Rational number is a subclass of real number |
No TPTP formula. May not be expressible in strict first order. |
chinese_format.kif 859-859 |
|
No TPTP formula. May not be expressible in strict first order. |
english_format.kif 920-920 |
|
No TPTP formula. May not be expressible in strict first order. |
french_format.kif 535-535 |
|
No TPTP formula. May not be expressible in strict first order. |
terms-hindi.txt 65-65 |
|
No TPTP formula. May not be expressible in strict first order. |
terms-it.txt 68-68 |
|
No TPTP formula. May not be expressible in strict first order. |
japanese_format.kif 2220-2220 |
|
No TPTP formula. May not be expressible in strict first order. |
portuguese_format.kif 487-487 |
|
|
Display limited to 25 items. Show next 25 |
|
Display limited to 25 items. Show next 25 |