assignment fn (AssignmentFn)

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.

Ontologie

SUMO / STRUCTURAL-ONTOLOGY

Class(es)

třída

inheritable relation

funkce

relace s proměnným počtem argumentů
is instance of

assignment fn

Související termín(y)

greatest common divisor fn least common multiple fn list fn contrary attribute disjoint decomposition disjoint relation exhaustive attribute exhaustive decomposition holds partition

Typy argumentů

entita AssignmentFn(funkce)

Axiomy (10)

Jestliže range of function je an instance of class a "function()" se rovná value, potom value je instancí třídy class.

(=>
      (and
            (range ?FUNCTION ?CLASS)
            (equal
                  (AssignmentFn ?FUNCTION @ROW)
                  ?VALUE))
      (instance ?VALUE ?CLASS))

Jestliže range subclass(function,class) platí a "function()" se rovná value, potom value je podtřídou class.

(=>
      (and
            (rangeSubclass ?FUNCTION ?CLASS)
            (equal
                  (AssignmentFn ?FUNCTION @ROW)
                  ?VALUE))
      (subclass ?VALUE ?CLASS))

Jestliže rel(,inst) holds a rel je instancí třídy funkce, potom "rel()" se rovná inst.

(=>
      (and
            (holds ?REL @ROW ?INST)
            (instance ?REL Function))
      (equal
            (AssignmentFn ?REL @ROW)
            ?INST))

jestliže fun je instancí třídy prostá funkce na,
potom pro všechny arg1,arg2 platí: jestliže th argument of fun je an instance of class a arg1 je instancí třídy class a arg2 je instancí třídy class a arg1 se nerovná arg2, potom "fun(arg1)" se nerovná "fun(arg2)"

(=>
      (instance ?FUN OneToOneFunction)
      (forall
            (?ARG1 ?ARG2)
            (=>
                  (and
                        (domain ?FUN 1 ?CLASS)
                        (instance ?ARG1 ?CLASS)
                        (instance ?ARG2 ?CLASS)
                        (not
                              (equal ?ARG1 ?ARG2)))
                  (not
                        (equal
                              (AssignmentFn ?FUN ?ARG1)
                              (AssignmentFn ?FUN ?ARG2))))))

jestliže function je instancí třídy asociativní funkce,
potom pro všechny inst1,inst2,inst3 platí: jestliže th argument of function je an instance of class a inst1 je instancí třídy class a inst2 je instancí třídy class a inst3 je instancí třídy class, potom "function(inst1,"function(inst2,inst3)")" se rovná "function("function(inst1,inst2)",inst3)"

(=>
      (instance ?FUNCTION AssociativeFunction)
      (forall
            (?INST1 ?INST2 ?INST3)
            (=>
                  (and
                        (domain ?FUNCTION 1 ?CLASS)
                        (instance ?INST1 ?CLASS)
                        (instance ?INST2 ?CLASS)
                        (instance ?INST3 ?CLASS))
                  (equal
                        (AssignmentFn
                              ?FUNCTION
                              ?INST1
                              (AssignmentFn ?FUNCTION ?INST2 ?INST3))
                        (AssignmentFn
                              ?FUNCTION
                              (AssignmentFn ?FUNCTION ?INST1 ?INST2)
                              ?INST3)))))

jestliže function je instancí třídy komutativní funkce,
potom pro všechny inst1,inst2 platí: jestliže th argument of function je an instance of class a inst1 je instancí třídy class a inst2 je instancí třídy class, potom "function(inst1,inst2)" se rovná "function(inst2,inst1)"

(=>
      (instance ?FUNCTION CommutativeFunction)
      (forall
            (?INST1 ?INST2)
            (=>
                  (and
                        (domain ?FUNCTION 1 ?CLASS)
                        (instance ?INST1 ?CLASS)
                        (instance ?INST2 ?CLASS))
                  (equal
                        (AssignmentFn ?FUNCTION ?INST1 ?INST2)
                        (AssignmentFn ?FUNCTION ?INST2 ?INST1)))))

jestliže function je closed on class a function je instancí třídy unární funkce,
potom pro všechny inst platí: jestliže inst je instancí třídy class, potom "function(inst)" je instancí třídy class

(=>
      (and
            (closedOn ?FUNCTION ?CLASS)
            (instance ?FUNCTION UnaryFunction))
      (forall
            (?INST)
            (=>
                  (instance ?INST ?CLASS)
                  (instance
                        (AssignmentFn ?FUNCTION ?INST)
                        ?CLASS))))

jestliže function je closed on class a function je instancí třídy binární funkce,
potom pro všechny inst1,inst2 platí: jestliže inst1 je instancí třídy class a inst2 je instancí třídy class, potom "function(inst1,inst2)" je instancí třídy class

(=>
      (and
            (closedOn ?FUNCTION ?CLASS)
            (instance ?FUNCTION BinaryFunction))
      (forall
            (?INST1 ?INST2)
            (=>
                  (and
                        (instance ?INST1 ?CLASS)
                        (instance ?INST2 ?CLASS))
                  (instance
                        (AssignmentFn ?FUNCTION ?INST1 ?INST2)
                        ?CLASS))))

jestliže function1 je distributive over function2,
potom pro všechny inst1,inst2,inst3 platí: jestliže th argument of function1 je an instance of class1 a inst1 je instancí třídy class1 a inst2 je instancí třídy class1 a inst3 je instancí třídy class1 a th argument of function2 je an instance of class2 a inst1 je instancí třídy class2 a inst2 je instancí třídy class2 a inst3 je instancí třídy class2, potom "function1(inst1,"function2(inst2,inst3)")" se rovná "function2("function1(inst1,inst2)","function1(inst1,inst3)")"

(=>
      (distributes ?FUNCTION1 ?FUNCTION2)
      (forall
            (?INST1 ?INST2 ?INST3)
            (=>
                  (and
                        (domain ?FUNCTION1 1 ?CLASS1)
                        (instance ?INST1 ?CLASS1)
                        (instance ?INST2 ?CLASS1)
                        (instance ?INST3 ?CLASS1)
                        (domain ?FUNCTION2 1 ?CLASS2)
                        (instance ?INST1 ?CLASS2)
                        (instance ?INST2 ?CLASS2)
                        (instance ?INST3 ?CLASS2))
                  (equal
                        (AssignmentFn
                              ?FUNCTION1
                              ?INST1
                              (AssignmentFn ?FUNCTION2 ?INST2 ?INST3))
                        (AssignmentFn
                              ?FUNCTION2
                              (AssignmentFn ?FUNCTION1 ?INST1 ?INST2)
                              (AssignmentFn ?FUNCTION1 ?INST1 ?INST3))))))

jestliže id je an identity element of function,
potom pro všechny inst platí: jestliže th argument of function je an instance of class a inst je instancí třídy class, potom "function(id,inst)" se rovná inst

(=>
      (identityElement ?FUNCTION ?ID)
      (forall
            (?INST)
            (=>
                  (and
                        (domain ?FUNCTION 1 ?CLASS)
                        (instance ?INST ?CLASS))
                  (equal
                        (AssignmentFn ?FUNCTION ?ID ?INST)
                        ?INST))))