list fn (ListFn)

A Function that takes any number of arguments and returns the List containing those arguments in exactly the same order.

Ontologie

SUMO / BASE-ONTOLOGY

Class(es)

třída

inheritable relation

funkce

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

list fn

Související termín(y)

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

Axiomy (27)

jestliže obj1 se rovná obj2,
potom jestliže obj1 se rovná "numberth element of "()"" a obj2 se rovná "numberth element of "()"" a "()" se rovná "()", potom () holds tehdy a jen tehdy pokud () holds

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

jestliže list1 se rovná list2,
potom jestliže list1 se rovná "()" a list2 se rovná "()", potom pro všechny number platí: "numberth element of "()"" se rovná "numberth element of "()""

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

Jestliže and ? are disjoint a rel je a member of "()", potom rel je instancí třídy relace.

(=>
      (and
            (disjointRelation @ROW)
            (inList
                  ?REL
                  (ListFn @ROW)))
      (instance ?REL Relation))

Jestliže and ? are disjoint a rel1 je a member of "()" a rel2 je a member of "()" a rel1 has number argument(s), potom rel2 has number argument(s).

(=>
      (and
            (disjointRelation @ROW)
            (inList
                  ?REL1
                  (ListFn @ROW))
            (inList
                  ?REL2
                  (ListFn @ROW))
            (valence ?REL1 ?NUMBER))
      (valence ?REL2 ?NUMBER))

Jestliže and ? are disjoint a rel1 je a member of "()" a rel2 je a member of "()" a rel1 se nerovná rel2 a rel1() holds, potom rel2() doesn't hold.

(=>
      (and
            (disjointRelation @ROW1)
            (inList
                  ?REL1
                  (ListFn @ROW1))
            (inList
                  ?REL2
                  (ListFn @ROW1))
            (not
                  (equal ?REL1 ?REL2))
            (holds ?REL1 @ROW2))
      (not
            (holds ?REL2 @ROW2)))

jestliže contrary attribute() platí,
potom jestliže element je a member of "()", potom element je instancí třídy atribut

(=>
      (contraryAttribute @ROW)
      (=>
            (inList
                  ?ELEMENT
                  (ListFn @ROW))
            (instance ?ELEMENT Attribute)))

jestliže contrary attribute() platí,
potom pro všechny attr1,attr2 platí:
- jestliže attr1 se rovná "number1th element of "()"" a attr2 se rovná "number2th element of "()"" a number1 se nerovná number2,
- potom jestliže obj má atribut attr1, potom obj nemá atribut attr2

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

jestliže exhaustive attribute(class,) platí,
potom jestliže attr je a member of "()", potom attr je instancí třídy atribut

(=>
      (exhaustiveAttribute ?CLASS @ROW)
      (=>
            (inList
                  ?ATTR
                  (ListFn @ROW))
            (instance ?ATTR Attribute)))

jestliže exhaustive attribute(class,) platí,
potom pro všechny obj platí: jestliže attr1 je instancí třídy class, potom existuje attr2 tak, že attr2 je a member of "()" a attr1 se rovná attr2

(=>
      (exhaustiveAttribute ?CLASS @ROW)
      (forall
            (?OBJ)
            (=>
                  (instance ?ATTR1 ?CLASS)
                  (exists
                        (?ATTR2)
                        (and
                              (inList
                                    ?ATTR2
                                    (ListFn @ROW))
                              (equal ?ATTR1 ?ATTR2))))))

jestliže je covered by ,
potom jestliže element je a member of "()", potom element je instancí třídy třída

(=>
      (exhaustiveDecomposition @ROW)
      (=>
            (inList
                  ?ELEMENT
                  (ListFn @ROW))
            (instance ?ELEMENT Class)))

jestliže je disjointly decomposed into ,
potom jestliže element je a member of "()", potom element je instancí třídy třída

(=>
      (disjointDecomposition @ROW)
      (=>
            (inList
                  ?ELEMENT
                  (ListFn @ROW))
            (instance ?ELEMENT Class)))

rel je instancí třídy úplná relace tehdy a jen tehdy pokud existuje valence tak, že rel je instancí třídy relace a rel has valence argument(s) a

jestliže pro všechny number,element,class platí: jestliže number je menší než valence a numberth argument of rel je an instance of class a element se rovná "numberth element of "()"", potom element je instancí třídy class,
potom existuje item tak, že rel(,item) holds

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

Jestliže rel je instancí třídy intentional relation a rel(agent,) holds a obj je a member of "()", potom agent je interested in obj.

(=>
      (and
            (instance ?REL IntentionalRelation)
            (holds ?REL ?AGENT @ROW)
            (inList
                  ?OBJ
                  (ListFn @ROW)))
      (inScopeOfInterest ?AGENT ?OBJ))

jestliže class je covered by ,
potom pro všechny obj platí: jestliže obj je instancí třídy class, potom existuje item tak, že item je a member of "()" a obj je instancí třídy item

(=>
      (exhaustiveDecomposition ?CLASS @ROW)
      (forall
            (?OBJ)
            (=>
                  (instance ?OBJ ?CLASS)
                  (exists
                        (?ITEM)
                        (and
                              (inList
                                    ?ITEM
                                    (ListFn @ROW))
                              (instance ?OBJ ?ITEM))))))

jestliže class je disjointly decomposed into ,
potom pro všechny item platí: jestliže item je a member of "()", potom item je podtřídou class

(=>
      (disjointDecomposition ?CLASS @ROW)
      (forall
            (?ITEM)
            (=>
                  (inList
                        ?ITEM
                        (ListFn @ROW))
                  (subclass ?ITEM ?CLASS))))

jestliže class je disjointly decomposed into ,
potom pro všechny item1,item2 platí: jestliže item1 je a member of "()" a item2 je a member of "()" a item1 se nerovná item2, potom item1 je disjoint from item2

(=>
      (disjointDecomposition ?CLASS @ROW)
      (forall
            (?ITEM1 ?ITEM2)
            (=>
                  (and
                        (inList
                              ?ITEM1
                              (ListFn @ROW))
                        (inList
                              ?ITEM2
                              (ListFn @ROW))
                        (not
                              (equal ?ITEM1 ?ITEM2)))
                  (disjoint ?ITEM1 ?ITEM2))))

Jestliže numberth argument of rel je an instance of class a rel() holds, potom "numberth element of "()"" je instancí třídy class.

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

Jestliže numberth argument of rel je a subclass of class a rel() holds, potom "numberth element of "()"" je podtřídou class.

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

"length of "(,item)"" se rovná "("length of "()""+1)".

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

""length of "(,item)""th element of "(,item)"" se rovná item.

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

jestliže rel has number argument(s),
potom pro všechny platí: jestliže rel() holds, potom "length of "()"" se rovná number

(=>
      (valence ?REL ?NUMBER)
      (forall
            (@ROW)
            (=>
                  (holds ?REL @ROW)
                  (equal
                        (ListLengthFn
                              (ListFn @ROW))
                        ?NUMBER))))

"()" starts "(,item)".

(initialList
      (ListFn @ROW)
      (ListFn @ROW ?ITEM))

jestliže "greatest common divisor fn()" se rovná number,
potom pro všechny element platí: jestliže element je a member of "()", potom "element mod number" se rovná

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

jestliže "greatest common divisor fn()" se rovná number,
potom neexistuje greater tak, že greater je větší než number a pro všechny element platí: jestliže element je a member of "()", potom "element mod greater" se rovná

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

jestliže "least common multiple fn()" se rovná number,
potom pro všechny element platí: jestliže element je a member of "()", potom "number mod element" se rovná

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

jestliže "least common multiple fn()" se rovná number,
potom neexistuje less tak, že less je menší než number a pro všechny element platí: jestliže element je a member of "()", potom "less mod element" se rovná

(=>
      (equal
            (LeastCommonMultipleFn @ROW)
            ?NUMBER)
      (not
            (exists
                  (?LESS)
                  (and
                        (lessThan ?LESS ?NUMBER)
                        (forall
                              (?ELEMENT)
                              (=>
                                    (inList
                                          ?ELEMENT
                                          (ListFn @ROW))
                                    (equal
                                          (RemainderFn ?LESS ?ELEMENT)
                                          0)))))))

Jestliže obj1 je attr1 vzhledem k obj2 a contrary attribute() platí a attr1 je a member of "()" a attr2 je a member of "()" a attr1 se nerovná attr2, potom obj1 není attr2 vzhledem k obj2.

(=>
      (and
            (orientation ?OBJ1 ?OBJ2 ?ATTR1)
            (contraryAttribute @ROW)
            (inList
                  ?ATTR1
                  (ListFn @ROW))
            (inList
                  ?ATTR2
                  (ListFn @ROW))
            (not
                  (equal ?ATTR1 ?ATTR2)))
      (not
            (orientation ?OBJ1 ?OBJ2 ?ATTR2)))