TreeView Knowledge Base Browser

appearance as argument number 1

(documentation ListFn ChineseLanguage "这是一个可以接受任何数量的参数，然后交出含有跟哪些参数完全相同顺序的 Function。")	chinese_format.kif 1962-1963
(documentation ListFn EnglishLanguage "A Function that takes any number of arguments and returns the List containing those arguments in exactly the same order.")	Merge.kif 2865-2866
(domain ListFn 1 Entity)	Merge.kif 2861-2861	domain ListFn, 1 and Entity
(instance ListFn Function)	Merge.kif 2859-2859	instance ListFn and Function
(instance ListFn VariableArityRelation)	Merge.kif 2860-2860	instance ListFn and VariableArityRelation
(range ListFn List)	Merge.kif 2863-2863	range ListFn and List

appearance as argument number 2

(format ChineseLanguage ListFn "(%*[,])")	chinese_format.kif 261-261
(format EnglishLanguage ListFn "(%*[,])")	english_format.kif 266-266
(termFormat ChineseLanguage ListFn "名单")	domainEnglishFormat.kif 34668-34668
(termFormat ChineseLanguage ListFn "表列函数")	chinese_format.kif 262-262
(termFormat ChineseTraditionalLanguage ListFn "名單")	domainEnglishFormat.kif 34667-34667
(termFormat EnglishLanguage ListFn "list")	domainEnglishFormat.kif 34666-34666

antecedent

(=> (and (contraryAttribute @ROW1) (identicalListItems (ListFn @ROW1) (ListFn @ROW2))) (contraryAttribute @ROW2))	Merge.kif 468-472	contraryAttribute @ROW1 identicalListItems ListFn @ROW1 and ListFn @ROW2 contraryAttribute @ROW2
(=> (and (defaultMaxValue ?REL ?ARG ?N) (?REL @ARGS) (equal ?VAL (ListOrderFn (ListFn @ARGS) ?ARG))) (modalAttribute (greaterThan ?N ?VAL) Likely))	Merge.kif 18179-18184	defaultMaxValue Predicate, PositiveInteger and Quantity Predicate @ARGS equal Entity and ListOrderFn ListFn @ARGS and PositiveInteger modalAttribute greaterThan Quantity and Entity and Likely
(=> (and (defaultMinValue ?REL ?ARG ?N) (?REL @ARGS) (equal ?VAL (ListOrderFn (ListFn @ARGS) ?ARG))) (modalAttribute (greaterThan ?VAL ?N) Likely))	Merge.kif 18162-18167	defaultMinValue Predicate, PositiveInteger and Quantity Predicate @ARGS equal Entity and ListOrderFn ListFn @ARGS and PositiveInteger modalAttribute greaterThan Entity and Quantity and Likely
(=> (and (defaultValue ?REL ?ARG ?N) (?REL @ARGS) (equal ?VAL (ListOrderFn (ListFn @ARGS) ?ARG))) (modalAttribute (equal ?N ?VAL) Likely))	Merge.kif 18196-18201	defaultValue Predicate, PositiveInteger and Quantity Predicate @ARGS equal Entity and ListOrderFn ListFn @ARGS and PositiveInteger modalAttribute equal Quantity and Entity and Likely
(=> (and (exactCardinality ?REL ?ARG 1) (instance ?REL Predicate) (?REL @ARGS) (equal ?X (ListOrderFn (ListFn @ARGS) ?ARG)) (equal ?Y (ListOrderFn (ListFn @ARGS) ?ARG))) (equal ?X ?Y))	Media.kif 2104-2111	exactCardinality Relation, PositiveInteger and 1 instance Relation and Predicate Relation @ARGS equal Entity and ListOrderFn ListFn @ARGS and PositiveInteger equal Entity and ListOrderFn ListFn @ARGS and PositiveInteger equal Entity and Entity
(=> (and (exactCardinality ?REL ?ARG 1) (instance ?REL Predicate) (?REL @ARGS) (equal ?X (ListOrderFn (ListFn @ARGS) ?ARG))) (not (exists (?Y) (and (equal ?Y (ListOrderFn (ListFn @ARGS) ?ARG)) (not (equal ?X ?Y))))))	Media.kif 2091-2101	exactCardinality Relation, PositiveInteger and 1 instance Relation and Predicate Relation @ARGS equal Entity and ListOrderFn ListFn @ARGS and PositiveInteger Entity equal Entity and ListOrderFn ListFn @ARGS and PositiveInteger equal Entity and Entity
(=> (and (exhaustiveAttribute ?CLASS @ROW) (inList ?ATTR (ListFn @ROW))) (instance ?ATTR ?CLASS))	Merge.kif 503-507	exhaustiveAttribute Attribute and @ROW inList Entity and ListFn @ROW instance Entity and Attribute
(=> (and (exhaustiveAttribute ?CLASS @ROW) (inList ?ATTR (ListFn @ROW))) (instance ?ATTR Attribute))	Merge.kif 497-501	exhaustiveAttribute Attribute and @ROW inList Entity and ListFn @ROW instance Entity and Attribute
(=> (and (instance (LatitudeFn ?DIRECTION @ROW) Region) (equal (ListOrderFn (ListFn @ROW) 1) (MeasureFn ?NUM AngularDegree))) (lessThanOrEqualTo ?NUM 90.0))	Geography.kif 427-431	instance LatitudeFn DirectionalAttribute and @ROW and Region equal ListOrderFn ListFn @ROW and 1 and MeasureFn RealNumber and AngularDegree lessThanOrEqualTo RealNumber and 90.0
(=> (and (instance (LongitudeFn ?DIRECTION @ROW) Region) (equal (ListOrderFn (ListFn @ROW) 1) (MeasureFn ?NUM AngularDegree))) (lessThanOrEqualTo ?NUM 180.0))	Geography.kif 467-474	instance LongitudeFn DirectionalAttribute and @ROW and Region equal ListOrderFn ListFn @ROW and 1 and MeasureFn RealNumber and AngularDegree lessThanOrEqualTo RealNumber and 180.0
(=> (and (instance ?REL IntentionalRelation) (?REL ?AGENT @ROW) (inList ?OBJ (ListFn @ROW))) (inScopeOfInterest ?AGENT ?OBJ))	Merge.kif 2617-2622	instance Entity and IntentionalRelation Entity CognitiveAgent and @ROW inList Entity and ListFn @ROW inScopeOfInterest CognitiveAgent and Entity
(=> (and (orientation ?OBJ1 ?OBJ2 ?ATTR1) (contraryAttribute @ROW) (inList ?ATTR1 (ListFn @ROW)) (inList ?ATTR2 (ListFn @ROW)) (not (equal ?ATTR1 ?ATTR2))) (not (orientation ?OBJ1 ?OBJ2 ?ATTR2)))	Merge.kif 16646-16654	orientation Object, Object and PositionalAttribute contraryAttribute @ROW inList PositionalAttribute and ListFn @ROW inList PositionalAttribute and ListFn @ROW equal PositionalAttribute and PositionalAttribute orientation Object, Object and PositionalAttribute
(=> (and (processList @ROW) (inList ?Process1 (ListFn @ROW)) (inList ?Process2 (ListFn @ROW)) (equal (ListOrderFn (ListFn @ROW) ?Number1) ?Process1) (equal (ListOrderFn (ListFn @ROW) ?Number2) ?Process2) (lessThan ?Number1 ?Number2)) (earlier (WhenFn ?Process1) (WhenFn ?Process2)))	QoSontology.kif 692-708	processList @ROW inList Physical and ListFn @ROW inList Physical and ListFn @ROW equal ListOrderFn ListFn @ROW and PositiveInteger and Physical equal ListOrderFn ListFn @ROW and PositiveInteger and Physical lessThan PositiveInteger and PositiveInteger earlier WhenFn Physical and WhenFn Physical

consequent

(=> (and (domain ?REL ?NUMBER ?CLASS) (instance ?REL Predicate) (?REL @ROW)) (instance (ListOrderFn (ListFn @ROW) ?NUMBER) ?CLASS))	Merge.kif 2926-2931	domain Relation, PositiveInteger and Class instance Relation and Predicate Relation @ROW instance ListOrderFn ListFn @ROW and PositiveInteger and Class
(=> (and (domainSubclass ?REL ?NUMBER ?CLASS) (instance ?REL Predicate) (?REL @ROW)) (subclass (ListOrderFn (ListFn @ROW) ?NUMBER) ?CLASS))	Merge.kif 2933-2938	domainSubclass Relation, PositiveInteger and Class instance Relation and Predicate Relation @ROW subclass ListOrderFn ListFn @ROW and PositiveInteger and Class
(=> (and (equal (GreatestCommonDivisorFn @ROW) ?NUMBER) (not (equal ?NUMBER 0))) (forall (?ELEMENT) (=> (inList ?ELEMENT (ListFn @ROW)) (equal (RemainderFn ?ELEMENT ?NUMBER) 0))))	Merge.kif 4765-4776	equal GreatestCommonDivisorFn @ROW and Integer equal Integer and 0 Integer inList Integer and ListFn @ROW equal RemainderFn Integer and Integer and 0
(=> (and (equal (GreatestCommonDivisorFn @ROW) ?NUMBER) (not (equal ?NUMBER 0))) (not (exists (?GREATER) (and (greaterThan ?GREATER ?NUMBER) (forall (?ELEMENT) (=> (inList ?ELEMENT (ListFn @ROW)) (equal (RemainderFn ?ELEMENT ?GREATER) 0)))))))	Merge.kif 4778-4792	equal GreatestCommonDivisorFn @ROW and Integer equal Integer and 0 Integer greaterThan Integer and Integer Integer inList Integer and ListFn @ROW equal RemainderFn Integer and Integer and 0
(=> (and (equal (LeastCommonMultipleFn @ROW) ?NUMBER) (not (equal ?NUMBER 0))) (forall (?ELEMENT) (=> (inList ?ELEMENT (ListFn @ROW)) (equal (RemainderFn ?NUMBER ?ELEMENT) 0))))	Merge.kif 4850-4860	equal LeastCommonMultipleFn @ROW and Integer equal Integer and 0 Integer inList Integer and ListFn @ROW equal RemainderFn Integer and Integer and 0
(=> (and (equal (LeastCommonMultipleFn @ROW) ?NUMBER) (not (equal ?NUMBER 0))) (not (exists (?LESS) (and (lessThan ?LESS ?NUMBER) (forall (?ELEMENT) (=> (inList ?ELEMENT (ListFn @ROW)) (equal (RemainderFn ?LESS ?ELEMENT) 0)))))))	Merge.kif 4862-4876	equal LeastCommonMultipleFn @ROW and Integer equal Integer and 0 Integer lessThan Integer and Integer Integer inList Integer and ListFn @ROW equal RemainderFn Integer and Integer and 0
(=> (and (equal ?R (SubListFn ?S ?E ?L)) (equal (SubtractionFn ?E ?S) 1)) (equal ?R (ListFn (ListOrderFn ?L ?S))))	Merge.kif 3107-3116	equal List and SubListFn PositiveInteger, Integer and List equal SubtractionFn Integer and PositiveInteger and 1 equal List and ListFn ListOrderFn List and PositiveInteger
(=> (and (equal ?R (SubListFn ?S ?E ?L)) (greaterThan (SubtractionFn ?E ?S) 1)) (equal ?R (ListConcatenateFn (ListFn (ListOrderFn ?L ?S)) (SubListFn (AdditionFn 1 ?S) ?E ?L))))	Merge.kif 3118-3130	equal List and SubListFn PositiveInteger, Integer and List greaterThan SubtractionFn Integer and PositiveInteger and 1 equal List and ListConcatenateFn ListFn ListOrderFn List and PositiveInteger and SubListFn AdditionFn 1 and PositiveInteger, Integer and List
(=> (and (exactCardinality ?REL ?ARG 1) (instance ?REL Predicate) (?REL @ARGS) (equal ?X (ListOrderFn (ListFn @ARGS) ?ARG))) (not (exists (?Y) (and (equal ?Y (ListOrderFn (ListFn @ARGS) ?ARG)) (not (equal ?X ?Y))))))	Media.kif 2091-2101	exactCardinality Relation, PositiveInteger and 1 instance Relation and Predicate Relation @ARGS equal Entity and ListOrderFn ListFn @ARGS and PositiveInteger Entity equal Entity and ListOrderFn ListFn @ARGS and PositiveInteger equal Entity and Entity
(=> (and (exactCardinality ?REL ?ARG 1) (instance ?REL Predicate)) (exists (?X @ARGS) (and (?REL @ARGS) (equal ?X (ListOrderFn (ListFn @ARGS) ?ARG)) (not (exists (?Y) (and (equal ?Y (ListOrderFn (ListFn @ARGS) ?ARG)) (not (equal ?X ?Y))))))))	Media.kif 2073-2088	exactCardinality Relation, PositiveInteger and 1 instance Relation and Predicate Entity @ARGS Relation @ARGS equal Entity and ListOrderFn ListFn @ARGS and PositiveInteger Entity equal Entity and ListOrderFn ListFn @ARGS and PositiveInteger equal Entity and Entity
(=> (and (exactCardinality ?REL ?ARG ?COUNT) (instance ?REL Predicate)) (exists (?S) (and (instance ?S SetOrClass) (=> (and (?REL @ARGS) (equal ?EL (ListOrderFn (ListFn @ARGS) ?ARG))) (and (instance ?EL ?S) (equal (CardinalityFn ?S) ?COUNT))))))	Media.kif 2130-2143	exactCardinality Relation, PositiveInteger and Integer instance Relation and Predicate Class instance Class and SetOrClass Relation @ARGS equal Entity and ListOrderFn ListFn @ARGS and PositiveInteger instance Entity and Class equal CardinalityFn Class and Integer
(=> (and (maxCardinality ?REL ?ARG ?COUNT) (instance ?REL Predicate)) (exists (?S) (and (instance ?S SetOrClass) (=> (and (?REL @ARGS) (equal ?EL (ListOrderFn (ListFn @ARGS) ?ARG))) (and (instance ?EL ?S) (lessThanOrEqualTo (CardinalityFn ?S) ?COUNT))))))	Media.kif 2201-2214	maxCardinality Relation, PositiveInteger and Integer instance Relation and Predicate Class instance Class and SetOrClass Relation @ARGS equal Entity and ListOrderFn ListFn @ARGS and PositiveInteger instance Entity and Class lessThanOrEqualTo CardinalityFn Class and Integer
(=> (and (minCardinality ?REL ?ARG ?COUNT) (instance ?REL Predicate)) (exists (?S) (and (instance ?S SetOrClass) (=> (and (?REL @ARGS) (equal ?EL (ListOrderFn (ListFn @ARGS) ?ARG))) (and (instance ?EL ?S) (greaterThanOrEqualTo (CardinalityFn ?S) ?COUNT))))))	Media.kif 2166-2179	minCardinality Relation, PositiveInteger and Integer instance Relation and Predicate Class instance Class and SetOrClass Relation @ARGS equal Entity and ListOrderFn ListFn @ARGS and PositiveInteger instance Entity and Class greaterThanOrEqualTo CardinalityFn Class and Integer
(=> (and (valence ?REL ?NUMBER) (instance ?REL Predicate)) (forall (@ROW) (=> (?REL @ROW) (equal (ListLengthFn (ListFn @ROW)) ?NUMBER))))	Merge.kif 2976-2983	valence Relation and PositiveInteger instance Relation and Predicate @ROW Relation @ROW equal ListLengthFn ListFn @ROW and PositiveInteger
(=> (contraryAttribute @ROW) (=> (inList ?ELEMENT (ListFn @ROW)) (instance ?ELEMENT Attribute)))	Merge.kif 462-466	contraryAttribute @ROW inList Entity and ListFn @ROW instance Entity and 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))))))	Merge.kif 474-484	contraryAttribute @ROW Attribute Attribute equal Attribute and ListOrderFn ListFn @ROW and PositiveInteger equal Attribute and ListOrderFn ListFn @ROW and PositiveInteger equal PositiveInteger and PositiveInteger property Entity and Attribute property Entity and Attribute
(=> (disjointDecomposition ?CLASS @ROW) (forall (?ITEM) (=> (inList ?ITEM (ListFn @ROW)) (subclass ?ITEM ?CLASS))))	Merge.kif 2878-2883	disjointDecomposition Class and @ROW Class inList Class and ListFn @ROW subclass Class and Class
(=> (disjointDecomposition ?CLASS @ROW) (forall (?ITEM1 ?ITEM2) (=> (and (inList ?ITEM1 (ListFn @ROW)) (inList ?ITEM2 (ListFn @ROW)) (not (equal ?ITEM1 ?ITEM2))) (disjoint ?ITEM1 ?ITEM2))))	Merge.kif 2885-2894	disjointDecomposition Class and @ROW Class Class inList Class and ListFn @ROW inList Class and ListFn @ROW equal Class and Class disjoint Class and Class
(=> (disjointDecomposition @ROW) (=> (inList ?ELEMENT (ListFn @ROW)) (instance ?ELEMENT Class)))	Merge.kif 574-578	disjointDecomposition @ROW inList Entity and ListFn @ROW instance Entity and Class
(=> (equal (GreatestCommonDivisorFn @ROW) ?NUMBER) (=> (inList ?ELEMENT (ListFn @ROW)) (instance ?ELEMENT Number)))	Merge.kif 4758-4763	equal GreatestCommonDivisorFn @ROW and Integer inList Entity and ListFn @ROW instance Entity and Number
(=> (equal (LeastCommonMultipleFn @ROW) ?NUMBER) (=> (inList ?ELEMENT (ListFn @ROW)) (instance ?ELEMENT Number)))	Merge.kif 4843-4848	equal LeastCommonMultipleFn @ROW and Integer inList Entity and ListFn @ROW instance Entity and Number
(=> (equal ?LIST1 ?LIST2) (=> (and (equal ?LIST1 (ListFn @ROW1)) (equal ?LIST2 (ListFn @ROW2))) (forall (?NUMBER) (equal (ListOrderFn (ListFn @ROW1) ?NUMBER) (ListOrderFn (ListFn @ROW2) ?NUMBER)))))	Merge.kif 293-300	equal List and List equal List and ListFn @ROW1 equal List and ListFn @ROW2 PositiveInteger equal ListOrderFn ListFn @ROW1 and PositiveInteger and ListOrderFn ListFn @ROW2 and PositiveInteger
(=> (exactCardinality ?REL ?ARG ?COUNT) (equal (CardinalityFn (KappaFn ?EL (and (?REL @ARGS) (equal ?EL (ListOrderFn (ListFn @ARGS) ?ARG))))) ?COUNT))	Media.kif 2119-2127	exactCardinality Relation, Integer and Integer equal CardinalityFn KappaFn SymbolicString and Relation @ARGS equal SymbolicString and ListOrderFn ListFn @ARGS and Integer and Integer
(=> (exhaustiveAttribute ?ATTRCLASS @ROW) (not (exists (?EL) (and (instance ?EL ?ATTRCLASS) (not (exists (?ATTR ?NUMBER) (and (equal ?EL ?ATTR) (equal ?ATTR (ListOrderFn (ListFn @ROW) ?NUMBER)))))))))	Merge.kif 519-531	exhaustiveAttribute Attribute and @ROW Entity instance Entity and Attribute Entity PositiveInteger equal Entity and Entity equal Entity and ListOrderFn ListFn @ROW and PositiveInteger
(=> (exhaustiveAttribute ?CLASS @ROW) (forall (?ATTR1) (=> (instance ?ATTR1 ?CLASS) (exists (?ATTR2) (and (inList ?ATTR2 (ListFn @ROW)) (equal ?ATTR1 ?ATTR2))))))	Merge.kif 509-517	exhaustiveAttribute Attribute and @ROW Entity instance Entity and Attribute Entity inList Entity and ListFn @ROW equal Entity and Entity

Display limited to 25 items. Show next 25

Display limited to 25 items. Show next 25

statement

(forall (@ROW ?ITEM) (equal (ListLengthFn (ListFn @ROW ?ITEM)) (SuccessorFn (ListLengthFn (ListFn @ROW)))))	Merge.kif 2965-2968	@ROW Entity equal ListLengthFn ListFn @ROW and entity and SuccessorFn ListLengthFn ListFn @ROW
(forall (@ROW ?ITEM) (equal (ListOrderFn (ListFn @ROW ?ITEM) (ListLengthFn (ListFn @ROW ?ITEM))) ?ITEM))	Merge.kif 2970-2974	@ROW Entity equal ListOrderFn ListFn @ROW and Entity and ListLengthFn ListFn @ROW and Entity and Entity
(forall (@ROW ?ITEM) (initialList (ListFn @ROW) (ListFn @ROW ?ITEM)))	Merge.kif 3244-3245	@ROW Entity initialList ListFn @ROW and ListFn @ROW and entity

Show simplified definition (without tree view)
Show simplified definition (with tree view)

KB Term:			Term intersection

English Word: