RealNumber
|
|
appearance as argument number 1 |
No TPTP formula. May not be expressible in strict first order. | chinese_format.kif 1737-1738 | |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 1895-1897 | |
No TPTP formula. May not be expressible in strict first order. | japanese_format.kif 345-346 | |
No TPTP formula. May not be expressible in strict first order. | pictureList.kif 11735-11735 | |
No TPTP formula. May not be expressible in strict first order. | pictureList.kif 10223-10223 | |
No TPTP formula. May not be expressible in strict first order. | pictureList.kif 11734-11734 | |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 1892-1892 | Nombre r�el est compl�tement d�compos� en nombre r�el n�gatif + nombre r�el non n�gatif |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 1893-1893 | Nombre r�el est compl�tement d�compos� en nombre rationnel + nombre irrationnel |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 1891-1891 | Nombre r�el est une sous-classe de nombre |
appearance as argument number 2 |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 2009-2009 | Nombre complexe est disjoint de nombre r�el |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 1825-1825 | Nombre est compl�tement d�compos� en nombre r�el, nombre imaginaire, + nombre complexe |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 4714-4714 | Le domaine de AdditionFn est une instance de nombre r�el |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 5260-5260 | Le domaine de ArcCosineFn est une instance de nombre r�el |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 5270-5270 | Le domaine de ArcSineFn est une instance de nombre r�el |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 5250-5250 | Le domaine de ArcTangentFn est une instance de nombre r�el |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 3272-3272 | Le domaine de AverageFn est une instance de nombre r�el |
No TPTP formula. May not be expressible in strict first order. | People.kif 71-71 | Le domaine de BirthsPerThousandFn est une instance de nombre r�el |
No TPTP formula. May not be expressible in strict first order. | People.kif 443-443 | Le domaine de ChildrenBornPerWomanFn est une instance de nombre r�el |
No TPTP formula. May not be expressible in strict first order. | UXExperimentalTerms.kif 3331-3331 | Le domaine de ClickThroughRateFn est une instance de nombre r�el |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 4802-4802 | Le domaine de CosineFn est une instance de nombre r�el |
No TPTP formula. May not be expressible in strict first order. | People.kif 104-104 | Le domaine de DeathsPerThousandFn est une instance de nombre r�el |
No TPTP formula. May not be expressible in strict first order. | People.kif 230-230 | Le domaine de DeathsPerThousandLiveBirthsFn est une instance de nombre r�el |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 4744-4744 | Le domaine de DivisionFn est une instance de nombre r�el |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 4821-4821 | Le domaine de ExponentiationFn est une instance de nombre r�el |
No TPTP formula. May not be expressible in strict first order. | People.kif 396-396 | Le domaine de FemaleLifeExpectancyAtBirthFn est une instance de nombre r�el |
No TPTP formula. May not be expressible in strict first order. | People.kif 299-299 | Le domaine de LifeExpectancyAtBirthFn est une instance de nombre r�el |
No TPTP formula. May not be expressible in strict first order. | UXExperimentalTerms.kif 4555-4555 | Le domaine de LiftFn est une instance de nombre r�el |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 3241-3241 | Le domaine de ListSumFn est une instance de nombre r�el |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 4977-4977 | Le domaine de LogFn est une instance de nombre r�el |
No TPTP formula. May not be expressible in strict first order. | People.kif 348-348 | Le domaine de MaleLifeExpectancyAtBirthFn est une instance de nombre r�el |
No TPTP formula. May not be expressible in strict first order. | People.kif 193-193 | Le domaine de MaleToFemaleRatioFn est une instance de nombre r�el |
No TPTP formula. May not be expressible in strict first order. | People.kif 140-140 | Le domaine de MigrantsPerThousandFn est une instance de nombre r�el |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 4701-4701 | Le domaine de MultiplicationFn est une instance de nombre r�el |
No TPTP formula. May not be expressible in strict first order. | UXExperimentalTerms.kif 3088-3088 | Le domaine de PPIFn est une instance de nombre r�el |
Display limited to 25 items. Show next 25 | ||
Display limited to 25 items. Show next 25 |
appearance as argument number 3 |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 4762-4762 | Le nombre 1 argument de AbsoluteValueFn est une instance de nombre r�el |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 4712-4712 | Le nombre 1 argument de AdditionFn est une instance de nombre r�el |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 4713-4713 | Le nombre 2 argument de AdditionFn est une instance de nombre r�el |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 5259-5259 | Le nombre 1 argument de ArcCosineFn est une instance de nombre r�el |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 5269-5269 | Le nombre 1 argument de ArcSineFn est une instance de nombre r�el |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 5249-5249 | Le nombre 1 argument de ArcTangentFn est une instance de nombre r�el |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 4783-4783 | Le nombre 1 argument de CeilingFn est une instance de nombre r�el |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 4810-4810 | Le nombre 1 argument de DenominatorFn est une instance de nombre r�el |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 4742-4742 | Le nombre 1 argument de DivisionFn est une instance de nombre r�el |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 4743-4743 | Le nombre 2 argument de DivisionFn est une instance de nombre r�el |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 4819-4819 | Le nombre 1 argument de ExponentiationFn est une instance de nombre r�el |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 4828-4828 | Le nombre 1 argument de FloorFn est une instance de nombre r�el |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 4923-4923 | Le nombre 1 argument de IntegerSquareRootFn est une instance de nombre r�el |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 4975-4975 | Le nombre 1 argument de LogFn est une instance de nombre r�el |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 6348-6348 | Le nombre 1 argument de MeasureFn est une instance de nombre r�el |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 4699-4699 | Le nombre 1 argument de MultiplicationFn est une instance de nombre r�el |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 4700-4700 | Le nombre 2 argument de MultiplicationFn est une instance de nombre r�el |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 5036-5036 | Le nombre 1 argument de NumeratorFn est une instance de nombre r�el |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 5070-5070 | Le nombre 1 argument de ReciprocalFn est une instance de nombre r�el |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 5170-5170 | Le nombre 1 argument de RoundFn est une instance de nombre r�el |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 5189-5189 | Le nombre 1 argument de SignumFn est une instance de nombre r�el |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 5211-5211 | Le nombre 1 argument de SineFn est une instance de nombre r�el |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 5219-5219 | Le nombre 1 argument de SquareRootFn est une instance de nombre r�el |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 4726-4726 | Le nombre 1 argument de SubtractionFn est une instance de nombre r�el |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 4727-4727 | Le nombre 2 argument de SubtractionFn est une instance de nombre r�el |
Display limited to 25 items. Show next 25 | ||
Display limited to 25 items. Show next 25 |
antecedent |
consequent |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 1948-1952 | Nombre r�el est une instance de nombre r�el n�gatif nombre r�el est moins que 0 nombre r�el est une instance de nombre r�el |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 1926-1930 | Nombre r�el est une instance de nombre r�el non n�gatif nombre r�el est plus grand ou �gal � 0 nombre r�el est une instance de nombre r�el |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 1937-1941 | Nombre r�el est une instance de nombre r�el positif nombre r�el est plus grand que 0 nombre r�el est une instance de nombre r�el |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 5369-5374 |
|
No TPTP formula. May not be expressible in strict first order. | Food.kif 770-781 |
|