FloorFn concept from the SUMO knowledge base

Next UnaryFunction: FutureFn Up: UnaryFunction Previous UnaryFunction: ExtensionFn

Next UnaryFunction: FutureFn Up: UnaryFunction Previous UnaryFunction: ExtensionFn

FloorFn	*documentation* (FloorFn ?NUMBER) returns the largest Integer less than or equal to the RealNumber ?NUMBER
	has axiom (<=> (equal (RemainderFn ?NUMBER1 ?NUMBER2) ?NUMBER) (equal (AdditionFn (MultiplicationFn (FloorFn (DivisionFn ?NUMBER1 ?NUMBER2)) ?NUMBER2) ?NUMBER) ?NUMBER1))
	has axiom (=> (equal (FloorFn ?NUMBER) ?INT) (not (exists (?OTHERINT) (and (instance ?OTHERINT Integer) (lessThanOrEqualTo ?OTHERINT ?NUMBER) (greaterThan ?OTHERINT ?INT)))))
	has axiom (=> (equal (RoundFn ?NUMBER1) ?NUMBER2) (or (=> (lessThan (SubtractionFn ?NUMBER1 (FloorFn ?NUMBER1)) .5) (equal ?NUMBER2 (FloorFn ?NUMBER1))) (=> (greaterThanOrEqualTo (SubtractionFn ?NUMBER1 (FloorFn ?NUMBER1)) .5) (equal ?NUMBER2 (CeilingFn ?NUMBER1)))))
	has domain1 RealNumber
	has range Integer
	*is an instance* of** UnaryFunction
BinaryRelation	*is first domain* of** DomainFn
	*is first domain* of** equivalenceRelationOn
	*is first domain* of** inverse
	*is first domain* of** irreflexiveOn
	*is first domain* of** partialOrderingOn
	*is first domain* of** RangeFn
	*is first domain* of** reflexiveOn
	*is first domain* of** totalOrderingOn
	*is first domain* of** trichotomizingOn
	*is second domain* of** inverse
Function	*is first domain* of** AssignmentFn
	*is first domain* of** closedOn
	*is first domain* of** range
	*is first domain* of** rangeSubclass
Class	*is third domain* of** domain
Class	*is third domain* of** domainSubclass
Abstract	*is disjoint* from** Physical


*FloorFn*
subject			fact