Zvolte jazyk: english | cesky | deutsch | italiano | simplified chinese | traditional chinese | hindi Koncept: Anglické slovo: Hlavní stránka

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

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)

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

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

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

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

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

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

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

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

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

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