xu4 lie4 han2 shu4 (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)
zhi3 ding4 han2 shu4
zui4 da4 gong1 yue1 shu4 han2 shu4
zui4 xiao3 gong1 bei4 shu4 han2 shu4
mao2 dun4 shu3 xing4
wu2 jiao1 ji2 fen1 jie3
wu2 jiao1 ji2 guan1 xi4
qiong2 jin4 de5 shu3 xing4
qiong2 jin4 de5 fen1 jie3
cheng2 li4
fen1 ge1
Axioms (27)
- if obj1 deng3 yu1 obj2,
- then if obj1 deng3 yu1 ""()" de5 di4 er4 yuan2 su4" and obj2 deng3 yu1 ""()" de5 di4 er4 yuan2 su4" and "()" deng3 yu1 "()", then () (bu2) cheng2 li4s if and only if () (bu2) cheng2 li4s
.
(=>
(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 deng3 yu1 list2,
- then if list1 deng3 yu1 "()" and list2 deng3 yu1 "()", then for all number holds: ""()" de5 di4 er4 yuan2 su4" deng3 yu1 ""()" de5 di4 er4 yuan2 su4"
.
(=>
(equal ?LIST1 ?LIST2)
(=>
(and
(equal
?LIST1
(ListFn @ROW1))
(equal
?LIST2
(ListFn @ROW2)))
(forall
(?NUMBER)
(equal
(ListOrderFn
(ListFn @ROW1)
?NUMBER)
(ListOrderFn
(ListFn @ROW2)
?NUMBER)))))
If wu2 jiao1 ji2 guan1 xi4() holds and rel shi4 "()" de5 yi1 cheng2 yuan2, then rel shi4 guan1 xi4 de5 shi2 li4.
(=>
(and
(disjointRelation @ROW)
(inList
?REL
(ListFn @ROW)))
(instance ?REL Relation))
If wu2 jiao1 ji2 guan1 xi4() holds and rel1 shi4 "()" de5 yi1 cheng2 yuan2 and rel2 shi4 "()" de5 yi1 cheng2 yuan2 and rel1 %&有 論元(s) number, then rel2 %&有 論元(s) number.
(=>
(and
(disjointRelation @ROW)
(inList
?REL1
(ListFn @ROW))
(inList
?REL2
(ListFn @ROW))
(valence ?REL1 ?NUMBER))
(valence ?REL2 ?NUMBER))
If wu2 jiao1 ji2 guan1 xi4() holds and rel1 shi4 "()" de5 yi1 cheng2 yuan2 and rel2 shi4 "()" de5 yi1 cheng2 yuan2 and rel1 deng3 yu1 rel2 and rel1() (bu2) cheng2 li4s, then rel2() not(bu2) cheng2 li4.
(=>
(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)))
- if dui4 li4 yu1 ?,
- then for all attr1,attr2 holds:
- if attr1 deng3 yu1 ""()" de5 di4 er4 yuan2 su4" and attr2 deng3 yu1 ""()" de5 di4 er4 yuan2 su4" and number1 deng3 yu1 number2,
- then if obj you3 shu3 xing4 attr1, then obj you3 shu3 xing4 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 qiong2 jin4 de5 shu3 xing4,
- then if attr shi4 "()" de5 yi1 cheng2 yuan2, then attr shi4 shu3 xing4 de5 shi2 li4
.
(=>
(exhaustiveAttribute ?CLASS @ROW)
(=>
(inList
?ATTR
(ListFn @ROW))
(instance ?ATTR Attribute)))
- if qiong2 jin4 de5 shu3 xing4,
- then for all obj holds: if attr1 shi4 class de5 shi2 li4, then there exists attr2 so_that_not attr2 shi4 "()" de5 yi1 cheng2 yuan2 and attr1 deng3 yu1 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)))
- if wu2 jiao1 ji2 di4 fen1 jie3 cheng2 ,
- then if element shi4 "()" de5 yi1 cheng2 yuan2, then element shi4 zhong3 lei4 de5 shi2 li4
.
(=>
(disjointDecomposition @ROW)
(=>
(inList
?ELEMENT
(ListFn @ROW))
(instance ?ELEMENT Class)))
rel shi4 quan2 zhi2 guan1 xi4 de5 shi2 li4 if and only if there exists valence so_that_not rel shi4 guan1 xi4 de5 shi2 li4 and rel %&有 論元(s) valence and - if for all number,element,class holds: if number xiao3 yu1 valence and rel de5 lun4 yuan2 number shi4 class de5 shi2 li4 and element deng3 yu1 ""()" de5 di4 er4 yuan2 su4", then element shi4 class de5 shi2 li4,
- then there exists item so_that_not rel(,item) (bu2) cheng2 li4s
.
(<=>
(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 shi4 yi4 tu2 guan1 xi4 de5 shi2 li4 and rel(agent,) (bu2) cheng2 li4s and obj shi4 "()" de5 yi1 cheng2 yuan2, then agent zai4 obj fan4 wei2 zhong1.
(=>
(and
(instance ?REL IntentionalRelation)
(holds ?REL ?AGENT @ROW)
(inList
?OBJ
(ListFn @ROW)))
(inScopeOfInterest ?AGENT ?OBJ))
- if class bei4 bao1 han2,
- then for all obj holds: if obj shi4 class de5 shi2 li4, then there exists item so_that_not item shi4 "()" de5 yi1 cheng2 yuan2 and obj shi4 item de5 shi2 li4
.
(=>
(exhaustiveDecomposition ?CLASS @ROW)
(forall
(?OBJ)
(=>
(instance ?OBJ ?CLASS)
(exists
(?ITEM)
(and
(inList
?ITEM
(ListFn @ROW))
(instance ?OBJ ?ITEM))))))
- if class wu2 jiao1 ji2 di4 fen1 jie3 cheng2 ,
- then for all item holds: if item shi4 "()" de5 yi1 cheng2 yuan2, then item shi4 class de5 ci4 zhong3 lei4
.
(=>
(disjointDecomposition ?CLASS @ROW)
(forall
(?ITEM)
(=>
(inList
?ITEM
(ListFn @ROW))
(subclass ?ITEM ?CLASS))))
- if class wu2 jiao1 ji2 di4 fen1 jie3 cheng2 ,
- then for all item1,item2 holds: if item1 shi4 "()" de5 yi1 cheng2 yuan2 and item2 shi4 "()" de5 yi1 cheng2 yuan2 and item1 deng3 yu1 item2, then item1 wu2 jiao1 ji2 yu1 item2
.
(=>
(disjointDecomposition ?CLASS @ROW)
(forall
(?ITEM1 ?ITEM2)
(=>
(and
(inList
?ITEM1
(ListFn @ROW))
(inList
?ITEM2
(ListFn @ROW))
(not
(equal ?ITEM1 ?ITEM2)))
(disjoint ?ITEM1 ?ITEM2))))
If rel de5 lun4 yuan2 number shi4 class de5 shi2 li4 and rel() (bu2) cheng2 li4s, then ""()" de5 di4 er4 yuan2 su4" shi4 class de5 shi2 li4.
(=>
(and
(domain ?REL ?NUMBER ?CLASS)
(holds ?REL @ROW))
(instance
(ListOrderFn
(ListFn @ROW)
?NUMBER)
?CLASS))
If rel de5 lun4 yuan2 number shi4 class de5 ci4 zhong3 lei4 and rel() (bu2) cheng2 li4s, then ""()" de5 di4 er4 yuan2 su4" shi4 class de5 ci4 zhong3 lei4.
(=>
(and
(domainSubclass ?REL ?NUMBER ?CLASS)
(holds ?REL @ROW))
(subclass
(ListOrderFn
(ListFn @ROW)
?NUMBER)
?CLASS))
""(,item)" de5 chang2 du4" deng3 yu1 "(""()" de5 chang2 du4"+1)".
(equal
(ListLengthFn
(ListFn @ROW ?ITEM))
(SuccessorFn
(ListLengthFn
(ListFn @ROW))))
""(,item)" de5 di4 er4 yuan2 su4" deng3 yu1 item.
(equal
(ListOrderFn
(ListFn @ROW ?ITEM)
(ListLengthFn
(ListFn @ROW ?ITEM)))
?ITEM)
- if rel %&有 論元(s) number,
- then for all holds: if rel() (bu2) cheng2 li4s, then ""()" de5 chang2 du4" deng3 yu1 number
.
(=>
(valence ?REL ?NUMBER)
(forall
(@ROW)
(=>
(holds ?REL @ROW)
(equal
(ListLengthFn
(ListFn @ROW))
?NUMBER))))
"()" (mei2chu1 shi3 hua4not(s) "(,item)".
(initialList
(ListFn @ROW)
(ListFn @ROW ?ITEM))
- if " de5 zui4 da4 gong1 yue1 shu4" deng3 yu1 number,
- then for all element holds: if element shi4 "()" de5 yi1 cheng2 yuan2, then "element qu3 yu2 shu4 number" deng3 yu1
.
(=>
(equal
(GreatestCommonDivisorFn @ROW)
?NUMBER)
(forall
(?ELEMENT)
(=>
(inList
?ELEMENT
(ListFn @ROW))
(equal
(RemainderFn ?ELEMENT ?NUMBER)
0))))
- if " de5 zui4 da4 gong1 yue1 shu4" deng3 yu1 number,
- then there doesn't exist greater so_that_not greater (bu2) da4 yu1 number and for all element holds: if element shi4 "()" de5 yi1 cheng2 yuan2, then "element qu3 yu2 shu4 greater" deng3 yu1
.
(=>
(equal
(GreatestCommonDivisorFn @ROW)
?NUMBER)
(not
(exists
(?GREATER)
(and
(greaterThan ?GREATER ?NUMBER)
(forall
(?ELEMENT)
(=>
(inList
?ELEMENT
(ListFn @ROW))
(equal
(RemainderFn ?ELEMENT ?GREATER)
0)))))))
- if " de5 zui4 xiao3 gong1 bei4 shu4" deng3 yu1 number,
- then for all element holds: if element shi4 "()" de5 yi1 cheng2 yuan2, then "number qu3 yu2 shu4 element" deng3 yu1
.
(=>
(equal
(LeastCommonMultipleFn @ROW)
?NUMBER)
(forall
(?ELEMENT)
(=>
(inList
?ELEMENT
(ListFn @ROW))
(equal
(RemainderFn ?NUMBER ?ELEMENT)
0))))
- if " de5 zui4 xiao3 gong1 bei4 shu4" deng3 yu1 number,
- then there doesn't exist less so_that_not less xiao3 yu1 number and for all element holds: if element shi4 "()" de5 yi1 cheng2 yuan2, then "less qu3 yu2 shu4 element" deng3 yu1
.
(=>
(equal
(LeastCommonMultipleFn @ROW)
?NUMBER)
(not
(exists
(?LESS)
(and
(lessThan ?LESS ?NUMBER)
(forall
(?ELEMENT)
(=>
(inList
?ELEMENT
(ListFn @ROW))
(equal
(RemainderFn ?LESS ?ELEMENT)
0)))))))
If obj1 dui4 obj2 shi4 attr1 and dui4 li4 yu1 ? and attr1 shi4 "()" de5 yi1 cheng2 yuan2 and attr2 shi4 "()" de5 yi1 cheng2 yuan2 and attr1 deng3 yu1 attr2, then obj1 dui4 obj2 shi4 not attr2.
(=>
(and
(orientation ?OBJ1 ?OBJ2 ?ATTR1)
(contraryAttribute @ROW)
(inList
?ATTR1
(ListFn @ROW))
(inList
?ATTR2
(ListFn @ROW))
(not
(equal ?ATTR1 ?ATTR2)))
(not
(orientation ?OBJ1 ?OBJ2 ?ATTR2)))
