list fn (ListFn)

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

Ontology

SUMO / BASE-ONTOLOGY

Class(es)

class

inheritable relation

function

variable arity relation
is instance of

list fn

Coordinate term(s)

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

Axioms (27)

if obj1 is equal to obj2,
then if obj1 is equal to "numberth element of "()"" and obj2 is equal to "numberth element of "()"" and "()" is equal to "()", then () holds if and only if () 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))))

if list1 is equal to list2,
then if list1 is equal to "()" and list2 is equal to "()", then for all number holds: "numberth element of "()"" is equal to "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)))))

If and ? are disjoint and rel is a member of "()", then rel is an instance of relation.

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

If and ? are disjoint and rel1 is a member of "()" and rel2 is a member of "()" and rel1 %&has number argument(s), then rel2 %&has number argument(s).

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

If and ? are disjoint and rel1 is a member of "()" and rel2 is a member of "()" and rel1 is not equal to rel2 and rel1() holds, then 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)))

if is opposed to ?,
then if element is a member of "()", then element is an instance of attribute

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

if is opposed to ?,
then for all attr1,attr2 holds:
- if attr1 is equal to "number1th element of "()"" and attr2 is equal to "number2th element of "()"" and number1 is not equal to number2,
- then if obj has an attribute attr1, then obj has not an attribute 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))))))

if exhaustive attribute(class,) holds,
then if attr is a member of "()", then attr is an instance of attribute

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

if exhaustive attribute(class,) holds,
then for all obj holds: if attr1 is an instance of class, then there exists attr2 so that attr2 is a member of "()" and attr1 is equal to attr2

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

if is covered by ,
then if element is a member of "()", then element is an instance of class

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

if is disjointly decomposed into ,
then if element is a member of "()", then element is an instance of class

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

rel is an instance of total valued relation if and only if there exists valence so that rel is an instance of relation and rel %&has valence argument(s) and

if for all number,element,class holds: if number is less than valence and the number number argument of rel is an instance of class and element is equal to "numberth element of "()"", then element is an instance of class,
then there exists item so that 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))))))

If rel is an instance of intentional relation and rel(agent,) holds and obj is a member of "()", then agent is interested in obj.

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

if class is covered by ,
then for all obj holds: if obj is an instance of class, then there exists item so that item is a member of "()" and obj is an instance of item

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

if class is disjointly decomposed into ,
then for all item holds: if item is a member of "()", then item is a subclass of class

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

if class is disjointly decomposed into ,
then for all item1,item2 holds: if item1 is a member of "()" and item2 is a member of "()" and item1 is not equal to item2, then item1 is 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))))

If the number number argument of rel is an instance of class and rel() holds, then "numberth element of "()"" is an instance of class.

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

If the number number argument of rel is a subclass of class and rel() holds, then "numberth element of "()"" is a subclass of class.

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

"length of "(,item)"" is equal to "("length of "()""+1)".

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

""length of "(,item)""th element of "(,item)"" is equal to item.

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

if rel %&has number argument(s),
then for all holds: if rel() holds, then "length of "()"" is equal to number

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

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

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

if "the greatest common divisor of " is equal to number,
then for all element holds: if element is a member of "()", then "element mod number" is equal to

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

if "the greatest common divisor of " is equal to number,
then there doesn't exist greater so that greater is greater than number and for all element holds: if element is a member of "()", then "element mod greater" is equal to

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

if "the least common multiple of " is equal to number,
then for all element holds: if element is a member of "()", then "number mod element" is equal to

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

if "the least common multiple of " is equal to number,
then there doesn't exist less so that less is less than number and for all element holds: if element is a member of "()", then "less mod element" is equal to

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

If obj1 is attr1 to obj2 and is opposed to ? and attr1 is a member of "()" and attr2 is a member of "()" and attr1 is not equal to attr2, then obj1 is not attr2 to 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)))