AssignmentFn (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)

Kategorie

inheritable relation

Funktion

Relation mit veränderlicher Anzahl Argumente
is instance of

AssignmentFn

Coordinate term(s)

GrössteGemeinsamerTeilerFn KleinsteGemeinsameVielfacheFn ListeFn konträresAttribut disjunkteAufspaltung disjunkteRelation exhaustive attribute vollständigeAufspaltung gilt fach

Type restrictions

Wesen AssignmentFn(Funktion)

Axioms (10)

Wenn bildbereich von function ist ein fall von class {nicht} und "function()" ist gleich value , dann value ist ein fall von class .

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

Wenn die werte die function zurückgibt sind teilkategorien von class und "function()" ist gleich value , dann value ist eine teilkategorie von class.

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

Wenn rel(,inst) gilt und rel ist ein fall von Funktion , dann "rel()" ist gleich inst .

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

wenn fun ist ein fall von eineindeutige Function ,
dann für jeden arg1,arg2 gilt: wenn die Zahl Argument von fun ist ein fall von class und arg1 ist ein fall von class und arg2 ist ein fall von class und arg1 ist gleich arg2 nicht, dann "fun(arg1)" ist gleich "fun(arg2)" nicht

(=>
      (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))))))

wenn function ist ein fall von associative Funktion ,
dann für jeden inst1,inst2,inst3 gilt: wenn die Zahl Argument von function ist ein fall von class und inst1 ist ein fall von class und inst2 ist ein fall von class und inst3 ist ein fall von class , dann "function(inst1,"function(inst2,inst3)")" ist gleich "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)))))

wenn function ist ein fall von commutative Funktion ,
dann für jeden inst1,inst2 gilt: wenn die Zahl Argument von function ist ein fall von class und inst1 ist ein fall von class und inst2 ist ein fall von class , dann "function(inst1,inst2)" ist gleich "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)))))

wenn function ist mit class aufgeschlossen und function ist ein fall von einstellige Funktion ,
dann für jeden inst gilt: wenn inst ist ein fall von class , dann "function(inst)" ist ein fall von class

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

wenn function ist mit class aufgeschlossen und function ist ein fall von zweistellige Funktion ,
dann für jeden inst1,inst2 gilt: wenn inst1 ist ein fall von class und inst2 ist ein fall von class , dann "function(inst1,inst2)" ist ein fall von class

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

wenn function1 ist distributiv über function2,
dann für jeden inst1,inst2,inst3 gilt: wenn die Zahl Argument von function1 ist ein fall von class1 und inst1 ist ein fall von class1 und inst2 ist ein fall von class1 und inst3 ist ein fall von class1 und die Zahl Argument von function2 ist ein fall von class2 und inst1 ist ein fall von class2 und inst2 ist ein fall von class2 und inst3 ist ein fall von class2 , dann "function1(inst1,"function2(inst2,inst3)")" ist gleich "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))))))

wenn id ist ein identitätsElement von function,
dann für jeden inst gilt: wenn die Zahl Argument von function ist ein fall von class und inst ist ein fall von class , dann "function(id,inst)" ist gleich inst

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