 SUMO   View all facts   Glossary   Help Entity > Abstract > Class > Relation > Function > BinaryFunction > DensityFn
Next BinaryFunctionExponentiationFn    UpBinaryFunction, DensityMeasure    Previous BinaryFunctionDayFn  DensityFn subject fact
 DensityFn documentation A very general FunctionQuantity. DensityFn maps an instance of MassMeasure and an instance of VolumeMeasure to the density represented by this combination of mass and volume. For example, (DensityFn (MeasureFn 3 Kilogram) (MeasureFn 1 Liter)) represents the density of 3 kilograms per liter has domain1 MassMeasure has domain2 VolumeMeasure has range DensityMeasure is an instance of BinaryFunction is an instance of DensityMeasure BinaryFunction has axiom `(<=> (and (holds ?REL ?INST1 ?INST2 ?INST3) (instance ?REL BinaryFunction)) (equal (AssignmentFn ?REL ?INST1 ?INST2) ?INST3))` has axiom `(=> (and (closedOn ?FUNCTION ?CLASS) (instance ?FUNCTION BinaryFunction)) (forall (?INST1 ?INST2) (=> (and (instance ?INST1 ?CLASS) (instance ?INST2 ?CLASS)) (instance (AssignmentFn ?FUNCTION ?INST1 ?INST2) ?CLASS))))` has axiom `(=> (and (instance ?FUNCTION BinaryFunction) (equal (AssignmentFn ?FUNCTION ?ARG1 ?ARG2) ?VALUE1) (equal (AssignmentFn ?FUNCTION ?ARG1 ?ARG2) ?VALUE2)) (equal ?VALUE1 ?VALUE2))` has 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)))))` has axiom `(=> (instance ?FUNCTION BinaryFunction) (valence ?FUNCTION 2))` is first domain of distributes is first domain of identityElement is second domain of distributes PhysicalQuantity is partitioned into ConstantQuantity, FunctionQuantity Class is third domain of domain is third domain of domainSubclass Abstract is disjoint from Physical  Next BinaryFunctionExponentiationFn    UpBinaryFunction, DensityMeasure    Previous BinaryFunctionDayFn