Select language: english | cesky | deutsch | italiano | simplified chinese | traditional chinese | hindi Concept: English word: Home

# 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)

 Classe

inheritable relation

Funzione

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)

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

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

Se e ? sono disgiunti e rel é un é membro di "(", allora rel é un' istanza di Relazione.
```(=>
(and
(disjointRelation @ROW)
(inList
?REL
(ListFn @ROW)))
(instance ?REL Relation))```

Se e ? sono disgiunti e rel1 é un é membro di "(" e rel2 é un é membro di "(" e rel1 %&ha number argomento(s, allora rel2 %&ha number argomento(s.
```(=>
(and
(disjointRelation @ROW)
(inList
?REL1
(ListFn @ROW))
(inList
?REL2
(ListFn @ROW))
(valence ?REL1 ?NUMBER))
(valence ?REL2 ?NUMBER))```

Se e ? sono disgiunti e rel1 é un é membro di "(" e rel2 é un é membro di "(" e rel1 is not uguale a rel2 e rel1( vales, allora rel2( non vale.
```(=>
(and
(disjointRelation @ROW1)
(inList
?REL1
(ListFn @ROW1))
(inList
?REL2
(ListFn @ROW1))
(not
(equal ?REL1 ?REL2))
(holds ?REL1 @ROW2))
(not
(holds ?REL2 @ROW2)))```

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

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

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

• se exhaustive attribute(class,) vale,
• allora per ogni obj vale: se attr1 é un' istanza di class, allora esiste attr2 tale che attr2 é un é membro di "(" e attr1 is uguale a attr2
• .
```(=>
(exhaustiveAttribute ?CLASS @ROW)
(forall
(?OBJ)
(=>
(instance ?ATTR1 ?CLASS)
(exists
(?ATTR2)
(and
(inList
?ATTR2
(ListFn @ROW))
(equal ?ATTR1 ?ATTR2))))))```

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

• se é scomposto disgiuntivamente in ,
• allora se element é un é membro di "(", allora element é un' istanza di Classe
• .
```(=>
(disjointDecomposition @ROW)
(=>
(inList
?ELEMENT
(ListFn @ROW))
(instance ?ELEMENT Class)))```

rel é un' istanza di RelazioneAValoreTotale se e solo se esiste valence tale che rel é un' istanza di Relazione e rel %&ha valence argomento(s e
• se per ogni number,element,class vale: se number é meno divalence e il numero number argomenti di rel é un istanza di class e element is uguale a "numberth elemento di "("", allora element é un' istanza di class,
• allora esiste item tale che rel(,item vales
• .
```(<=>
(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))))))```

Se rel é un' istanza di intentional relation e rel(agent, vales e obj é un é membro di "(", allora agent é interessato a obj.
```(=>
(and
(instance ?REL IntentionalRelation)
(holds ?REL ?AGENT @ROW)
(inList
?OBJ
(ListFn @ROW)))
(inScopeOfInterest ?AGENT ?OBJ))```

• se class é coperto da ,
• allora per ogni obj vale: se obj é un' istanza di class, allora esiste item tale che item é un é membro di "(" e obj é un' istanza di item
• .
```(=>
(exhaustiveDecomposition ?CLASS @ROW)
(forall
(?OBJ)
(=>
(instance ?OBJ ?CLASS)
(exists
(?ITEM)
(and
(inList
?ITEM
(ListFn @ROW))
(instance ?OBJ ?ITEM))))))```

• se class é scomposto disgiuntivamente in ,
• allora per ogni item vale: se item é un é membro di "(", allora item é una sottoclasse di class
• .
```(=>
(disjointDecomposition ?CLASS @ROW)
(forall
(?ITEM)
(=>
(inList
?ITEM
(ListFn @ROW))
(subclass ?ITEM ?CLASS))))```

• se class é scomposto disgiuntivamente in ,
• allora per ogni item1,item2 vale: se item1 é un é membro di "(" e item2 é un é membro di "(" e item1 is not uguale a item2, allora item1 é disgiunto da item2
• .
```(=>
(disjointDecomposition ?CLASS @ROW)
(forall
(?ITEM1 ?ITEM2)
(=>
(and
(inList
?ITEM1
(ListFn @ROW))
(inList
?ITEM2
(ListFn @ROW))
(not
(equal ?ITEM1 ?ITEM2)))
(disjoint ?ITEM1 ?ITEM2))))```

Se il numero number argomenti di rel é un istanza di class e rel( vales, allora "numberth elemento di "("" é un' istanza di class.
```(=>
(and
(domain ?REL ?NUMBER ?CLASS)
(holds ?REL @ROW))
(instance
(ListOrderFn
(ListFn @ROW)
?NUMBER)
?CLASS))```

Se il numero number argomento rel é una sottoclasse diclass e rel( vales, allora "numberth elemento di "("" é una sottoclasse di class.
```(=>
(and
(domainSubclass ?REL ?NUMBER ?CLASS)
(holds ?REL @ROW))
(subclass
(ListOrderFn
(ListFn @ROW)
?NUMBER)
?CLASS))```

"lunghezza di "(,item"" is uguale a "("lunghezza di "(""+1".
```(equal
(ListLengthFn
(ListFn @ROW ?ITEM))
(SuccessorFn
(ListLengthFn
(ListFn @ROW))))```

""lunghezza di "(,item""th elemento di "(,item"" is uguale a item.
```(equal
(ListOrderFn
(ListFn @ROW ?ITEM)
(ListLengthFn
(ListFn @ROW ?ITEM)))
?ITEM)```

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

"(" inizias "(,item".
```(initialList
(ListFn @ROW)
(ListFn @ROW ?ITEM))```

• se "il massimo comune divisore di" is uguale a number,
• allora per ogni element vale: se element é un é membro di "(", allora "element mod number" is uguale a
• .
```(=>
(equal
(GreatestCommonDivisorFn @ROW)
?NUMBER)
(forall
(?ELEMENT)
(=>
(inList
?ELEMENT
(ListFn @ROW))
(equal
(RemainderFn ?ELEMENT ?NUMBER)
0))))```

• se "il massimo comune divisore di" is uguale a number,
• allora non esiste greater tale che greater é più grande di number e per ogni element vale: se element é un é membro di "(", allora "element mod greater" is uguale a
• .
```(=>
(equal
(GreatestCommonDivisorFn @ROW)
?NUMBER)
(not
(exists
(?GREATER)
(and
(greaterThan ?GREATER ?NUMBER)
(forall
(?ELEMENT)
(=>
(inList
?ELEMENT
(ListFn @ROW))
(equal
(RemainderFn ?ELEMENT ?GREATER)
0)))))))```

• se "il minimo comune multiplo di " is uguale a number,
• allora per ogni element vale: se element é un é membro di "(", allora "number mod element" is uguale a
• .
```(=>
(equal
(LeastCommonMultipleFn @ROW)
?NUMBER)
(forall
(?ELEMENT)
(=>
(inList
?ELEMENT
(ListFn @ROW))
(equal
(RemainderFn ?NUMBER ?ELEMENT)
0))))```

• se "il minimo comune multiplo di " is uguale a number,
• allora non esiste less tale che less é meno dinumber e per ogni element vale: se element é un é membro di "(", allora "less mod element" is uguale a
• .
```(=>
(equal
(LeastCommonMultipleFn @ROW)
?NUMBER)
(not
(exists
(?LESS)
(and
(lessThan ?LESS ?NUMBER)
(forall
(?ELEMENT)
(=>
(inList
?ELEMENT
(ListFn @ROW))
(equal
(RemainderFn ?LESS ?ELEMENT)
0)))))))```

Se obj1 é attr1 a obj2 e é opposto a ? e attr1 é un é membro di "(" e attr2 é un é membro di "(" e attr1 is not uguale a attr2, allora obj1 é not attr2 a 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)))```