ListeFn (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)
AssignmentFn
GrössteGemeinsamerTeilerFn
KleinsteGemeinsameVielfacheFn
konträresAttribut
disjunkteAufspaltung
disjunkteRelation
exhaustive attribute
vollständigeAufspaltung
gilt
fach
Axioms (27)
- wenn obj1 ist gleich obj2 ,
- dann wenn obj1 ist gleich "numberte mitglied von "()"" und obj2 ist gleich "numberte mitglied von "()"" und "()" ist gleich "()" , dann () gilt nur wenn () gilt
.
(=>
(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))))
- wenn list1 ist gleich list2 ,
- dann wenn list1 ist gleich "()" und list2 ist gleich "()" , dann für jeden number gilt: "numberte mitglied von "()"" ist gleich "numberte mitglied von "()""
.
(=>
(equal ?LIST1 ?LIST2)
(=>
(and
(equal
?LIST1
(ListFn @ROW1))
(equal
?LIST2
(ListFn @ROW2)))
(forall
(?NUMBER)
(equal
(ListOrderFn
(ListFn @ROW1)
?NUMBER)
(ListOrderFn
(ListFn @ROW2)
?NUMBER)))))
Wenn und ? werden disjunkt und rel ist ein Mitglied von "()", dann rel ist ein fall von Relation .
(=>
(and
(disjointRelation @ROW)
(inList
?REL
(ListFn @ROW)))
(instance ?REL Relation))
Wenn und ? werden disjunkt und rel1 ist ein Mitglied von "()" und rel2 ist ein Mitglied von "()" und rel1 hat number argument(e), dann rel2 hat number argument(e).
(=>
(and
(disjointRelation @ROW)
(inList
?REL1
(ListFn @ROW))
(inList
?REL2
(ListFn @ROW))
(valence ?REL1 ?NUMBER))
(valence ?REL2 ?NUMBER))
Wenn und ? werden disjunkt und rel1 ist ein Mitglied von "()" und rel2 ist ein Mitglied von "()" und rel1 ist gleich rel2 nicht und rel1() gilt , dann rel2() gilt nicht.
(=>
(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)))
- wenn wird ? entgegengesetzet ,
- dann für jeden attr1,attr2 gilt:
- wenn attr1 ist gleich "number1te mitglied von "()"" und attr2 ist gleich "number2te mitglied von "()"" und number1 ist gleich number2 nicht,
- dann wenn obj hat ein attribut attr1 , dann obj hat ein attribut attr2 nicht
.
(=>
(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)))
- wenn exhaustive attribute(class,) gilt,
- dann für jeden obj gilt: wenn attr1 ist ein fall von class , dann es gibt ein attr2 der attr2 ist ein Mitglied von "()" und attr1 ist gleich attr2
.
(=>
(exhaustiveAttribute ?CLASS @ROW)
(forall
(?OBJ)
(=>
(instance ?ATTR1 ?CLASS)
(exists
(?ATTR2)
(and
(inList
?ATTR2
(ListFn @ROW))
(equal ?ATTR1 ?ATTR2))))))
- wenn wird mit behandelt,
- dann wenn element ist ein Mitglied von "()", dann element ist ein fall von Kategorie
.
(=>
(exhaustiveDecomposition @ROW)
(=>
(inList
?ELEMENT
(ListFn @ROW))
(instance ?ELEMENT Class)))
- wenn wird zusammenhanglos auf disjunkt,
- dann wenn element ist ein Mitglied von "()", dann element ist ein fall von Kategorie
.
(=>
(disjointDecomposition @ROW)
(=>
(inList
?ELEMENT
(ListFn @ROW))
(instance ?ELEMENT Class)))
rel ist ein fall von totalwertige Relation nur wenn es gibt ein valence der rel ist ein fall von Relation und rel hat valence argument(e) und - wenn für jeden number,element,class gilt: wenn number ist kleinerAls valence und die Zahl number Argument von rel ist ein fall von class und element ist gleich "numberte mitglied von "()"" , dann element ist ein fall von class ,
- dann es gibt ein item der rel(,item) gilt
.
(<=>
(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))))))
Wenn rel ist ein fall von intentional relation und rel(agent,) gilt und obj ist ein Mitglied von "()", dann agent ist an obj interessiert .
(=>
(and
(instance ?REL IntentionalRelation)
(holds ?REL ?AGENT @ROW)
(inList
?OBJ
(ListFn @ROW)))
(inScopeOfInterest ?AGENT ?OBJ))
- wenn class wird mit behandelt,
- dann für jeden obj gilt: wenn obj ist ein fall von class , dann es gibt ein item der item ist ein Mitglied von "()" und obj ist ein fall von item
.
(=>
(exhaustiveDecomposition ?CLASS @ROW)
(forall
(?OBJ)
(=>
(instance ?OBJ ?CLASS)
(exists
(?ITEM)
(and
(inList
?ITEM
(ListFn @ROW))
(instance ?OBJ ?ITEM))))))
- wenn class wird zusammenhanglos auf disjunkt,
- dann für jeden item gilt: wenn item ist ein Mitglied von "()", dann item ist eine teilkategorie von class
.
(=>
(disjointDecomposition ?CLASS @ROW)
(forall
(?ITEM)
(=>
(inList
?ITEM
(ListFn @ROW))
(subclass ?ITEM ?CLASS))))
- wenn class wird zusammenhanglos auf disjunkt,
- dann für jeden item1,item2 gilt: wenn item1 ist ein Mitglied von "()" und item2 ist ein Mitglied von "()" und item1 ist gleich item2 nicht, dann item1 ist dijunkt von item2
.
(=>
(disjointDecomposition ?CLASS @ROW)
(forall
(?ITEM1 ?ITEM2)
(=>
(and
(inList
?ITEM1
(ListFn @ROW))
(inList
?ITEM2
(ListFn @ROW))
(not
(equal ?ITEM1 ?ITEM2)))
(disjoint ?ITEM1 ?ITEM2))))
Wenn die Zahl number Argument von rel ist ein fall von class und rel() gilt , dann "numberte mitglied von "()"" ist ein fall von class .
(=>
(and
(domain ?REL ?NUMBER ?CLASS)
(holds ?REL @ROW))
(instance
(ListOrderFn
(ListFn @ROW)
?NUMBER)
?CLASS))
Wenn die Zahl number Argument von rel ist eine teilkategorie von class und rel() gilt , dann "numberte mitglied von "()"" ist eine teilkategorie von class.
(=>
(and
(domainSubclass ?REL ?NUMBER ?CLASS)
(holds ?REL @ROW))
(subclass
(ListOrderFn
(ListFn @ROW)
?NUMBER)
?CLASS))
"Länge von "(,item)"" ist gleich "("Länge von "()""+1)" .
(equal
(ListLengthFn
(ListFn @ROW ?ITEM))
(SuccessorFn
(ListLengthFn
(ListFn @ROW))))
""Länge von "(,item)""te mitglied von "(,item)"" ist gleich item .
(equal
(ListOrderFn
(ListFn @ROW ?ITEM)
(ListLengthFn
(ListFn @ROW ?ITEM)))
?ITEM)
- wenn rel hat number argument(e),
- dann für jeden gilt: wenn rel() gilt , dann "Länge von "()"" ist gleich number
.
(=>
(valence ?REL ?NUMBER)
(forall
(@ROW)
(=>
(holds ?REL @ROW)
(equal
(ListLengthFn
(ListFn @ROW))
?NUMBER))))
"()" beginnt "(,item)" .
(initialList
(ListFn @ROW)
(ListFn @ROW ?ITEM))
- wenn "die größte gemeinsamer teiler von " ist gleich number ,
- dann für jeden element gilt: wenn element ist ein Mitglied von "()", dann "element betrag number" ist gleich
.
(=>
(equal
(GreatestCommonDivisorFn @ROW)
?NUMBER)
(forall
(?ELEMENT)
(=>
(inList
?ELEMENT
(ListFn @ROW))
(equal
(RemainderFn ?ELEMENT ?NUMBER)
0))))
- wenn "die größte gemeinsamer teiler von " ist gleich number ,
- dann es gibt kein greater der greater ist grösserAls number und für jeden element gilt: wenn element ist ein Mitglied von "()", dann "element betrag greater" ist gleich
.
(=>
(equal
(GreatestCommonDivisorFn @ROW)
?NUMBER)
(not
(exists
(?GREATER)
(and
(greaterThan ?GREATER ?NUMBER)
(forall
(?ELEMENT)
(=>
(inList
?ELEMENT
(ListFn @ROW))
(equal
(RemainderFn ?ELEMENT ?GREATER)
0)))))))
- wenn "das kleinste gemeinsames vielfach von " ist gleich number ,
- dann für jeden element gilt: wenn element ist ein Mitglied von "()", dann "number betrag element" ist gleich
.
(=>
(equal
(LeastCommonMultipleFn @ROW)
?NUMBER)
(forall
(?ELEMENT)
(=>
(inList
?ELEMENT
(ListFn @ROW))
(equal
(RemainderFn ?NUMBER ?ELEMENT)
0))))
- wenn "das kleinste gemeinsames vielfach von " ist gleich number ,
- dann es gibt kein less der less ist kleinerAls number und für jeden element gilt: wenn element ist ein Mitglied von "()", dann "less betrag element" ist gleich
.
(=>
(equal
(LeastCommonMultipleFn @ROW)
?NUMBER)
(not
(exists
(?LESS)
(and
(lessThan ?LESS ?NUMBER)
(forall
(?ELEMENT)
(=>
(inList
?ELEMENT
(ListFn @ROW))
(equal
(RemainderFn ?LESS ?ELEMENT)
0)))))))
Wenn obj1 ist attr1 hinsichlich obj2 und wird ? entgegengesetzet und attr1 ist ein Mitglied von "()" und attr2 ist ein Mitglied von "()" und attr1 ist gleich attr2 nicht, dann obj1 ist attr2 hinsichlich obj2 nicht.
(=>
(and
(orientation ?OBJ1 ?OBJ2 ?ATTR1)
(contraryAttribute @ROW)
(inList
?ATTR1
(ListFn @ROW))
(inList
?ATTR2
(ListFn @ROW))
(not
(equal ?ATTR1 ?ATTR2)))
(not
(orientation ?OBJ1 ?OBJ2 ?ATTR2)))
