SUMO   View all facts   Glossary   Help
Entity > Abstract > Class > Relation > Function > AssignmentFn
Next Function: BinaryFunction    Up: Function, VariableArityRelation    Previous Function: UnaryFunction   

AssignmentFn
subjectfact 
AssignmentFndocumentation 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 undefined2001-11-30 13:33:38.0
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))))))
2001-11-30 13:33:38.0
has axiom 
(<=>
    (and
       (holds ?REL ?INST1 ?INST2 ?INST3)
       (instance ?REL BinaryFunction))
    (equal (AssignmentFn ?REL ?INST1 ?INST2) ?INST3))
2001-11-30 13:33:38.0
has axiom 
(<=>
    (and
       (holds ?REL ?INST1 ?INST2 ?INST3 ?INST4)
       (instance ?REL TernaryFunction))
    (equal (AssignmentFn ?REL ?INST1 ?INST2 ?INST3) ?INST4))
2001-11-30 13:33:38.0
has axiom 
(<=>
    (and
       (holds ?REL ?INST1 ?INST2 ?INST3 ?INST4 ?INST5)
       (instance ?REL QuaternaryFunction))
    (equal (AssignmentFn ?REL ?INST1 ?INST2 ?INST3 ?INST4) ?INST5))
2001-11-30 13:33:38.0
has axiom 
(<=>
    (and
       (holds ?REL ?INST1 ?INST2)
       (instance ?REL UnaryFunction))
    (equal (AssignmentFn ?REL ?INST1) ?INST2))
2001-11-30 13:33:39.0
has axiom 
(=>
    (and
       (closedOn ?FUNCTION ?CLASS)
       (instance ?FUNCTION UnaryFunction))
    (forall (?INST)
       (=> 
          (instance ?INST ?CLASS) 
          (instance (AssignmentFn ?FUNCTION ?INST) ?CLASS))))
2001-11-30 13:33:39.0
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:39.0
has axiom 
(=>
    (and
       (instance ?FUNCTION BinaryFunction)
       (equal (AssignmentFn ?FUNCTION ?ARG1 ?ARG2) ?VALUE1)
       (equal (AssignmentFn ?FUNCTION ?ARG1 ?ARG2) ?VALUE2))
    (equal ?VALUE1 ?VALUE2))
2001-11-30 13:33:39.0
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:39.0
has axiom 
(=>
    (and
       (instance ?FUNCTION TernaryFunction)
       (equal (AssignmentFn ?FUNCTION ?ARG1 ?ARG2 ?ARG3) ?VALUE1)
       (equal (AssignmentFn ?FUNCTION ?ARG1 ?ARG2 ?ARG3) ?VALUE2))
    (equal ?VALUE1 ?VALUE2))
2001-11-30 13:33:39.0
has axiom 
(=>
    (and
       (instance ?FUNCTION UnaryFunction)
       (equal (AssignmentFn ?FUNCTION ?ARG) ?VALUE1)
       (equal (AssignmentFn ?FUNCTION ?ARG) ?VALUE2))
    (equal ?VALUE1 ?VALUE2))
2001-11-30 13:33:39.0
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))))))
2001-11-30 13:33:39.0
has axiom 
(=>
    (identityElement ?FUNCTION ?ID)
    (forall (?INST)
       (=>
          (instance ?INST (DomainFn ?FUNCTION))
          (equal (AssignmentFn ?FUNCTION ?ID ?INST) ?INST))))
2001-11-30 13:33:39.0
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)))))
2001-11-30 13:33:39.0
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)))))
2001-11-30 13:33:39.0
has domain1 Function2001-11-30 13:33:39.0
has range Entity2001-11-30 13:33:39.0
is an instance of Function2001-11-30 13:33:39.0
is an instance of VariableArityRelation2001-11-30 13:33:39.0
Functionis first domain of AssignmentFn2001-11-30 13:34:18.0
is first domain of closedOn2001-11-30 13:34:18.0
is first domain of range2001-11-30 13:34:18.0
is first domain of rangeSubclass2001-11-30 13:34:18.0
Relationis second domain of subrelation2001-11-30 13:35:10.0
Classis third domain of domain2001-11-30 13:33:51.0
is third domain of domainSubclass2001-11-30 13:33:51.0
Abstractis disjoint from Physical2001-11-30 13:33:32.0

Next Function: BinaryFunction    Up: Function, VariableArityRelation    Previous Function: UnaryFunction