SUMO   View all facts   Glossary   Help

Entity > Abstract > Class > Relation > Function > BinaryFunction > DensityFn

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 BinaryFunction: ExponentiationFn    Up: BinaryFunction, DensityMeasure    Previous BinaryFunction: DayFn