BinaryFunction concept from the SUMO knowledge base

Entity > Abstract > Class > Relation > Function > BinaryFunction

Next Function: ContinuousFunction Up: Function, TernaryRelation Previous Function: AssignmentFn

BinaryFunction

subject fact

BinaryFunction documentation The Class of Functions that require two arguments 2001-11-30 13:33:43.0
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))))
2001-11-30 13:33:43.0
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)))))
2001-11-30 13:33:43.0
has axiom
(=>
(instance ?FUNCTION BinaryFunction)
(valence ?FUNCTION 2))
is first domain of distributes
is first domain of identityElement
is second domain of distributes
is a kind of Function
is a kind of TernaryRelation

Class is third domain of domain 2001-11-30 13:33:51.0
is third domain of domainSubclass

Abstract is disjoint from Physical 2001-11-30 13:33:32.0

Kinds of BinaryFunction :

AssociativeFunction (6 kinds, 105 facts) - A BinaryFunction is associative if bracketing has no effect on the value returned by the Function. More precisely, a Function ?FUNCTION is associative just in case (?FUNCTION ?INST1 (?FUNCTION ?INST2 ?INST3)) is equal to (?FUNCTION (?FUNCTION ?INST1 ?INST2) ?INST3), for all ?INST1, ?INST2, and ?INST3
CommutativeFunction (4 kinds, 80 facts) - A BinaryFunction is commutative if the ordering of the arguments of the function has no effect on the value returned by the function. More precisely, a function ?FUNCTION is commutative just in case (?FUNCTION ?INST1 ?INST2) is equal to (?FUNCTION ?INST2 ?INST1), for all ?INST1 and ?INST2
DayFn (7 facts) - A BinaryFunction that maps a number and a Month to the corresponding Day of the Month. For example, (DayFn 18 (MonthFn 8 (YearFn 1912))) denotes the 18th day of August 1912
DensityFn (6 facts) - 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
ExponentiationFn (7 facts) - (ExponentiationFn ?NUMBER ?INT) returns the RealNumber ?NUMBER raised to the power of the Integer ?INT
HourFn (7 facts) - A BinaryFunction that maps a number and a Day to the corresponding Hour of the Day. For example, (HourFn 14 (DayFn 18 (MonthFn 8 (YearFn 1912)))) denotes the 14th hour, i.e. 2 PM, on the 18th day of August 1912
HourIntervalFn (7 facts) - A BinaryFunction that maps two numbers to the Class of TimeIntervals that begin at the hour corresponding to the first number and that end at the hour corresponding to the second number. For example, (HourIntervalFn 6 12) returns the set of TimeIntervals that begin at 6 AM every day and that end at 12 noon every day. If necessary, we will define other interval functions for seconds, minutes, days, and/or months
IntersectionFn (7 facts) - A BinaryFunction that maps two %Classes to the intersection of these Classes. An object is an instance of the intersection of two Classes just in case it is an instance of both of those Classes
KappaFn (5 facts) - A class-forming operator that takes two arguments: a variable and a formula containing at least one unbound occurrence of the variable. The result of applying KappaFn to a variable and a formula is the Class of things that satisfy the formula. For example, we can denote the Class of prime numbers that are less than 100 with the following expression: (KappaFn ?NUMBER (and (instance ?NUMBER PrimeNumber) (lessThan ?NUMBER 100))). Note that the use of this function is discouraged, since there is currently no axiomatic support for it
LogFn (5 facts) - (LogFn ?NUMBER ?INT) returns the logarithm of the RealNumber ?NUMBER in the base denoted by the Integer ?INT
MeasureFn (59 facts) - This BinaryFunction maps a RealNumber and a UnitOfMeasure to that Number of units. It is used for expressing ConstantQuantities. For example, the concept of three meters is represented as (MeasureFn 3 Meter)
MereologicalDifferenceFn (7 facts) - (MereologicalDifferenceFn ?OBJ1 ?OBJ2) denotes the Object consisting of the parts which belong to ?OBJ1 and not to ?OBJ2
MereologicalProductFn (9 facts) - (MereologicalProductFn ?OBJ1 ?OBJ2) denotes the Object consisting of the parts which belong to both ?OBJ1 and ?OBJ2
MereologicalSumFn (11 facts) - (MereologicalSumFn ?OBJ1 ?OBJ2) denotes the Object consisting of the parts which belong to either ?OBJ1 or ?OBJ2
MinuteFn (7 facts) - A BinaryFunction that maps a number and an Hour to the corresponding Minute of the Hour. For example, (MinuteFn 15 (HourFn 14 (DayFn 18 (MonthFn 8 (YearFn 1912))))) denotes 15 minutes after 2 PM on the 18th day of August 1912
MonthFn (7 facts) - A BinaryFunction that maps a number and a Year to the corresponding Month of the Year. For example (MonthFn 8 (YearFn 1912)) denotes the eighth Month, i.e. August, of the Year 1912
RelativeComplementFn (7 facts) - A BinaryFunction that maps two Classes to the difference between these Classes. More precisely, the relative complement of one class C1 relative to another C2 consists of the instances of C1 that are instances of the ComplementFn of C2
RemainderFn (11 facts) - (RemainderFn ?NUMBER ?DIVISOR) is the remainder of the number ?NUMBER divided by the number ?DIVISOR. The result has the same sign as ?DIVISOR
SecondFn (7 facts) - A BinaryFunction that maps a number and a Minute to the corresponding Second of the Minute. For example, (SecondFn 9 (MinuteFn 15 (HourFn 14 (DayFn 18 (MonthFn 8 (YearFn 1912)))))) denotes 9 seconds and 15 minutes after 2 PM on the 18th day of August 1912
UnionFn (6 facts) - A BinaryFunction that maps two Classes to the union of these Classes. An object is an instance of the union of two Classes just in case it is an instance of either Class
WhereFn (12 facts) - Maps an Object and a TimePoint at which the Object exists to the Region where the Object existed at that TimePoint

BinaryFunction	*documentation* The Class of Functions that require two arguments
	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
	is a kind of Function
	is a kind of TernaryRelation
Class	*is third domain* of** domain
Class	*is third domain* of** domainSubclass
Abstract	*is disjoint* from** Physical