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

Formal Language: 



KB Term:  Term intersection
English Word: 

  inList

 Sigma KEE - inList
inList

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


(documentation inList ChineseLanguage "这是类似 List 的 element 和 instance。 (inList ?OBJ ?LIST) 的意思是 ?OBJ 是在 ?LIST List 里。例如： (inList Tuesday (ListFn Monday Tuesday Wednesday)) 是真的") chinese_format.kif 1973-1975
(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 3037-3039
(domain inList 1 Entity) Merge.kif 3034-3034
(domain inList 2 List) Merge.kif 3035-3035
(instance inList BinaryPredicate) Merge.kif 3032-3032
(instance inList PartialValuedRelation) Merge.kif 3033-3033

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 132-132
(subrelation albumTrack inList) Music.kif 330-330
(termFormat ChineseLanguage inList "在列表中") domainEnglishFormat.kif 30180-30180
(termFormat ChineseLanguage inList "在列表内") chinese_format.kif 132-132
(termFormat ChineseTraditionalLanguage inList "在列表中") domainEnglishFormat.kif 30179-30179
(termFormat EnglishLanguage inList "in list") domainEnglishFormat.kif 30178-30178

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


(=>
    (and
        (equal ?A
            (AverageFn ?L))
        (inList ?N ?L))
    (instance ?N Number))		 Merge.kif 3215-3219
(=>
    (and
        (equal ?SPEEDLIST
            (Mean3SecondWindSpeedListFn ?PLACE ?TIME))
        (inList ?SPEED ?SPEEDLIST))
    (exists (?TIMELIST ?INT)
        (and
            (equal ?TIMELIST
                (TimeIntervalListFn ?TIME
                    (MeasureFn 3 SecondDuration)))
            (inList ?INT ?TIMELIST)
            (equal ?SPEED
                (Mean3SecondWindSpeedFn ?PLACE ?INT)))))		 Weather.kif 2004-2016
(=>
    (and
        (equal ?SPEEDLIST
            (Mean3SecondWindSpeedListFn ?PLACE ?TIME))
        (inList ?SPEED ?SPEEDLIST))
    (instance ?SPEED FunctionQuantity))		 Weather.kif 1997-2002
(=>
    (and
        (exhaustiveAttribute ?CLASS @ROW)
        (inList ?ATTR
            (ListFn @ROW)))
    (instance ?ATTR ?CLASS))		 Merge.kif 503-507
(=>
    (and
        (exhaustiveAttribute ?CLASS @ROW)
        (inList ?ATTR
            (ListFn @ROW)))
    (instance ?ATTR Attribute))		 Merge.kif 497-501
(=>
    (and
        (inList ?E ?L)
        (equal ?L
            (AmountsFn ?S ?CO ?U)))
    (instance ?E RationalNumber))		 Merge.kif 7486-7491
(=>
    (and
        (inList ?INT ?LIST)
        (equal ?LIST
            (TimeIntervalListFn ?TIME ?DUR)))
    (duration ?INT ?DUR))		 Weather.kif 1974-1979
(=>
    (and
        (inList ?INT ?LIST)
        (equal ?LIST
            (TimeIntervalListFn ?TIME ?DUR)))
    (equal
        (BeginFn ?TIME)
        (BeginFn
            (FirstFn ?LIST))))		 Weather.kif 1965-1972
(=>
    (and
        (inList ?ITEM ?RESULTS)
        (instance ?RESULTS SRPResults))
    (exists (?SRP)
        (and
            (instance ?SRP SearchResultsPage)
            (component ?RESULTS ?SRP))))		 UXExperimentalTerms.kif 2701-2708
(=>
    (and
        (inList ?ITEM ?RESULTS)
        (instance ?RESULTS SRPResults))
    (or
        (instance ?ITEM WebListing)
        (instance ?ITEM WebPage)))		 UXExperimentalTerms.kif 2693-2699
(=>
    (and
        (instance ?LIST ConsecutiveTimeIntervalList)
        (inList ?TIME ?LIST))
    (instance ?Time TimeInterval))		 Weather.kif 1928-1932
(=>
    (and
        (instance ?LIST MeasuringList)
        (inList ?M ?LIST))
    (instance ?M Measuring))		 Weather.kif 1715-1719
(=>
    (and
        (instance ?LIST MeasuringResultList)
        (inList ?R ?LIST))
    (instance ?R PhysicalQuantity))		 Weather.kif 1783-1787
(=>
    (and
        (instance ?LIST MeasuringSurfaceWindSpeedList)
        (inList ?M ?LIST))
    (instance ?M SurfaceWindSpeedMeasuring))		 Weather.kif 1749-1753
(=>
    (and
        (instance ?LIST NumberList)
        (inList ?NUM ?LIST))
    (instance ?NUM Number))		 Weather.kif 1818-1822
(=>
    (and
        (instance ?REL IntentionalRelation)
        (?REL ?AGENT @ROW)
        (inList ?OBJ
            (ListFn @ROW)))
    (inScopeOfInterest ?AGENT ?OBJ))		 Merge.kif 2617-2622
(=>
    (and
        (locationMeasuringList ?LIST ?PLACE)
        (inList ?M ?LIST))
    (and
        (instance ?M Measuring)
        (eventLocated ?M ?PLACE)))		 Weather.kif 1768-1774
(=>
    (and
        (measuringListInterval ?LIST ?DUR)
        (inList ?M ?LIST))
    (duration
        (WhenFn ?M) ?DUR))		 Weather.kif 1859-1863
(=>
    (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 16639-16647
(=>
    (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
(=>
    (and
        (viewedItemList ?USER ?LIST)
        (inList ?ACCESSING ?LIST))
    (and
        (instance ?ACCESSING AccessingWebPage)
        (agent ?ACCESSING ?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 3041-3044

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


(<=>
    (and
        (instance ?Y
            (YearFn ?YEAR))
        (equal
            (MaleLifeExpectancyAtBirthFn ?AREA ?Y) ?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) ?Y)
                                        (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 372-405
(<=>
    (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 289-310
(<=>
    (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 418-449
(<=>
    (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 327-357
(=>
    (albumArtist ?A ?P)
    (exists (?R ?M)
        (and
            (instance ?R Recording)
            (inList ?R ?A)
            (record ?R ?M)
            (agent ?M ?P))))		 Music.kif 278-285
(=>
    (and
        (amount ?S ?CO
            (MeasureFn ?N ?U))
        (instance ?SI ?S)
        (measure ?SI
            (MeasureFn ?N2 ?U))
        (part ?SI ?CO))
    (exists (?L)
        (and
            (inList
                (MeasureFn ?N2 ?U) ?L)
            (equal ?L
                (AmountsFn ?S ?CO ?U))
            (equal ?N
                (ListSumFn ?L)))))		 Merge.kif 7500-7515
(=>
    (and
        (equal
            (GreatestCommonDivisorFn @ROW) ?NUMBER)
        (not
            (equal ?NUMBER 0)))
    (forall (?ELEMENT)
        (=>
            (inList ?ELEMENT
                (ListFn @ROW))
            (equal
                (RemainderFn ?ELEMENT ?NUMBER) 0))))		 Merge.kif 4765-4776
(=>
    (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
(=>
    (and
        (equal
            (LeastCommonMultipleFn @ROW) ?NUMBER)
        (not
            (equal ?NUMBER 0)))
    (forall (?ELEMENT)
        (=>
            (inList ?ELEMENT
                (ListFn @ROW))
            (equal
                (RemainderFn ?NUMBER ?ELEMENT) 0))))		 Merge.kif 4850-4860
(=>
    (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
(=>
    (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 931-941
(=>
    (and
        (equal ?SPEEDLIST
            (Mean3SecondWindSpeedListFn ?PLACE ?TIME))
        (inList ?SPEED ?SPEEDLIST))
    (exists (?TIMELIST ?INT)
        (and
            (equal ?TIMELIST
                (TimeIntervalListFn ?TIME
                    (MeasureFn 3 SecondDuration)))
            (inList ?INT ?TIMELIST)
            (equal ?SPEED
                (Mean3SecondWindSpeedFn ?PLACE ?INT)))))		 Weather.kif 2004-2016
(=>
    (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
(=>
    (and
        (instance ?WW WaterWave)
        (waveHeight ?WW ?WH))
    (exists (?LIST ?WA ?U)
        (and
            (inList ?WH ?LIST)
            (instance ?WA WaterArea)
            (eventLocated ?WW ?WA)
            (instance ?U LengthMeasure)
            (significantWaveHeight ?WA
                (WhenFn ?WW)
                (MeasureFn ?SWH ?U))
            (equal ?SWH
                (MultiplicationFn 4.0
                    (StandardDeviationFn ?LIST))))))		 Weather.kif 1531-1546
(=>
    (average ?LIST ?AVERAGE)
    (forall (?LISTITEM)
        (=>
            (inList ?LISTITEM ?LIST)
            (instance ?LISTITEM RealNumber))))		 Merge.kif 5269-5274
(=>
    (contraryAttribute @ROW)
    (=>
        (inList ?ELEMENT
            (ListFn @ROW))
        (instance ?ELEMENT Attribute)))		 Merge.kif 462-466
(=>
    (disjointDecomposition ?CLASS @ROW)
    (forall (?ITEM)
        (=>
            (inList ?ITEM
                (ListFn @ROW))
            (subclass ?ITEM ?CLASS))))		 Merge.kif 2878-2883
(=>
    (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 @ROW)
    (=>
        (inList ?ELEMENT
            (ListFn @ROW))
        (instance ?ELEMENT Class)))		 Merge.kif 574-578
(=>
    (equal
        (GreatestCommonDivisorFn @ROW) ?NUMBER)
    (=>
        (inList ?ELEMENT
            (ListFn @ROW))
        (instance ?ELEMENT Number)))		 Merge.kif 4758-4763
(=>
    (equal
        (LeastCommonMultipleFn @ROW) ?NUMBER)
    (=>
        (inList ?ELEMENT
            (ListFn @ROW))
        (instance ?ELEMENT Number)))		 Merge.kif 4843-4848
(=>
    (equal ?X
        (MaxValueFn ?LIST))
    (not
        (exists (?Y)
            (and
                (inList ?Y ?LIST)
                (greaterThan ?Y ?X)))))		 Weather.kif 1684-1691
(=>
    (exhaustiveAttribute ?CLASS @ROW)
    (forall (?ATTR1)
        (=>
            (instance ?ATTR1 ?CLASS)
            (exists (?ATTR2)
                (and
                    (inList ?ATTR2
                        (ListFn @ROW))
                    (equal ?ATTR1 ?ATTR2))))))		 Merge.kif 509-517
(=>
    (exhaustiveDecomposition ?CLASS @ROW)
    (forall (?OBJ)
        (=>
            (instance ?OBJ ?CLASS)
            (exists (?ITEM)
                (and
                    (inList ?ITEM
                        (ListFn @ROW))
                    (instance ?OBJ ?ITEM))))))		 Merge.kif 2868-2876
(=>
    (exhaustiveDecomposition @ROW)
    (=>
        (inList ?ELEMENT
            (ListFn @ROW))
        (instance ?ELEMENT Class)))		 Merge.kif 558-562

Display limited to 25 items. Show next 25

Display limited to 25 items. Show next 25


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

Show without tree


Sigma web home      Suggested Upper Merged Ontology (SUMO) web home
Sigma version 3.0 is open source software produced by Articulate Software and its partners