 SUMO   View all facts   Glossary   Help Entity > Abstract > Class > Relation > Function > AssignmentFn
Next FunctionBinaryFunction    UpFunction, VariableArityRelation    Previous FunctionUnaryFunction  AssignmentFn subject fact
 AssignmentFn documentation If F is a function with a value for the objects denoted by N1,..., NK, then the term (AssignmentFn F N1 ... NK) denotes the value of applying F to the objects denoted by N1,..., NK. Otherwise, the value is undefined has axiom `(<=> (instance ?FUN OneToOneFunction) (forall (?ARG1 ?ARG2) (=> (and (instance ?ARG1 (DomainFn ?FUN)) (instance ?ARG2 (DomainFn ?FUN)) (not (equal ?ARG1 ?ARG2))) (not (equal (AssignmentFn ?FUN ?ARG1) (AssignmentFn ?FUN ?ARG2))))))` has axiom `(<=> (and (holds ?REL ?INST1 ?INST2 ?INST3) (instance ?REL BinaryFunction)) (equal (AssignmentFn ?REL ?INST1 ?INST2) ?INST3))` has axiom `(<=> (and (holds ?REL ?INST1 ?INST2 ?INST3 ?INST4) (instance ?REL TernaryFunction)) (equal (AssignmentFn ?REL ?INST1 ?INST2 ?INST3) ?INST4))` has axiom `(<=> (and (holds ?REL ?INST1 ?INST2 ?INST3 ?INST4 ?INST5) (instance ?REL QuaternaryFunction)) (equal (AssignmentFn ?REL ?INST1 ?INST2 ?INST3 ?INST4) ?INST5))` has axiom `(<=> (and (holds ?REL ?INST1 ?INST2) (instance ?REL UnaryFunction)) (equal (AssignmentFn ?REL ?INST1) ?INST2))` has axiom `(=> (and (closedOn ?FUNCTION ?CLASS) (instance ?FUNCTION UnaryFunction)) (forall (?INST) (=> (instance ?INST ?CLASS) (instance (AssignmentFn ?FUNCTION ?INST) ?CLASS))))` 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 `(=> (and (instance ?FUNCTION TernaryFunction) (equal (AssignmentFn ?FUNCTION ?ARG1 ?ARG2 ?ARG3) ?VALUE1) (equal (AssignmentFn ?FUNCTION ?ARG1 ?ARG2 ?ARG3) ?VALUE2)) (equal ?VALUE1 ?VALUE2))` has axiom `(=> (and (instance ?FUNCTION UnaryFunction) (equal (AssignmentFn ?FUNCTION ?ARG) ?VALUE1) (equal (AssignmentFn ?FUNCTION ?ARG) ?VALUE2)) (equal ?VALUE1 ?VALUE2))` has axiom `(=> (distributes ?FUNCTION1 ?FUNCTION2) (forall (?INST1 ?INST2 ?INST3) (=> (and (instance ?INST1 (DomainFn ?FUNCTION1)) (instance ?INST2 (DomainFn ?FUNCTION1)) (instance ?INST3 (DomainFn ?FUNCTION1)) (instance ?INST1 (DomainFn ?FUNCTION2)) (instance ?INST2 (DomainFn ?FUNCTION2)) (instance ?INST3 (DomainFn ?FUNCTION2))) (equal (AssignmentFn ?FUNCTION1 ?INST1 (AssignmentFn ?FUNCTION2 ?INST2 ?INST3)) (AssignmentFn ?FUNCTION2 (AssignmentFn ?FUNCTION1 ?INST1 ?INST2) (AssignmentFn ?FUNCTION1 ?INST1 ?INST3))))))` has axiom `(=> (identityElement ?FUNCTION ?ID) (forall (?INST) (=> (instance ?INST (DomainFn ?FUNCTION)) (equal (AssignmentFn ?FUNCTION ?ID ?INST) ?INST))))` has axiom `(=> (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)))))` has axiom `(=> (instance ?FUNCTION CommutativeFunction) (forall (?INST1 ?INST2) (=> (and (instance ?INST1 (DomainFn ?FUNCTION)) (instance ?INST2 (DomainFn ?FUNCTION))) (equal (AssignmentFn ?FUNCTION ?INST1 ?INST2) (AssignmentFn ?FUNCTION ?INST2 ?INST1)))))` has domain1 Function has range Entity is an instance of Function is an instance of VariableArityRelation Function is first domain of AssignmentFn is first domain of closedOn is first domain of range is first domain of rangeSubclass Relation is second domain of subrelation Class is third domain of domain is third domain of domainSubclass Abstract is disjoint from Physical  Next FunctionBinaryFunction    UpFunction, VariableArityRelation    Previous FunctionUnaryFunction