Browsing Interface : Welcome guest : log in
Home |  Graph |  ]  KB:  Language:   

Formal Language: 



KB Term:  Term intersection
English Word: 

Sigma KEE - inList
inList

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


(documentation inList ChineseLanguage "这是类似 Listelementinstance。 (inList ?OBJ ?LIST) 的意思是 ?OBJ 是在 ?LIST List 里。例如: (inList Tuesday (ListFn Monday Tuesday Wednesday)) 是真的") Merge.kif 4909-4911
(documentation inList EnglishLanguage "The analog of element and instance for Lists. (inList ?OBJ ?LIST) means that ?OBJ is in the List ?LIST. For example, (inList Tuesday (ListFn Monday Tuesday Wednesday)) would be true.") Merge.kif 4905-4907
(documentation inList JapaneseLanguage "Lists の elementinstance のアナログ。 (inList ?OBJ ?LIST)とは、?OBJ が List ?LIST 内であることを意味する。例: (inList Tuesday (ListFn Monday Tuesday Wednesday)) は正しい。") Merge.kif 4914-4916
(domain inList 1 Entity) Merge.kif 4902-4902 The number 1 argument of in list is an instance of entity
(domain inList 2 List) Merge.kif 4903-4903 The number 2 argument of in list is an instance of list
(instance inList AsymmetricRelation) Merge.kif 4900-4900 in list is an instance of asymmetric relation
(instance inList BinaryPredicate) Merge.kif 4898-4898 in list is an instance of binary predicate
(instance inList IrreflexiveRelation) Merge.kif 4899-4899 in list is an instance of irreflexive relation
(instance inList PartialValuedRelation) Merge.kif 4901-4901 in list is an instance of partial valued relation

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


(format ChineseLanguage inList "%1 %n 是 %2 的 member") chinese_format.kif 131-131
(format EnglishLanguage inList "%1 is %n a member of %2") english_format.kif 171-171
(format JapaneseLanguage inList "%1 は %2 の member では %n") english_format.kif 172-172
(subrelation albumTrack inList) Music.kif 335-335 album track is a subrelation of in list
(termFormat ChineseLanguage inList "在列表中") domainEnglishFormat.kif 30097-30097 "在列表中" is the printable form of in list in ChineseLanguage
(termFormat ChineseLanguage inList "在列表内") chinese_format.kif 132-132 "在列表内" is the printable form of in list in ChineseLanguage
(termFormat ChineseTraditionalLanguage inList "在列表中") domainEnglishFormat.kif 30096-30096 "在列表中" is the printable form of in list in ChineseTraditionalLanguage
(termFormat EnglishLanguage inList "in list") domainEnglishFormat.kif 30095-30095 "in list" is the printable form of in list in english language

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


(=>
    (and
        (inList ?ITEM ?RESULTS)
        (instance ?RESULTS SRPResults))
    (exists (?SRP)
        (and
            (instance ?SRP SearchResultsPage)
            (component ?RESULTS ?SRP))))
UXExperimentalTerms.kif 2698-2705
(=>
    (and
        (inList ?ITEM ?RESULTS)
        (instance ?RESULTS SRPResults))
    (or
        (instance ?ITEM WebListing)
        (instance ?ITEM WebPage)))
UXExperimentalTerms.kif 2690-2696
(=>
    (and
        (instance ?REL IntentionalRelation)
        (?REL ?AGENT @ROW)
        (inList ?OBJ
            (ListFn @ROW)))
    (inScopeOfInterest ?AGENT ?OBJ))
Merge.kif 4334-4339
(=>
    (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 21609-21617
(=>
    (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 690-698
(=>
    (and
        (viewedItemList ?USER ?LIST)
        (inList ?ACCESSING ?LIST))
    (and
        (instance ?ACCESSING AccessingWebPage)
        (agent ?ACESSING ?USER)
        (exists (?DEST)
            (and
                (instance ?DEST WebPage)
                (destination ?ACCESSING WebPage)))))
UXExperimentalTerms.kif 961-971
(=>
    (inList ?ITEM ?LIST)
    (exists (?NUMBER)
        (equal
            (ListOrderFn ?LIST ?NUMBER) ?ITEM)))
Merge.kif 4918-4921

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


(<=>
    (average ?LIST1 ?AVERAGE)
    (exists (?LIST2)
        (and
            (equal
                (ListLengthFn ?LIST2)
                (ListLengthFn ?LIST1))
            (equal
                (ListOrderFn ?LIST2 1)
                (ListOrderFn ?LIST1 1))
            (forall (?ITEMFROM2)
                (=>
                    (inList ?ITEMFROM2 ?LIST2)
                    (exists (?POSITION ?POSITIONMINUSONE ?ITEMFROM1 ?PRIORFROM2)
                        (and
                            (greaterThan ?POSITION 1)
                            (lessThanOrEqualTo ?POSITION
                                (ListLengthFn ?LIST2))
                            (equal
                                (ListOrderFn ?LIST2 ?ITEMFROM2) ?POSITION)
                            (inList ?ITEMFROM1 ?LIST1)
                            (equal ?POSITION
                                (ListOrderFn ?LIST1 ?ITEMFROM1))
                            (inList ?PRIORFROM2 ?LIST2)
                            (equal ?POSITIONMINUSONE
                                (SubtractionFn ?POSITION 1))
                            (equal ?POSITIONMINUSONE
                                (ListOrderFn ?LIST2 ?PRIORFROM2))
                            (equal ?ITEMFROM2
                                (AdditionFn ?ITEMFROM1 ?PRIORFROM2))))))
            (equal ?LASTPLACE
                (ListLengthFn ?LIST2))
            (equal ?AVERAGE
                (DivisionFn
                    (ListOrderFn ?LIST2 ?LASTPLACE) ?LASTPLACE)))))
People.kif 285-306 A real number is an average of a list if and only if there exists another list such that length of the other list is equal to length of the list and 1th element of the other list is equal to 1th element of the list and for all a positive integer and a fourth positive integer is equal to length of the other list and the real number is equal to the fourth positive integerth element of the other list and the fourth positive integer
(<=>
    (equal
        (FemaleLifeExpectancyAtBirthFn ?AREA
            (YearFn ?YEAR)) ?REALNUMBER)
    (exists (?LIST)
        (and
            (instance ?LIST List)
            (instance
                (ListLengthFn ?LIST) ?COUNT)
            (forall (?LISTITEM)
                (=>
                    (inList ?LISTITEM ?LIST)
                    (and
                        (instance ?LISTITEM ?LIFEEXPECTANCYAGE)
                        (not
                            (exists (?NUMBER)
                                (and
                                    (instance ?NUMBER ?LIFEEXPECTANCYAGE)
                                    (not
                                        (inList ?NUMBER ?LIST)))))
                        (equal ?COUNT
                            (CardinalityFn
                                (KappaFn ?LIFEEXPECTANCYAGE
                                    (and
                                        (instance ?BIRTH Birth)
                                        (experiencer ?BIRTH ?INDIVIDUAL)
                                        (instance ?INDIVIDUAL Human)
                                        (attribute ?INDIVIDUAL Female)
                                        (during
                                            (WhenFn ?BIRTH)
                                            (YearFn ?YEAR))
                                        (equal
                                            (WhereFn ?BIRTH
                                                (WhenFn ?BIRTH)) ?AREA)
                                        (instance ?DEATH Death)
                                        (experiencer ?DEATH ?INDIVIDUAL)
                                        (holdsDuring
                                            (WhenFn ?DEATH)
                                            (age ?INDIVIDUAL
                                                (MeasureFn ?LIFEEXPECTANCYAGE YearDuration))))))))))
            (average ?LIST ?REALNUMBER))))
People.kif 411-442 The female life expectancy at birth of a geopolitical area and the year an integer is equal to a real number if and only if there exists a list such that the list is an instance of list and length of the list is an instance of another integer and for all the listITEM and the real number is an average of the list
(<=>
    (equal
        (LifeExpectancyAtBirthFn ?AREA
            (YearFn ?YEAR)) ?REALNUMBER)
    (exists (?LIST)
        (and
            (instance ?LIST List)
            (instance
                (ListLengthFn ?LIST) ?COUNT)
            (forall (?LISTITEM)
                (=>
                    (inList ?LISTITEM ?LIST)
                    (and
                        (instance ?LISTITEM ?LIFEEXPECTANCYAGE)
                        (not
                            (exists (?NUMBER)
                                (and
                                    (instance ?NUMBER ?LIFEEXPECTANCYAGE)
                                    (not
                                        (inList ?NUMBER ?LIST)))))
                        (equal ?COUNT
                            (CardinalityFn
                                (KappaFn ?LIFEEXPECTANCYAGE
                                    (and
                                        (instance ?BIRTH Birth)
                                        (experiencer ?BIRTH ?INDIVIDUAL)
                                        (instance ?INDIVIDUAL Human)
                                        (during
                                            (WhenFn ?BIRTH)
                                            (YearFn ?YEAR))
                                        (equal
                                            (WhereFn ?BIRTH
                                                (WhenFn ?BIRTH)) ?AREA)
                                        (instance ?DEATH Death)
                                        (experiencer ?DEATH ?INDIVIDUAL)
                                        (holdsDuring
                                            (WhenFn ?DEATH)
                                            (age ?INDIVIDUAL
                                                (MeasureFn ?LIFEEXPECTANCYAGE YearDuration))))))))))
            (average ?LIST ?REALNUMBER))))
People.kif 323-353 The life expectancy at birth of a geopolitical area and the year an integer is equal to a real number if and only if there exists a list such that the list is an instance of list and length of the list is an instance of another integer and for all the listITEM and the real number is an average of the list
(<=>
    (equal
        (MaleLifeExpectancyAtBirthFn ?AREA
            (YearFn ?YEAR)) ?REALNUMBER)
    (exists (?LIST)
        (and
            (instance ?LIST List)
            (instance
                (ListLengthFn ?LIST) ?COUNT)
            (forall (?LISTITEM)
                (=>
                    (inList ?LISTITEM ?LIST)
                    (and
                        (instance ?LISTITEM ?LIFEEXPECTANCYAGE)
                        (not
                            (exists (?NUMBER)
                                (and
                                    (instance ?NUMBER ?LIFEEXPECTANCYAGE)
                                    (not
                                        (inList ?NUMBER ?LIST)))))
                        (equal ?COUNT
                            (CardinalityFn
                                (KappaFn ?LIFEEXPECTANCYAGE
                                    (and
                                        (instance ?BIRTH Birth)
                                        (experiencer ?BIRTH ?INDIVIDUAL)
                                        (instance ?INDIVIDUAL Human)
                                        (attribute ?INDIVIDUAL Male)
                                        (during
                                            (WhenFn ?BIRTH)
                                            (YearFn ?YEAR))
                                        (equal
                                            (WhereFn ?BIRTH
                                                (WhenFn ?BIRTH)) ?AREA)
                                        (instance ?DEATH Death)
                                        (experiencer ?DEATH ?INDIVIDUAL)
                                        (holdsDuring
                                            (WhenFn ?DEATH)
                                            (age ?INDIVIDUAL
                                                (MeasureFn ?LIFEEXPECTANCYAGE YearDuration))))))))))
            (average ?LIST ?REALNUMBER))))
People.kif 367-398 The male life expectancy at birth of a geopolitical area and the year an integer is equal to a real number if and only if there exists a list such that the list is an instance of list and length of the list is an instance of another integer and for all the listITEM and the real number is an average of the list
(=>
    (albumArtist ?A ?P)
    (exists (?R ?M)
        (and
            (instance ?R Recording)
            (inList ?R ?A)
            (record ?R ?M)
            (agent ?M ?P))))
Music.kif 274-281
(=>
    (and
        (equal ?D
            (AlbumCopiesFn ?A ?DS))
        (instance ?X ?D))
    (forall (?S)
        (=>
            (inList ?S ?A)
            (exists (?C)
                (and
                    (copy ?C ?S)
                    (stored ?C ?D))))))
Music.kif 936-946
(=>
    (and
        (instance ?ATTR RecordingAttribute)
        (albumType ?A ?ATTR))
    (forall (?R)
        (=>
            (inList ?R ?M)
            (attribute ?R ?A))))
Music.kif 291-298
(=>
    (and
        (instance ?OBJ DigitalDataStorageDevice)
        (part ?PART ?OBJ)
        (instance ?PART DigitalData))
    (exists (?SCHEME ?LIST)
        (and
            (codeMapping ?SCHEME ?PART ?NUM)
            (represents ?LIST ?SCHEME)
            (=>
                (inList ?NUM ?LIST)
                (instance ?NUM BinaryNumber)))))
Media.kif 801-812
(=>
    (average ?LIST ?AVERAGE)
    (forall (?LISTITEM)
        (=>
            (inList ?LISTITEM ?LIST)
            (instance ?LISTITEM RealNumber))))
Merge.kif 7757-7762
(=>
    (contraryAttribute @ROW)
    (=>
        (inList ?ELEMENT
            (ListFn @ROW))
        (instance ?ELEMENT Attribute)))
Merge.kif 688-692
(=>
    (disjointDecomposition ?CLASS @ROW)
    (forall (?ITEM)
        (=>
            (inList ?ITEM
                (ListFn @ROW))
            (subclass ?ITEM ?CLASS))))
Merge.kif 4721-4726
(=>
    (disjointDecomposition ?CLASS @ROW)
    (forall (?ITEM1 ?ITEM2)
        (=>
            (and
                (inList ?ITEM1
                    (ListFn @ROW))
                (inList ?ITEM2
                    (ListFn @ROW))
                (not
                    (equal ?ITEM1 ?ITEM2)))
            (disjoint ?ITEM1 ?ITEM2))))
Merge.kif 4728-4737
(=>
    (disjointDecomposition @ROW)
    (=>
        (inList ?ELEMENT
            (ListFn @ROW))
        (instance ?ELEMENT Class)))
Merge.kif 835-839
(=>
    (equal
        (GreatestCommonDivisorFn @ROW) ?NUMBER)
    (=>
        (inList ?ELEMENT
            (ListFn @ROW))
        (instance ?ELEMENT Number)))
Merge.kif 7187-7192
(=>
    (equal
        (GreatestCommonDivisorFn @ROW) ?NUMBER)
    (forall (?ELEMENT)
        (=>
            (inList ?ELEMENT
                (ListFn @ROW))
            (equal
                (RemainderFn ?ELEMENT ?NUMBER) 0))))
Merge.kif 7194-7199
(=>
    (equal
        (GreatestCommonDivisorFn @ROW) ?NUMBER)
    (not
        (exists (?GREATER)
            (and
                (greaterThan ?GREATER ?NUMBER)
                (forall (?ELEMENT)
                    (=>
                        (inList ?ELEMENT
                            (ListFn @ROW))
                        (equal
                            (RemainderFn ?ELEMENT ?GREATER) 0)))))))
Merge.kif 7201-7209
(=>
    (equal
        (LeastCommonMultipleFn @ROW) ?NUMBER)
    (=>
        (inList ?ELEMENT
            (ListFn @ROW))
        (instance ?ELEMENT Number)))
Merge.kif 7286-7291
(=>
    (equal
        (LeastCommonMultipleFn @ROW) ?NUMBER)
    (forall (?ELEMENT)
        (=>
            (inList ?ELEMENT
                (ListFn @ROW))
            (equal
                (RemainderFn ?NUMBER ?ELEMENT) 0))))
Merge.kif 7293-7298
(=>
    (equal
        (LeastCommonMultipleFn @ROW) ?NUMBER)
    (not
        (exists (?LESS)
            (and
                (lessThan ?LESS ?NUMBER)
                (forall (?ELEMENT)
                    (=>
                        (inList ?ELEMENT
                            (ListFn @ROW))
                        (equal
                            (RemainderFn ?LESS ?ELEMENT) 0)))))))
Merge.kif 7300-7308
(=>
    (exhaustiveAttribute ?CLASS @ROW)
    (=>
        (inList ?ATTR
            (ListFn @ROW))
        (instance ?ATTR Attribute)))
Merge.kif 740-744
(=>
    (exhaustiveAttribute ?CLASS @ROW)
    (forall (?ATTR1)
        (=>
            (instance ?ATTR1 ?CLASS)
            (exists (?ATTR2)
                (and
                    (inList ?ATTR2
                        (ListFn @ROW))
                    (equal ?ATTR1 ?ATTR2))))))
Merge.kif 746-754
(=>
    (exhaustiveDecomposition ?CLASS @ROW)
    (forall (?OBJ)
        (=>
            (instance ?OBJ ?CLASS)
            (exists (?ITEM)
                (and
                    (inList ?ITEM
                        (ListFn @ROW))
                    (instance ?OBJ ?ITEM))))))
Merge.kif 4711-4719
(=>
    (exhaustiveDecomposition @ROW)
    (=>
        (inList ?ELEMENT
            (ListFn @ROW))
        (instance ?ELEMENT Class)))
Merge.kif 810-814
(=>
    (instance ?L Album)
    (forall (?X)
        (=>
            (inList ?X ?L)
            (instance ?X Recording))))
Music.kif 53-58
(=>
    (instance ?SVC ShuttleService)
    (exists (?LIST ?VEHICLE ?AGENT)
        (and
            (agent ?SVC ?AGENT)
            (possesses ?AGENT ?VEHICLE)
            (instance ?VEHICLE Automobile)
            (instance ?LIST List)
            (forall (?X)
                (=>
                    (inList ?X ?LIST)
                    (and
                        (instance ?X PostalPlace)
                        (exists (?TRANSPORT)
                            (and
                                (instance ?TRANSPORT Transportation)
                                (agent ?TRANSPORT ?AGENT)
                                (instrument ?TRANSPORT ?VEHICLE)
                                (destination ?TRANSPORT ?X)))))))))
Hotel.kif 1979-1997

Display limited to 25 items. Show next 25

Display limited to 25 items. Show next 25


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 2.99c (>= 2017/11/20) is open source software produced by Articulate Software and its partners