SUMO   View all facts   Glossary   Help Entity > Abstract > Class > Relation > Function > BinaryFunction
Next FunctionContinuousFunction    UpFunction, TernaryRelation    Previous FunctionAssignmentFn

 BinaryFunction comparison table
 have domain2 have domain1 partition into have range documentation have axiom is a kind of is an instance of have relatedInternalConcept Subject 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 FunctionContinuousFunction    UpFunction, TernaryRelation    Previous FunctionAssignmentFn