Browsing Interface : Welcome guest : log in 		[  Home |  Graph |  LogLearn |  Editor |  ]  KB:  Language: 
  Formal Language: 


KB Term:  Term intersection
English Word: 

Sigma KEE - ListFn
ListFn

appearance as argument number 1
-------------------------


(instance ListFn Function) Merge.kif 3042-3042 List is an instance of function
(instance ListFn VariableArityRelation) Merge.kif 3043-3043 List is an instance of variable arity relation
(domain ListFn 1 Entity) Merge.kif 3044-3044 The number 1 argument of list is an instance of entity
(range ListFn List) Merge.kif 3046-3046 The range of list is an instance of list
(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 3048-3049 The range of list is an instance of list

appearance as argument number 2
-------------------------


(termFormat EnglishLanguage ListFn "list") domainEnglishFormat.kif 34687-34687
(termFormat ChineseTraditionalLanguage ListFn "名單") domainEnglishFormat.kif 34688-34688
(termFormat ChineseLanguage ListFn "名单") domainEnglishFormat.kif 34689-34689
(format EnglishLanguage ListFn "(%*[,])") english_format.kif 266-266

antecedent
-------------------------


(=>
    (and
        (equal ?LIST1 ?LIST2)
        (equal ?LIST1
            (ListFn @ROW1))
        (equal ?LIST2
            (ListFn @ROW2)))
    (equal
        (ListOrderFn
            (ListFn @ROW1) ?NUMBER)
        (ListOrderFn
            (ListFn @ROW2) ?NUMBER)))		 Merge.kif 289-296 If equal X and Y, equal X and (@ROW1), and equal Y and (@ROW2), then equal V element of (@ROW1) and V element of (@ROW2)
(=>
    (and
        (contraryAttribute @ROW1)
        (identicalListItems
            (ListFn @ROW1)
            (ListFn @ROW2)))
    (contraryAttribute @ROW2))		 Merge.kif 462-466 If @ROW1 is the opposite of and (@ROW2) is an identical list items of (@ROW1), then @ROW2 is the opposite of
(=>
    (and
        (contraryAttribute @ROW)
        (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 468-476 If @ROW is the opposite of, equal Y and Z element of (@ROW), equal W and V element of (@ROW), equal U and T, and S the attribute Y, then S does not have the attribute W
(=>
    (and
        (exhaustiveAttribute ?CLASS @ROW)
        (inList ?ATTR
            (ListFn @ROW)))
    (instance ?ATTR Attribute))		 Merge.kif 489-493 If @ROW are all the attributes of Y and Z is a member of (@ROW), then Z is an instance of attribute
(=>
    (and
        (exhaustiveAttribute ?CLASS @ROW)
        (inList ?ATTR
            (ListFn @ROW)))
    (instance ?ATTR ?CLASS))		 Merge.kif 495-499 If @ROW are all the attributes of Y and Z is a member of (@ROW), then Z is an instance of Y
(=>
    (and
        (instance ?REL IntentionalRelation)
        (?REL ?AGENT @ROW)
        (inList ?OBJ
            (ListFn @ROW)))
    (inScopeOfInterest ?AGENT ?OBJ))		 Merge.kif 2786-2791 If X is an instance of intentional relation, X Y and @ROW, and W is a member of (@ROW), then Y is interested in W
(=>
    (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 17275-17283 If X is Y to Z, @ROW is the opposite of, Y is a member of (@ROW), V is a member of (@ROW), and equal Y and V, then X is not V to Z
(=>
    (and
        (defaultMinValue ?REL ?ARG ?N)
        (?REL @ARGS)
        (equal ?VAL
            (ListOrderFn
                (ListFn @ARGS) ?ARG)))
    (modalAttribute
        (greaterThan ?VAL ?N) Likely))		 Merge.kif 18777-18782 If The defaultMinValue of X with Y arguments is Z., X @ARGS, and equal V and U element of (@ARGS), then the statement V is greater than Z has the modal force of likely
(=>
    (and
        (defaultMaxValue ?REL ?ARG ?N)
        (?REL @ARGS)
        (equal ?VAL
            (ListOrderFn
                (ListFn @ARGS) ?ARG)))
    (modalAttribute
        (greaterThan ?N ?VAL) Likely))		 Merge.kif 18794-18799 If The defalutMaxValue of X with Y arguments is Z., X @ARGS, and equal V and U element of (@ARGS), then the statement Z is greater than V has the modal force of likely
(=>
    (and
        (defaultValue ?REL ?ARG ?N)
        (?REL @ARGS)
        (equal ?VAL
            (ListOrderFn
                (ListFn @ARGS) ?ARG)))
    (modalAttribute
        (equal ?N ?VAL) Likely))		 Merge.kif 18811-18816 If The defaultValue of X with Y arguments is Z., X @ARGS, and equal V and U element of (@ARGS), then the statement equal Z and V has the modal force of likely
(=>
    (and
        (instance
            (LatitudeFn ?DIRECTION @ROW) Region)
        (equal
            (ListOrderFn
                (ListFn @ROW) 1)
            (MeasureFn ?NUM AngularDegree)))
    (lessThanOrEqualTo ?NUM 90.0))		 Geography.kif 1905-1909 If the region X of @ROW is an instance of region and equal 1th element of (@ROW) and Z angular degree(s), then Z is less than or equal to 90.0
(=>
    (and
        (instance
            (LongitudeFn ?DIRECTION @ROW) Region)
        (equal
            (ListOrderFn
                (ListFn @ROW) 1)
            (MeasureFn ?NUM AngularDegree)))
    (lessThanOrEqualTo ?NUM 180.0))		 Geography.kif 1943-1950 If the meridian at @ROW Y is an instance of region and equal 1th element of (@ROW) and Z angular degree(s), then Z is less than or equal to 180.0
(=>
    (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 2040-2050 If there can be 1 values to argument X of Y, Y is an instance of predicate, Y @ARGS, and equal W and V element of (@ARGS), then there doesn't exist U such that equal U and V element of (@ARGS) and equal W and U
(=>
    (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 2053-2060 If there can be 1 values to argument X of Y, Y is an instance of predicate, Y @ARGS, equal W and V element of (@ARGS), and equal U and V element of (@ARGS), then equal W and U
(=>
    (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 790-806 If All of the following hold: (1) the list of processes @ROW (2) Y is a member of (@ROW) (3) Z is a member of (@ROW) (4) equal W element of (@ROW) and Y (5) equal V element of (@ROW) and Z (6) U is less than T, then the time of existence of Y happens earlier than the time of existence of Z

consequent
-------------------------


(=>
    (and
        (equal ?LIST1 ?LIST2)
        (equal ?LIST1
            (ListFn @ROW1))
        (equal ?LIST2
            (ListFn @ROW2)))
    (equal
        (ListOrderFn
            (ListFn @ROW1) ?NUMBER)
        (ListOrderFn
            (ListFn @ROW2) ?NUMBER)))		 Merge.kif 289-296 If equal X and Y, equal X and (@ROW1), and equal Y and (@ROW2), then equal V element of (@ROW1) and V element of (@ROW2)
(=>
    (contraryAttribute @ROW)
    (=>
        (inList ?ELEMENT
            (ListFn @ROW))
        (instance ?ELEMENT Attribute)))		 Merge.kif 456-460 Assuming @ROW is the opposite of, it follows that: if Y is a member of (@ROW), then Y is an instance of attribute
(=>
    (exhaustiveAttribute ?CLASS @ROW)
    (forall (?ATTR1)
        (=>
            (instance ?ATTR1 ?CLASS)
            (exists (?ATTR2)
                (and
                    (inList ?ATTR2
                        (ListFn @ROW))
                    (equal ?ATTR1 ?ATTR2))))))		 Merge.kif 501-509 If @ROW are all the attributes of Y, then For all Entity Z: if Z is an instance of Y, then there exists W such that W is a member of (@ROW) and equal Z and W
(=>
    (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 511-523 If @ROW are all the attributes of Y, then there doesn't exist Z such that Z is an instance of Y and there don't exist W and V such that equal Z and W and equal W and U element of (@ROW)
(=>
    (exhaustiveDecomposition @ROW)
    (=>
        (inList ?ELEMENT
            (ListFn @ROW))
        (instance ?ELEMENT Class)))		 Merge.kif 550-554 Assuming @ROW is covered by @ROW, it follows that: if Y is a member of (@ROW), then Y is an instance of class
(=>
    (disjointDecomposition @ROW)
    (=>
        (inList ?ELEMENT
            (ListFn @ROW))
        (instance ?ELEMENT Class)))		 Merge.kif 566-570 Assuming @ROW is disjointly decomposed into @ROW, it follows that: if Y is a member of (@ROW), then Y is an instance of class
(=>
    (exhaustiveDecomposition ?CLASS @ROW)
    (forall (?OBJ)
        (=>
            (instance ?OBJ ?CLASS)
            (exists (?ITEM)
                (and
                    (inList ?ITEM
                        (ListFn @ROW))
                    (instance ?OBJ ?ITEM))))))		 Merge.kif 3051-3059 If X is covered by @ROW, then For all Entity Z: if Z is an instance of X, then there exists W such that W is a member of (@ROW) and Z is an instance of W
(=>
    (disjointDecomposition ?CLASS @ROW)
    (forall (?ITEM)
        (=>
            (inList ?ITEM
                (ListFn @ROW))
            (subclass ?ITEM ?CLASS))))		 Merge.kif 3061-3066 If X is disjointly decomposed into @ROW, then For all Class Z: if Z is a member of (@ROW), then Z is a subclass of X
(=>
    (disjointDecomposition ?CLASS @ROW)
    (forall (?ITEM1 ?ITEM2)
        (=>
            (and
                (inList ?ITEM1
                    (ListFn @ROW))
                (inList ?ITEM2
                    (ListFn @ROW))
                (not
                    (equal ?ITEM1 ?ITEM2)))
            (disjoint ?ITEM1 ?ITEM2))))		 Merge.kif 3068-3077 If X is disjointly decomposed into @ROW, then For all Classes Z and W: if Z is a member of (@ROW), W is a member of (@ROW), and equal Z and W, then Z is disjoint from W
(=>
    (and
        (domain ?REL ?NUMBER ?CLASS)
        (instance ?REL Predicate)
        (?REL @ROW))
    (instance
        (ListOrderFn
            (ListFn @ROW) ?NUMBER) ?CLASS))		 Merge.kif 3109-3114 If the number X argument of Y is an instance of Z, Y is an instance of predicate, and Y @ROW, then V element of (@ROW) is an instance of Z
(=>
    (and
        (domainSubclass ?REL ?NUMBER ?CLASS)
        (instance ?REL Predicate)
        (?REL @ROW))
    (subclass
        (ListOrderFn
            (ListFn @ROW) ?NUMBER) ?CLASS))		 Merge.kif 3116-3121 If the number X argument of Y is a subclass of Z, Y is an instance of predicate, and Y @ROW, then V element of (@ROW) is a subclass of Z
(=>
    (and
        (valence ?REL ?NUMBER)
        (instance ?REL Predicate))
    (forall (@ROW)
        (=>
            (?REL @ROW)
            (equal
                (ListLengthFn
                    (ListFn @ROW)) ?NUMBER))))		 Merge.kif 3159-3166 If X has Y argument(s) and X is an instance of predicate, then for all : if X @ROW, then equal length of (@ROW) and Y
(=>
    (and
        (equal ?R
            (SubListFn ?S ?E ?L))
        (equal
            (SubtractionFn ?E ?S) 1))
    (equal ?R
        (ListFn
            (ListOrderFn ?L ?S))))		 Merge.kif 3290-3299 If equal X and the sub-list from Y to Z of W and equal (Z and Y) and 1, then equal X and (V element of W)
(=>
    (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 3301-3313 If equal X and the sub-list from Y to Z of W and (Z and Y) is greater than 1, then equal X and the list composed of (V element of W) and the sub-list from (1 and Y) to Z of W
(=>
    (equal
        (GreatestCommonDivisorFn @ROW) ?NUMBER)
    (=>
        (inList ?ELEMENT
            (ListFn @ROW))
        (instance ?ELEMENT Number)))		 Merge.kif 4966-4971 Assuming equal the greatest common divisor of @ROW and Y, it follows that: if Z is a member of (@ROW), then Z is an instance of number
(=>
    (and
        (equal
            (GreatestCommonDivisorFn @ROW) ?NUMBER)
        (not
            (equal ?NUMBER 0)))
    (forall (?ELEMENT)
        (=>
            (inList ?ELEMENT
                (ListFn @ROW))
            (equal
                (RemainderFn ?ELEMENT ?NUMBER) 0))))		 Merge.kif 4973-4984 If equal the greatest common divisor of @ROW and Y and equal Y and 0, then For all Integer Z: if Z is a member of (@ROW), then equal Z mod Y 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 4986-5000 If equal the greatest common divisor of @ROW and Y and equal Y and 0, then there doesn't exist Z such that Z is greater than Y and W W is a member of (@ROW)equal W mod Z and 0
(=>
    (equal
        (LeastCommonMultipleFn @ROW) ?NUMBER)
    (=>
        (inList ?ELEMENT
            (ListFn @ROW))
        (instance ?ELEMENT Number)))		 Merge.kif 5051-5056 Assuming equal the least common multiple of @ROW and Y, it follows that: if Z is a member of (@ROW), then Z is an instance of number
(=>
    (and
        (equal
            (LeastCommonMultipleFn @ROW) ?NUMBER)
        (not
            (equal ?NUMBER 0)))
    (forall (?ELEMENT)
        (=>
            (inList ?ELEMENT
                (ListFn @ROW))
            (equal
                (RemainderFn ?NUMBER ?ELEMENT) 0))))		 Merge.kif 5058-5068 If equal the least common multiple of @ROW and Y and equal Y and 0, then For all Integer Z: if Z is a member of (@ROW), then equal Y mod Z 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 5070-5084 If equal the least common multiple of @ROW and Y and equal Y and 0, then there doesn't exist Z such that Z is less than Y and W W is a member of (@ROW)equal Z mod W and 0
(=>
    (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 2022-2037 If there can be 1 values to argument X of Y and Y is an instance of predicate, then there exist Z and @ARGS such that Y @ARGS and equal Z and V element of (@ARGS) and there doesn't exist U such that equal U and V element of (@ARGS) and equal Z and U
(=>
    (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 2040-2050 If there can be 1 values to argument X of Y, Y is an instance of predicate, Y @ARGS, and equal W and V element of (@ARGS), then there doesn't exist U such that equal U and V element of (@ARGS) and equal W and U
(=>
    (exactCardinality ?REL ?ARG ?COUNT)
    (exists (?EL @ARGS)
        (equal
            (CardinalityFn
                (KappaFn ?EL
                    (and
                        (?REL @ARGS)
                        (equal ?EL
                            (ListOrderFn
                                (ListFn @ARGS) ?ARG))))) ?COUNT)))		 Media.kif 2072-2081 If there can be X values to argument Y of Z, then there exist W, @ARGS such that equal the number of instances in the class described by W, and X
(=>
    (and
        (exactCardinality ?REL ?ARG ?COUNT)
        (instance ?REL Predicate))
    (exists (?S ?EL @ARGS)
        (and
            (instance ?S SetOrClass)
            (=>
                (and
                    (?REL @ARGS)
                    (equal ?EL
                        (ListOrderFn
                            (ListFn @ARGS) ?ARG)))
                (and
                    (instance ?EL ?S)
                    (equal
                        (CardinalityFn ?S) ?COUNT))))))		 Media.kif 2084-2097 If there can be X values to argument Y of Z and Z is an instance of predicate, then there exist W, V and @ARGS such that W is an instance of set or class and Z @ARGS and equal V and T element of (@ARGS)V is an instance of W and equal the number of instances in W and X
(=>
    (minCardinality ?REL ?ARG ?COUNT)
    (exists (?EL @ARGS)
        (greaterThanOrEqualTo
            (CardinalityFn
                (KappaFn ?EL
                    (and
                        (?REL @ARGS)
                        (equal ?EL
                            (ListOrderFn
                                (ListFn @ARGS) ?ARG))))) ?COUNT)))		 Media.kif 2108-2117 If there are at least X values to argument Y of Z, then there exist W and @ARGS such that the number of instances in the class described by W is greater than or equal to X

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 3148-3151 For all Entity Y: equal length of (@ROW and Y) and (length of (@ROW)+1)
(forall (@ROW ?ITEM)
    (equal
        (ListOrderFn
            (ListFn @ROW ?ITEM)
            (ListLengthFn
                (ListFn @ROW ?ITEM))) ?ITEM))		 Merge.kif 3153-3157 For all Entity Y: equal length of (@ROW and Y)th element of (@ROW and Y) and Y
(forall (@ROW ?ITEM)
    (initialList
        (ListFn @ROW)
        (ListFn @ROW ?ITEM)))		 Merge.kif 3428-3429 For all Entity Y: (@ROW) starts (@ROW and Y)


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


Sigma web home      Suggested Upper Merged Ontology (SUMO) web home
Sigma version 3.0.0-0a80e6c8 (2026-05-12) is open source software produced by Articulate Software and its partners