SUMO   View all facts   Glossary   Help

Entity > Abstract > Class > Relation > Function > BinaryFunction > LogFn

LogFn
subject			fact

LogFn	documentation (LogFn ?NUMBER ?INT) returns the logarithm of the RealNumber ?NUMBER in the base denoted by the Integer ?INT
	has domain1 RealNumber
	has domain2 PositiveInteger
	has range RealNumber
	is an instance of BinaryFunction
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
Class	is third domain of domain
	is third domain of domainSubclass
Abstract	is disjoint from Physical

Next BinaryFunction: MeasureFn    Up: BinaryFunction    Previous BinaryFunction: KappaFn