GrössteGemeinsamerTeilerFn (GreatestCommonDivisorFn)

(GreatestCommonDivisorFn number1 number2 ... number) returns the greatest common divisor of number1 through number.

Ontology

SUMO / NUMERIC-FUNCTIONS

Class(es)

Kategorie

inheritable relation

Funktion

Relation mit veränderlicher Anzahl Argumente
is instance of

GrössteGemeinsamerTeilerFn

Coordinate term(s)

AssignmentFn KleinsteGemeinsameVielfacheFn ListeFn konträresAttribut disjunkteAufspaltung disjunkteRelation exhaustive attribute vollständigeAufspaltung gilt fach

Axioms (2)

wenn "die größte gemeinsamer teiler von " ist gleich number ,
dann für jeden element gilt: wenn element ist ein Mitglied von "()", dann "element betrag number" ist gleich

(=>
      (equal
            (GreatestCommonDivisorFn @ROW)
            ?NUMBER)
      (forall
            (?ELEMENT)
            (=>
                  (inList
                        ?ELEMENT
                        (ListFn @ROW))
                  (equal
                        (RemainderFn ?ELEMENT ?NUMBER)
                        0))))

wenn "die größte gemeinsamer teiler von " ist gleich number ,
dann es gibt kein greater der greater ist grösserAls number und für jeden element gilt: wenn element ist ein Mitglied von "()", dann "element betrag greater" ist gleich

(=>
      (equal
            (GreatestCommonDivisorFn @ROW)
            ?NUMBER)
      (not
            (exists
                  (?GREATER)
                  (and
                        (greaterThan ?GREATER ?NUMBER)
                        (forall
                              (?ELEMENT)
                              (=>
                                    (inList
                                          ?ELEMENT
                                          (ListFn @ROW))
                                    (equal
                                          (RemainderFn ?ELEMENT ?GREATER)
                                          0)))))))