BinaryFunction Comparison Table

Entity > Abstract > Class > Relation > Function > BinaryFunction

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

BinaryFunction comparison table

Subject have domain2 have domain1 partition into have range documentation have axiom is a kind of is an instance of have relatedInternalConcept

AssociativeFunction 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
(=>
(instance ?FUNCTION AssociativeFunction)
(forall (?INST1 ?INST2 ?INST3)
(=>
(and
(instance ?INST1 (DomainFn ?FUNCTION))
(instance ?INST2 (DomainFn ?FUNCTION))
(instance ?INST3 (DomainFn ?FUNCTION)))
(equal (AssignmentFn ?FUNCTION ?INST1 (AssignmentFn ?FUNCTION ?INST1 ?INST2))
(AssignmentFn ?FUNCTION (AssignmentFn ?FUNCTION ?INST1 ?INST2) ?INST3)))))
BinaryFunction

CommutativeFunction 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
(=>
(instance ?FUNCTION CommutativeFunction)
(forall (?INST1 ?INST2)
(=>
(and
(instance ?INST1 (DomainFn ?FUNCTION))
(instance ?INST2 (DomainFn ?FUNCTION)))
(equal (AssignmentFn ?FUNCTION ?INST1 ?INST2)
(AssignmentFn ?FUNCTION ?INST2 ?INST1)))))
BinaryFunction

DayFn Month PositiveInteger Day 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
(=>
(instance (DayFn ?NUMBER ?MONTH) Day)
(lessThanOrEqualTo ?NUMBER 31))
TemporalRelation

DensityFn VolumeMeasure MassMeasure ConstantQuantity, FunctionQuantity DensityMeasure 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
(=>
(instance ?FUNCTION BinaryFunction)
(valence ?FUNCTION 2))
DensityMeasure

ExponentiationFn Integer Quantity Quantity (ExponentiationFn ?NUMBER ?INT) returns the RealNumber ?NUMBER raised to the power of the Integer ?INT
(equal (ReciprocalFn ?NUMBER)
(ExponentiationFn ?NUMBER -1))
RelationExtendedToQuantities

HourFn Day PositiveRealNumber Hour 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
(=>
(instance (HourFn ?NUMBER ?DAY) Hour)
(lessThan ?NUMBER 24))
TemporalRelation

HourIntervalFn PositiveRealNumber PositiveRealNumber TimeInterval 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
(=>
(instance ?INTERVAL (HourIntervalFn ?NUMBER1 ?NUMBER2))
(and
(lessThan ?NUMBER1 24)
(lessThan ?NUMBER2 24)
(lessThan ?NUMBER1 ?NUMBER2)))
TemporalRelation

IntersectionFn Class Class Class 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
(equal (RelativeComplementFn ?CLASS1 ?CLASS2)
(IntersectionFn ?CLASS1 (ComplementFn ?CLASS2)))
BinaryFunction

KappaFn Formula SymbolicString Class 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
(=>
(instance ?FUNCTION BinaryFunction)
(valence ?FUNCTION 2))
BinaryFunction

LogFn PositiveInteger RealNumber RealNumber (LogFn ?NUMBER ?INT) returns the logarithm of the RealNumber ?NUMBER in the base denoted by the Integer ?INT
(=>
(instance ?FUNCTION BinaryFunction)
(valence ?FUNCTION 2))
BinaryFunction

MeasureFn UnitOfMeasure RealNumber ConstantQuantity 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)
(equal
(MeasureFn ?NUMBER YearDuration)
(MeasureFn (MultiplicationFn ?NUMBER 365) DayDuration))
BinaryFunction

MereologicalDifferenceFn Object Object Object (MereologicalDifferenceFn ?OBJ1 ?OBJ2) denotes the Object consisting of the parts which belong to ?OBJ1 and not to ?OBJ2
(=>
(equal ?OBJ3 (MereologicalDifferenceFn ?OBJ1 ?OBJ2))
(forall (?PART)
(<=>
(part ?PART ?OBJ3)
(and
(part ?PART ?OBJ1)
(not
(part ?PART ?OBJ2))))))
SpatialRelation

MereologicalProductFn Object Object Object (MereologicalProductFn ?OBJ1 ?OBJ2) denotes the Object consisting of the parts which belong to both ?OBJ1 and ?OBJ2
(=>
(equal ?OBJ3 (MereologicalProductFn ?OBJ1 ?OBJ2))
(forall (?PART)
(<=>
(part ?PART ?OBJ3)
(and
(part ?PART ?OBJ1)
(part ?PART ?OBJ2)))))
SpatialRelation MereologicalDifferenceFn

MereologicalSumFn Object Object Object (MereologicalSumFn ?OBJ1 ?OBJ2) denotes the Object consisting of the parts which belong to either ?OBJ1 or ?OBJ2
(=>
(equal ?OBJ3 (MereologicalSumFn ?OBJ1 ?OBJ2))
(forall (?PART)
(<=>
(part ?PART ?OBJ3)
(or
(part ?PART ?OBJ1)
(part ?PART ?OBJ2)))))
SpatialRelation MereologicalProductFn

MinuteFn Hour PositiveRealNumber Minute 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
(=>
(instance (MinuteFn ?NUMBER ?HOUR) Minute)
(lessThan ?NUMBER 60))
TemporalRelation

MonthFn Year PositiveInteger Month 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
(=>
(instance (MonthFn ?NUMBER ?YEAR) Month)
(lessThanOrEqualTo ?NUMBER 12))
TemporalRelation

RelativeComplementFn Class Class Class 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
(equal (RelativeComplementFn ?CLASS1 ?CLASS2)
(IntersectionFn ?CLASS1 (ComplementFn ?CLASS2)))
BinaryFunction

RemainderFn Quantity Quantity Quantity (RemainderFn ?NUMBER ?DIVISOR) is the remainder of the number ?NUMBER divided by the number ?DIVISOR. The result has the same sign as ?DIVISOR
(=>
(instance ?NUMBER OddInteger)
(equal (RemainderFn ?NUMBER 2) 1))
RelationExtendedToQuantities

SecondFn Minute PositiveRealNumber Second 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
(=>
(instance (SecondFn ?NUMBER ?MINUTE) Second)
(lessThan ?NUMBER 60))
TemporalRelation

UnionFn Class Class Class 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
(<=>
(instance ?ENTITY (UnionFn ?CLASS1 ?CLASS2))
(or
(instance ?ENTITY ?CLASS1)
(instance ?ENTITY ?CLASS2)))
BinaryFunction

WhereFn TimePoint Physical Region Maps an Object and a TimePoint at which the Object exists to the Region where the Object existed at that TimePoint
(=>
(origin ?PROCESS ?OBJ)
(located (WhereFn ?PROCESS (BeginFn (WhenFn ?PROCESS))) (WhereFn ?OBJ (BeginFn (WhenFn ?OBJ)))))
SpatialRelation WhenFn

Subject	have domain2	have domain1	partition into	have range	documentation	have axiom	is a kind of	is an instance of	have relatedInternalConcept
AssociativeFunction					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	(=> (instance ?FUNCTION AssociativeFunction) (forall (?INST1 ?INST2 ?INST3) (=> (and (instance ?INST1 (DomainFn ?FUNCTION)) (instance ?INST2 (DomainFn ?FUNCTION)) (instance ?INST3 (DomainFn ?FUNCTION))) (equal (AssignmentFn ?FUNCTION ?INST1 (AssignmentFn ?FUNCTION ?INST1 ?INST2)) (AssignmentFn ?FUNCTION (AssignmentFn ?FUNCTION ?INST1 ?INST2) ?INST3)))))	BinaryFunction
CommutativeFunction					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	(=> (instance ?FUNCTION CommutativeFunction) (forall (?INST1 ?INST2) (=> (and (instance ?INST1 (DomainFn ?FUNCTION)) (instance ?INST2 (DomainFn ?FUNCTION))) (equal (AssignmentFn ?FUNCTION ?INST1 ?INST2) (AssignmentFn ?FUNCTION ?INST2 ?INST1)))))	BinaryFunction
DayFn	Month	PositiveInteger		Day	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	(=> (instance (DayFn ?NUMBER ?MONTH) Day) (lessThanOrEqualTo ?NUMBER 31))		TemporalRelation
DensityFn	VolumeMeasure	MassMeasure	ConstantQuantity, FunctionQuantity	DensityMeasure	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	(=> (instance ?FUNCTION BinaryFunction) (valence ?FUNCTION 2))		DensityMeasure
ExponentiationFn	Integer	Quantity		Quantity	(ExponentiationFn ?NUMBER ?INT) returns the RealNumber ?NUMBER raised to the power of the Integer ?INT	(equal (ReciprocalFn ?NUMBER) (ExponentiationFn ?NUMBER -1))		RelationExtendedToQuantities
HourFn	Day	PositiveRealNumber		Hour	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	(=> (instance (HourFn ?NUMBER ?DAY) Hour) (lessThan ?NUMBER 24))		TemporalRelation
HourIntervalFn	PositiveRealNumber	PositiveRealNumber		TimeInterval	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	(=> (instance ?INTERVAL (HourIntervalFn ?NUMBER1 ?NUMBER2)) (and (lessThan ?NUMBER1 24) (lessThan ?NUMBER2 24) (lessThan ?NUMBER1 ?NUMBER2)))		TemporalRelation
IntersectionFn	Class	Class		Class	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	(equal (RelativeComplementFn ?CLASS1 ?CLASS2) (IntersectionFn ?CLASS1 (ComplementFn ?CLASS2)))		BinaryFunction
KappaFn	Formula	SymbolicString		Class	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	(=> (instance ?FUNCTION BinaryFunction) (valence ?FUNCTION 2))		BinaryFunction
LogFn	PositiveInteger	RealNumber		RealNumber	(LogFn ?NUMBER ?INT) returns the logarithm of the RealNumber ?NUMBER in the base denoted by the Integer ?INT	(=> (instance ?FUNCTION BinaryFunction) (valence ?FUNCTION 2))		BinaryFunction
MeasureFn	UnitOfMeasure	RealNumber		ConstantQuantity	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)	(equal (MeasureFn ?NUMBER YearDuration) (MeasureFn (MultiplicationFn ?NUMBER 365) DayDuration))		BinaryFunction
MereologicalDifferenceFn	Object	Object		Object	(MereologicalDifferenceFn ?OBJ1 ?OBJ2) denotes the Object consisting of the parts which belong to ?OBJ1 and not to ?OBJ2	(=> (equal ?OBJ3 (MereologicalDifferenceFn ?OBJ1 ?OBJ2)) (forall (?PART) (<=> (part ?PART ?OBJ3) (and (part ?PART ?OBJ1) (not (part ?PART ?OBJ2))))))		SpatialRelation
MereologicalProductFn	Object	Object		Object	(MereologicalProductFn ?OBJ1 ?OBJ2) denotes the Object consisting of the parts which belong to both ?OBJ1 and ?OBJ2	(=> (equal ?OBJ3 (MereologicalProductFn ?OBJ1 ?OBJ2)) (forall (?PART) (<=> (part ?PART ?OBJ3) (and (part ?PART ?OBJ1) (part ?PART ?OBJ2)))))		SpatialRelation	MereologicalDifferenceFn
MereologicalSumFn	Object	Object		Object	(MereologicalSumFn ?OBJ1 ?OBJ2) denotes the Object consisting of the parts which belong to either ?OBJ1 or ?OBJ2	(=> (equal ?OBJ3 (MereologicalSumFn ?OBJ1 ?OBJ2)) (forall (?PART) (<=> (part ?PART ?OBJ3) (or (part ?PART ?OBJ1) (part ?PART ?OBJ2)))))		SpatialRelation	MereologicalProductFn
MinuteFn	Hour	PositiveRealNumber		Minute	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	(=> (instance (MinuteFn ?NUMBER ?HOUR) Minute) (lessThan ?NUMBER 60))		TemporalRelation
MonthFn	Year	PositiveInteger		Month	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	(=> (instance (MonthFn ?NUMBER ?YEAR) Month) (lessThanOrEqualTo ?NUMBER 12))		TemporalRelation
RelativeComplementFn	Class	Class		Class	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	(equal (RelativeComplementFn ?CLASS1 ?CLASS2) (IntersectionFn ?CLASS1 (ComplementFn ?CLASS2)))		BinaryFunction
RemainderFn	Quantity	Quantity		Quantity	(RemainderFn ?NUMBER ?DIVISOR) is the remainder of the number ?NUMBER divided by the number ?DIVISOR. The result has the same sign as ?DIVISOR	(=> (instance ?NUMBER OddInteger) (equal (RemainderFn ?NUMBER 2) 1))		RelationExtendedToQuantities
SecondFn	Minute	PositiveRealNumber		Second	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	(=> (instance (SecondFn ?NUMBER ?MINUTE) Second) (lessThan ?NUMBER 60))		TemporalRelation
UnionFn	Class	Class		Class	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	(<=> (instance ?ENTITY (UnionFn ?CLASS1 ?CLASS2)) (or (instance ?ENTITY ?CLASS1) (instance ?ENTITY ?CLASS2)))		BinaryFunction
WhereFn	TimePoint	Physical		Region	Maps an Object and a TimePoint at which the Object exists to the Region where the Object existed at that TimePoint	(=> (origin ?PROCESS ?OBJ) (located (WhereFn ?PROCESS (BeginFn (WhenFn ?PROCESS))) (WhereFn ?OBJ (BeginFn (WhenFn ?OBJ)))))		SpatialRelation	WhenFn

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