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-ONTOLOGYClass(es)
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)))
- se é opposto a ?,
- allora per ogni attr1,attr2 vale:
.
(=>
(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)))
