SUMO   View all facts   Glossary   Help
Entity > Abstract > Quantity > Number > RealNumber > Pi
Next RealNumber: RationalNumber    Up: RealNumber    Previous RealNumber: NonnegativeRealNumber   

Pi
subjectfact 
Pidocumentation Pi is the RealNumber that is the ratio of the perimeter of a circle to its diameter. It is approximately equal to 3.1415926535897932001-11-30 13:34:59.0
is an instance of RealNumber2001-11-30 13:34:59.0
RealNumberhas axiom 
(=>
    (and
       (instance ?FUNCTION RelationExtendedToQuantities)
       (instance ?FUNCTION BinaryFunction)
       (instance ?NUMBER1 RealNumber)
       (instance ?NUMBER2 RealNumber)
       (equal (AssignmentFn ?FUNCTION ?NUMBER1 ?NUMBER2) ?VALUE))
    (forall (?UNIT)
       (=>
          (instance ?UNIT UnitOfMeasure)
          (equal (AssignmentFn ?FUNCTION 
                    (MeasureFn ?NUMBER1 ?UNIT) 
                    (MeasureFn ?NUMBER2 ?UNIT)) 
                 (MeasureFn ?VALUE ?UNIT)))))
2001-11-30 13:35:08.0
has axiom 
(=>
    (and
       (instance ?REL RelationExtendedToQuantities)
       (instance ?REL BinaryRelation)
       (instance ?NUMBER1 RealNumber)
       (instance ?NUMBER2 RealNumber)
       (holds ?REL ?NUMBER1 ?NUMBER2))
    (forall (?UNIT)
       (=>
          (instance ?UNIT UnitOfMeasure)
          (holds ?REL (MeasureFn ?NUMBER1 ?UNIT) (MeasureFn ?NUMBER2 ?UNIT)))))
2001-11-30 13:35:08.0
has axiom 
(=>
    (instance ?NUMBER ImaginaryNumber)
    (instance ?NUMBER (RelativeComplementFn Number RealNumber)))
2001-11-30 13:35:08.0
is first domain of AbsoluteValueFn2001-11-30 13:35:08.0
is first domain of ArcCosineFn2001-11-30 13:35:08.0
is first domain of ArcSineFn2001-11-30 13:35:08.0
is first domain of ArcTangentFn2001-11-30 13:35:08.0
is first domain of CeilingFn2001-11-30 13:35:08.0
is first domain of DenominatorFn2001-11-30 13:35:08.0
is first domain of FloorFn2001-11-30 13:35:08.0
is first domain of IntegerSquareRootFn2001-11-30 13:35:08.0
is first domain of LogFn2001-11-30 13:35:08.0
is first domain of MeasureFn2001-11-30 13:35:08.0
is first domain of NumeratorFn2001-11-30 13:35:08.0
is first domain of SignumFn2001-11-30 13:35:08.0
is first domain of SquareRootFn2001-11-30 13:35:08.0
is partitioned into NegativeRealNumber, NonnegativeRealNumber2001-11-30 13:35:08.0
Quantityis second domain of AdditionFn2001-11-30 13:35:06.0
is second domain of DivisionFn2001-11-30 13:35:06.0
is second domain of greaterThan2001-11-30 13:35:06.0
is second domain of greaterThanOrEqualTo2001-11-30 13:35:06.0
is second domain of lessThan2001-11-30 13:35:06.0
is second domain of lessThanOrEqualTo2001-11-30 13:35:06.0
is second domain of MaxFn2001-11-30 13:35:06.0
is second domain of MinFn2001-11-30 13:35:06.0
is second domain of MultiplicationFn2001-11-30 13:35:06.0
is second domain of RemainderFn2001-11-30 13:35:06.0
is second domain of SubtractionFn2001-11-30 13:35:06.0
Abstractis disjoint from Physical2001-11-30 13:33:32.0

Next RealNumber: RationalNumber    Up: RealNumber    Previous RealNumber: NonnegativeRealNumber