Base Template RealMagnitudeOfProperty

This template provides a version of MagnitudeOfProperty for which the magnitude is given by a datatyped representation rather than a number object.

RealMagnitudeOfProperty(a, b, c) means that a is is an instance of Property, b is a floating point number with the property value and d the Scale as unit of measurement.

Roles:
1 hasProperty Property
2 valPropertyValue ExpressReal
3 hasPropertyScale Scale

Axiom

Template RealMagnitudeOfProperty(x1, x2, x3) <-> 
Property(x1) & 
ExpressReal(x2) & 
Scale(x3) & 
exists u(MagnitudeOfProperty(x1, u, x3) & 
IdentificationByNumber(x2, u)) . 

Lifted template

  Property(x1)
& ExpressReal(x2)
& Scale(x3)
& exists u
     (  (  Property(x1)
         & RealNumber(u)
         & Scale(x3)
         & exists u0
              (  (  PropertyQuantification(u0)
                  & hasInput(u0, x1)
                  & hasResult(u0, u))
               & exists z
                    (  Classification(z)
                     & hasClassified(z, u0)
                     & hasClassifier(z, x3))))
      & ExpressReal(x2)
      & Thing(u)
      & exists z0
           (ClassOfIdentification(z0) & hasPattern(z0, x2) & hasRepresented(z0, u)))      

Analysis diagram

Revision log

date	by	description
02/06/2011	Onno Paap	Changed ArithmeticNumber to RealNumber