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.

Ontology

SUMO / STRUCTURAL-ONTOLOGY

Class(es)

Classe

inheritable relation

Funzione

RelazioneAdAritáVariabile
is instance of

assignment fn

Coordinate term(s)

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

Type restrictions

Entitá AssignmentFn(Funzione)

Axioms (10)

Se rango di function é un'istanza di class e "function(" is uguale a value, allora value é un' istanza di class.

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

Se i valori resi da function sono sottoclassi diclass e "function(" is uguale a value, allora value é una sottoclasse di class.

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

Se rel(,inst vales e rel é un' istanza di Funzione, allora "rel(" is uguale a inst.

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

se fun é un' istanza di FunzioneUnoAUno,
allora per ogni arg1,arg2 vale: se il numero argomenti di fun é un istanza di class e arg1 é un' istanza di class e arg2 é un' istanza di class e arg1 is not uguale a arg2, allora "fun(arg1" is not uguale a "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))))))

se function é un' istanza di FunzioneAssociativa,
allora per ogni inst1,inst2,inst3 vale: se il numero argomenti di function é un istanza di class e inst1 é un' istanza di class e inst2 é un' istanza di class e inst3 é un' istanza di class, allora "function(inst1,"function(inst2,inst3"" is uguale a "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)))))

se function é un' istanza di FunzioneCommutativa,
allora per ogni inst1,inst2 vale: se il numero argomenti di function é un istanza di class e inst1 é un' istanza di class e inst2 é un' istanza di class, allora "function(inst1,inst2" is uguale a "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)))))

se function is closed on class e function é un' istanza di FunzioneUnaria,
allora per ogni inst vale: se inst é un' istanza di class, allora "function(inst" é un' istanza di class

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

se function is closed on class e function é un' istanza di FunzioneBinaria,
allora per ogni inst1,inst2 vale: se inst1 é un' istanza di class e inst2 é un' istanza di class, allora "function(inst1,inst2" é un' istanza di class

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

se function1 é distributivo su function2,
allora per ogni inst1,inst2,inst3 vale: se il numero argomenti di function1 é un istanza di class1 e inst1 é un' istanza di class1 e inst2 é un' istanza di class1 e inst3 é un' istanza di class1 e il numero argomenti di function2 é un istanza di class2 e inst1 é un' istanza di class2 e inst2 é un' istanza di class2 e inst3 é un' istanza di class2, allora "function1(inst1,"function2(inst2,inst3"" is uguale a "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))))))

se id é un elemento di identitá di function,
allora per ogni inst vale: se il numero argomenti di function é un istanza di class e inst é un' istanza di class, allora "function(id,inst" is uguale a inst

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