ListeOrdnungFn (ListOrderFn)

(ListOrderFn list number) denotes the item that is in the number position in the List list. For example, (ListOrderFn (ListFn Monday Tuesday Wednesday) 2) would return the value Tuesday.

Ontology

SUMO / BASE-ONTOLOGY

Class(es)

Kategorie

inheritable relation

zweistellige Funktion

ListeOrdnungFn

Coordinate term(s)

AdditionFn TagFn DichteFn DivisionFn AusgabeFn ExponentiationFn GraphPfadFn StundeFn DurchschnittFn AbstandFn KappaFn ListeVerkettenFn LogarithmusFn MaximumFn MaximalerBelasteterPfadFn MassFn MereologischeDifferenzFn MereologischesProduktFn MereologischeSummeFn MinumumFn MinimalerBelasteterPfadFn MinuteFn MonatFn MultiplikationFn PeriodikumAusgabeFn RückläufigeZeitAbstandFn RelativeErgänzungFn RelativeZeitFn RestFn SekundFn ReiheBandeFn GeschwindigkeitFn SubtraktionFn ZeitlicheAufbauFn ZeitabstandFn VereinigungFn WoFn

Type restrictions

Wesen ListOrderFn(Liste, positive Ganzzahl)

Related WordNet synsets

See more related synsets on a separate page.

Axioms (16)

wenn obj1 ist gleich obj2 ,
dann wenn obj1 ist gleich "numberte mitglied von "()"" und obj2 ist gleich "numberte mitglied von "()"" und "()" ist gleich "()" , dann () gilt nur wenn () gilt

(=>
      (equal ?OBJ1 ?OBJ2)
      (=>
            (and
                  (equal
                        ?OBJ1
                        (ListOrderFn
                              (ListFn @ROW1)
                              ?NUMBER))
                  (equal
                        ?OBJ2
                        (ListOrderFn
                              (ListFn @ROW2)
                              ?NUMBER))
                  (equal
                        (ListFn @ROW1)
                        (ListFn @ROW2)))
            (<=>
                  (holds @ROW1)
                  (holds @ROW2))))

wenn list1 ist gleich list2 ,
dann wenn list1 ist gleich "()" und list2 ist gleich "()" , dann für jeden number gilt: "numberte mitglied von "()"" ist gleich "numberte mitglied von "()""

(=>
      (equal ?LIST1 ?LIST2)
      (=>
            (and
                  (equal
                        ?LIST1
                        (ListFn @ROW1))
                  (equal
                        ?LIST2
                        (ListFn @ROW2)))
            (forall
                  (?NUMBER)
                  (equal
                        (ListOrderFn
                              (ListFn @ROW1)
                              ?NUMBER)
                        (ListOrderFn
                              (ListFn @ROW2)
                              ?NUMBER)))))

wenn wird ? entgegengesetzet ,
dann für jeden attr1,attr2 gilt:
- wenn attr1 ist gleich "number1te mitglied von "()"" und attr2 ist gleich "number2te mitglied von "()"" und number1 ist gleich number2 nicht,
- dann wenn obj hat ein attribut attr1 , dann obj hat ein attribut attr2 nicht

(=>
      (contraryAttribute @ROW)
      (forall
            (?ATTR1 ?ATTR2)
            (=>
                  (and
                        (equal
                              ?ATTR1
                              (ListOrderFn
                                    (ListFn @ROW)
                                    ?NUMBER1))
                        (equal
                              ?ATTR2
                              (ListOrderFn
                                    (ListFn @ROW)
                                    ?NUMBER2))
                        (not
                              (equal ?NUMBER1 ?NUMBER2)))
                  (=>
                        (property ?OBJ ?ATTR1)
                        (not
                              (property ?OBJ ?ATTR2))))))

rel ist ein fall von totalwertige Relation nur wenn es gibt ein valence der rel ist ein fall von Relation und rel hat valence argument(e) und

wenn für jeden number,element,class gilt: wenn number ist kleinerAls valence und die Zahl number Argument von rel ist ein fall von class und element ist gleich "numberte mitglied von "()"" , dann element ist ein fall von class ,
dann es gibt ein item der rel(,item) gilt

(<=>
      (instance ?REL TotalValuedRelation)
      (exists
            (?VALENCE)
            (and
                  (instance ?REL Relation)
                  (valence ?REL ?VALENCE)
                  (=>
                        (forall
                              (?NUMBER ?ELEMENT ?CLASS)
                              (=>
                                    (and
                                          (lessThan ?NUMBER ?VALENCE)
                                          (domain ?REL ?NUMBER ?CLASS)
                                          (equal
                                                ?ELEMENT
                                                (ListOrderFn
                                                      (ListFn @ROW)
                                                      ?NUMBER)))
                                    (instance ?ELEMENT ?CLASS)))
                        (exists
                              (?ITEM)
                              (holds ?REL @ROW ?ITEM))))))

wenn list ist ein fall von Liste ,
dann es gibt ein number1 der es gibt ein item1 der "number1te mitglied von list" ist gleich item1 nicht und für jeden number2 gilt: wenn number2 ist ein fall von positive Ganzzahl und number2 ist kleinerAls number1 , dann es gibt ein item2 der "number2te mitglied von list" ist gleich item2

(=>
      (instance ?LIST List)
      (exists
            (?NUMBER1)
            (exists
                  (?ITEM1)
                  (and
                        (not
                              (equal
                                    (ListOrderFn ?LIST ?NUMBER1)
                                    ?ITEM1))
                        (forall
                              (?NUMBER2)
                              (=>
                                    (and
                                          (instance ?NUMBER2 PositiveInteger)
                                          (lessThan ?NUMBER2 ?NUMBER1))
                                    (exists
                                          (?ITEM2)
                                          (equal
                                                (ListOrderFn ?LIST ?NUMBER2)
                                                ?ITEM2))))))))

list ist ein fall von einzigartige Liste nur wenn für jeden number1,number2 gilt: wenn "number1te mitglied von list" ist gleich "number2te mitglied von list" , dann number1 ist gleich number2 .

(<=>
      (instance ?LIST UniqueList)
      (forall
            (?NUMBER1 ?NUMBER2)
            (=>
                  (equal
                        (ListOrderFn ?LIST ?NUMBER1)
                        (ListOrderFn ?LIST ?NUMBER2))
                  (equal ?NUMBER1 ?NUMBER2))))

Wenn list1 ist ein fall von Liste und list2 ist ein fall von Liste und für jeden number gilt: "numberte mitglied von list1" ist gleich "numberte mitglied von list2" , dann list1 ist gleich list2 .

(=>
      (and
            (instance ?LIST1 List)
            (instance ?LIST2 List)
            (forall
                  (?NUMBER)
                  (equal
                        (ListOrderFn ?LIST1 ?NUMBER)
                        (ListOrderFn ?LIST2 ?NUMBER))))
      (equal ?LIST1 ?LIST2))

Wenn die Zahl number Argument von rel ist ein fall von class und rel() gilt , dann "numberte mitglied von "()"" ist ein fall von class .

(=>
      (and
            (domain ?REL ?NUMBER ?CLASS)
            (holds ?REL @ROW))
      (instance
            (ListOrderFn
                  (ListFn @ROW)
                  ?NUMBER)
            ?CLASS))

Wenn die Zahl number Argument von rel ist eine teilkategorie von class und rel() gilt , dann "numberte mitglied von "()"" ist eine teilkategorie von class.

(=>
      (and
            (domainSubclass ?REL ?NUMBER ?CLASS)
            (holds ?REL @ROW))
      (subclass
            (ListOrderFn
                  (ListFn @ROW)
                  ?NUMBER)
            ?CLASS))

Wenn "Länge von list" ist gleich number1 , dann für jeden number2 gilt: es gibt ein item der "number2te mitglied von list" ist gleich item nur wenn number2 ist kleinerAlsOderGleich number1 .

(=>
      (equal
            (ListLengthFn ?LIST)
            ?NUMBER1)
      (forall
            (?NUMBER2)
            (<=>
                  (exists
                        (?ITEM)
                        (equal
                              (ListOrderFn ?LIST ?NUMBER2)
                              ?ITEM))
                  (lessThanOrEqualTo ?NUMBER2 ?NUMBER1))))

""Länge von "(,item)""te mitglied von "(,item)"" ist gleich item .

(equal
      (ListOrderFn
            (ListFn @ROW ?ITEM)
            (ListLengthFn
                  (ListFn @ROW ?ITEM)))
      ?ITEM)

Wenn "Länge von list1" ist gleich number , dann es gibt ein list2 der list1 beginnt list2 und "(number+1)" ist gleich "Länge von list2" und ""(number+1)"te mitglied von list2" ist gleich item .

(=>
      (equal
            (ListLengthFn ?LIST1)
            ?NUMBER)
      (exists
            (?LIST2)
            (and
                  (initialList ?LIST1 ?LIST2)
                  (equal
                        (SuccessorFn ?NUMBER)
                        (ListLengthFn ?LIST2))
                  (equal
                        (ListOrderFn
                              ?LIST2
                              (SuccessorFn ?NUMBER))
                        ?ITEM))))

list3 ist gleich "die Liste bestanden aus list1 und list2" nur wenn für jeden number1,number2 gilt: wenn number1 ist kleinerAlsOderGleich "Länge von list1" und number2 ist kleinerAlsOderGleich "Länge von list2" und number1 ist ein fall von positive Ganzzahl und number2 ist ein fall von positive Ganzzahl , dann "number1te mitglied von list3" ist gleich "number1te mitglied von list1" und ""("Länge von list1"+number2)"te mitglied von list3" ist gleich "number2te mitglied von list2" .

(<=>
      (equal
            ?LIST3
            (ListConcatenateFn ?LIST1 ?LIST2))
      (forall
            (?NUMBER1 ?NUMBER2)
            (=>
                  (and
                        (lessThanOrEqualTo
                              ?NUMBER1
                              (ListLengthFn ?LIST1))
                        (lessThanOrEqualTo
                              ?NUMBER2
                              (ListLengthFn ?LIST2))
                        (instance ?NUMBER1 PositiveInteger)
                        (instance ?NUMBER2 PositiveInteger))
                  (and
                        (equal
                              (ListOrderFn ?LIST3 ?NUMBER1)
                              (ListOrderFn ?LIST1 ?NUMBER1))
                        (equal
                              (ListOrderFn
                                    ?LIST3
                                    (AdditionFn
                                          (ListLengthFn ?LIST1)
                                          ?NUMBER2))
                              (ListOrderFn ?LIST2 ?NUMBER2))))))

item ist ein Mitglied von list nur wenn es gibt ein number der "numberte mitglied von list" ist gleich item .

(<=>
      (inList ?ITEM ?LIST)
      (exists
            (?NUMBER)
            (equal
                  (ListOrderFn ?LIST ?NUMBER)
                  ?ITEM)))

wenn list1 ist eine teilliste von list2 ,
dann es gibt ein number3 der für jeden item gilt: wenn item ist ein Mitglied von list1, dann es gibt ein number1,number2 der "number1te mitglied von list1" ist gleich item und "number2te mitglied von list2" ist gleich item und number2 ist gleich "(number1+number3)"

(=>
      (subList ?LIST1 ?LIST2)
      (exists
            (?NUMBER3)
            (forall
                  (?ITEM)
                  (=>
                        (inList ?ITEM ?LIST1)
                        (exists
                              (?NUMBER1 ?NUMBER2)
                              (and
                                    (equal
                                          (ListOrderFn ?LIST1 ?NUMBER1)
                                          ?ITEM)
                                    (equal
                                          (ListOrderFn ?LIST2 ?NUMBER2)
                                          ?ITEM)
                                    (equal
                                          ?NUMBER2
                                          (AdditionFn ?NUMBER1 ?NUMBER3))))))))

wenn list1 beginnt list2 ,
dann für jeden number1,number2 gilt: wenn "Länge von list1" ist gleich number1 und number2 ist kleinerAlsOderGleich number1 , dann "number2te mitglied von list1" ist gleich "number2te mitglied von list2"

(=>
      (initialList ?LIST1 ?LIST2)
      (forall
            (?NUMBER1 ?NUMBER2)
            (=>
                  (and
                        (equal
                              (ListLengthFn ?LIST1)
                              ?NUMBER1)
                        (lessThanOrEqualTo ?NUMBER2 ?NUMBER1))
                  (equal
                        (ListOrderFn ?LIST1 ?NUMBER2)
                        (ListOrderFn ?LIST2 ?NUMBER2)))))