inList - Sigma Knowledge base Browser

appearance as argument number 1

(documentation inList ChineseLanguage "这是类似 List 的 element 和 instance。 (inList ?OBJ ?LIST) 的意思是 ?OBJ 是在 ?LIST List 里。例如： (inList Tuesday (ListFn Monday Tuesday Wednesday)) 是真的")	Merge.kif 3313-3315
(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 3310-3312
(domain inList 1 Entity)	Merge.kif 3308-3308	The number 1 argument of in list is an instance of entity
(domain inList 2 List)	Merge.kif 3309-3309	The number 2 argument of in list is an instance of list
(instance inList AsymmetricRelation)	Merge.kif 3306-3306	in list is an instance of asymmetric relation
(instance inList BinaryPredicate)	Merge.kif 3304-3304	in list is an instance of binary predicate
(instance inList IrreflexiveRelation)	Merge.kif 3305-3305	in list is an instance of irreflexive relation
(instance inList PartialValuedRelation)	Merge.kif 3307-3307	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 92-92
(subrelation albumTrack inList)	Music.kif 335-335	album track is a subrelation of in list
(termFormat ChineseLanguage inList "在列表内")	chinese_format.kif 132-132	"在列表内" is the printable form of in list in ChineseLanguage
(termFormat EnglishLanguage inList "in list")	domainEnglishFormat.kif 5449-5449	"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	If an entity is a member of a list and the list is an instance of search results, then there exists a corpuscular object such that the corpuscular object is an instance of search results page and the list is a component of the corpuscular object
(=> (and (inList ?ITEM ?RESULTS) (instance ?RESULTS SRPResults)) (or (instance ?ITEM WebListing) (instance ?ITEM WebPage)))	UXExperimentalTerms.kif 2690-2696	If an entity is a member of a list and the list is an instance of search results, then the entity is an instance of web listing or the entity is an instance of WebPage
(=> (and (instance ?REL IntentionalRelation) (?REL ?AGENT @ROW) (inList ?OBJ (ListFn @ROW))) (inScopeOfInterest ?AGENT ?OBJ))	Merge.kif 2859-2864	If an entity is an instance of intentional relation and the entity a cognitive agent and @ROW and a third entity is a member of (@ROW), then the cognitive agent is interested in the third 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 17237-17245	If an object is a positional attribute to another object and @ROW is the opposite of and the positional attribute is a member of (@ROW) and another positional attribute is a member of (@ROW) and the positional attribute is not equal to the other positional attribute, then the object is not the other positional attribute to the other object
(=> (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	If the list of processes @ROW and a physical is a member of (@ROW) and another physical is a member of (@ROW) and another entity element of (@ROW) is equal to the physical and a third entity element of (@ROW) is equal to the other physical and a positive integer is less than another positive integer, then the time of existence of the physical happens earlier than the time of existence of the other physical
(=> (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	If %2 is the list of items viewed by 1 and a process is a member of a list, then the process is an instance of AccessingWebPage and an agent is an agent of another process and there exists an entity such that the entity is an instance of WebPage and the process ends up at WebPage
(=> (inList ?ITEM ?LIST) (exists (?NUMBER) (equal (ListOrderFn ?LIST ?NUMBER) ?ITEM)))	Merge.kif 3317-3320	If an entity is a member of a list, then there exists a positive integer such that the positive integerth element of the list is equal to the entity

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 if the positive integer is a member of the other list, then there exist a quantity, the quantityMINUSONE,, , another positive integer and a third positive integer such that the quantity is greater than 1 and the quantity is less than or equal to length of the other list and the positive integerth element of the other list is equal to the quantity and the other positive integer is a member of the list and the quantity is equal to the other positive integerth element of the list and the third positive integer is a member of the other list and the quantityMINUSONE is equal to (the quantity and 1) and the quantityMINUSONE is equal to the third positive integerth element of the other list and the positive integer is equal to (the other positive integer and the third 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 if the listITEM is a member of the list, then the listITEM is an instance of a symbolic string and there doesn't exist another entity such that the other entity is an instance of the symbolic string and the other entity is not a member of the list and the other integer is equal to the number of instances in the class described by the symbolic string 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 if the listITEM is a member of the list, then the listITEM is an instance of a symbolic string and there doesn't exist another entity such that the other entity is an instance of the symbolic string and the other entity is not a member of the list and the other integer is equal to the number of instances in the class described by the symbolic string 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 if the listITEM is a member of the list, then the listITEM is an instance of a symbolic string and there doesn't exist another entity such that the other entity is an instance of the symbolic string and the other entity is not a member of the list and the other integer is equal to the number of instances in the class described by the symbolic string 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	If a cognitive agent is a performer on an album, then there exist a content bearing object and a process such that the content bearing object is an instance of recording and the content bearing object is a member of the album and the content bearing object is a record of the process and the cognitive agent is an agent of the process
(=> (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	If a kind of DataStorageDevice is equal to the set of copies on a kind of DataStorageDeviceS of an album and an entity is an instance of the kind of DataStorageDevice, then for all an object if the object is a member of the album, then there exists a content bearing object such that the content bearing object is a copy of the object and the content bearing object is stored on the kind of DataStorageDevice
(=> (and (instance ?ATTR RecordingAttribute) (albumType ?A ?ATTR)) (forall (?R) (=> (inList ?R ?M) (attribute ?R ?A))))	Music.kif 291-298	If a relational attribute is an instance of recording attribute and an album is a the relational attribute, then for all an object if the object is a member of a list, then the album is an attribute of the object
(=> (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	If an object is an instance of DigitalDataStorageDevice and a symbolic string is a part of the object and the symbolic string is an instance of digital data, then there exist a CodeMap and a list such that the symbolic string in the CodeMap denotes an entity and the list expresses the CodeMap and if the entity is a member of the list, then the entity is an instance of binary number
(=> (average ?LIST ?AVERAGE) (forall (?LISTITEM) (=> (inList ?LISTITEM ?LIST) (instance ?LISTITEM RealNumber))))	Merge.kif 5465-5470	If a real number is an average of a list, then for all the listITEM if the listITEM is a member of the list, then the listITEM is an instance of real number
(=> (contraryAttribute @ROW) (=> (inList ?ELEMENT (ListFn @ROW)) (instance ?ELEMENT Attribute)))	Merge.kif 516-520	If @ROW is the opposite of , then if another entity is a member of (@ROW), then the other entity is an instance of attribute
(=> (disjointDecomposition ?CLASS @ROW) (forall (?ITEM) (=> (inList ?ITEM (ListFn @ROW)) (subclass ?ITEM ?CLASS))))	Merge.kif 3146-3151	If a class is disjointly decomposed into @ROW, then for all a set or class if the set or class is a member of (@ROW), then the set or class is a subclass of the 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 3153-3162	If a class is disjointly decomposed into @ROW, then for all a set or class and another set or class if the set or class is a member of (@ROW) and the other set or class is a member of (@ROW) and the set or class is not equal to the other set or class, then the set or class is disjoint from the other set or class
(=> (disjointDecomposition @ROW) (=> (inList ?ELEMENT (ListFn @ROW)) (instance ?ELEMENT Class)))	Merge.kif 628-632	If @ROW is disjointly decomposed into @ROW, then if another entity is a member of (@ROW), then the other entity is an instance of class
(=> (equal (GreatestCommonDivisorFn @ROW) ?NUMBER) (=> (inList ?ELEMENT (ListFn @ROW)) (instance ?ELEMENT Number)))	Merge.kif 5016-5021	If the greatest common divisor of @ROW is equal to an integer, then if another entity is a member of (@ROW), then the other entity is an instance of number
(=> (equal (GreatestCommonDivisorFn @ROW) ?NUMBER) (forall (?ELEMENT) (=> (inList ?ELEMENT (ListFn @ROW)) (equal (RemainderFn ?ELEMENT ?NUMBER) 0))))	Merge.kif 5023-5028	If the greatest common divisor of @ROW is equal to an integer, then for all another integer if the other integer is a member of (@ROW), then the other integer mod the integer is equal to 0
(=> (equal (GreatestCommonDivisorFn @ROW) ?NUMBER) (not (exists (?GREATER) (and (greaterThan ?GREATER ?NUMBER) (forall (?ELEMENT) (=> (inList ?ELEMENT (ListFn @ROW)) (equal (RemainderFn ?ELEMENT ?GREATER) 0)))))))	Merge.kif 5030-5038	If the greatest common divisor of @ROW is equal to an integer, then there doesn't exist another integer such that the other integer is greater than the integer and for all a third integer if the third integer is a member of (@ROW), then the third integer mod the other integer is equal to 0
(=> (equal (LeastCommonMultipleFn @ROW) ?NUMBER) (=> (inList ?ELEMENT (ListFn @ROW)) (instance ?ELEMENT Number)))	Merge.kif 5095-5100	If the least common multiple of @ROW is equal to an integer, then if another entity is a member of (@ROW), then the other entity is an instance of number
(=> (equal (LeastCommonMultipleFn @ROW) ?NUMBER) (forall (?ELEMENT) (=> (inList ?ELEMENT (ListFn @ROW)) (equal (RemainderFn ?NUMBER ?ELEMENT) 0))))	Merge.kif 5102-5107	If the least common multiple of @ROW is equal to an integer, then for all another integer if the other integer is a member of (@ROW), then the integer mod the other integer is equal to 0
(=> (equal (LeastCommonMultipleFn @ROW) ?NUMBER) (not (exists (?LESS) (and (lessThan ?LESS ?NUMBER) (forall (?ELEMENT) (=> (inList ?ELEMENT (ListFn @ROW)) (equal (RemainderFn ?LESS ?ELEMENT) 0)))))))	Merge.kif 5109-5117	If the least common multiple of @ROW is equal to an integer, then there doesn't exist another integer such that the other integer is less than the integer and for all a third integer if the third integer is a member of (@ROW), then the other integer mod the third integer is equal to 0
(=> (exhaustiveAttribute ?CLASS @ROW) (=> (inList ?ATTR (ListFn @ROW)) (instance ?ATTR Attribute)))	Merge.kif 554-558	If @ROW are all the attributes of another kind of attribute, then if an entity is a member of (@ROW), then the entity 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 560-568	If @ROW are all the attributes of another kind of attribute, then for all an entity if the entity is an instance of another kind of attribute, then there exists another entity such that the other entity is a member of (@ROW) and the entity is equal to the other entity
(=> (exhaustiveDecomposition ?CLASS @ROW) (forall (?OBJ) (=> (instance ?OBJ ?CLASS) (exists (?ITEM) (and (inList ?ITEM (ListFn @ROW)) (instance ?OBJ ?ITEM))))))	Merge.kif 3136-3144	If a class is covered by @ROW, then for all an entity if the entity is an instance of the class, then there exists a set or class such that the set or class is a member of (@ROW) and the entity is an instance of the set or class
(=> (exhaustiveDecomposition @ROW) (=> (inList ?ELEMENT (ListFn @ROW)) (instance ?ELEMENT Class)))	Merge.kif 611-615	If @ROW is covered by @ROW, then if another entity is a member of (@ROW), then the other entity is an instance of class
(=> (instance ?L Album) (forall (?X) (=> (inList ?X ?L) (instance ?X Recording))))	Music.kif 53-58	If a list is an instance of album, then for all an entity if the entity is a member of the list, then the entity is an instance of recording
(=> (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	If a process is an instance of shuttle, then there exist a list, an object and an agent such that the agent is an agent of the process and the agent possesses the object and the object is an instance of automobile and the list is an instance of list and for all an entity if the entity is a member of the list, then the entity is an instance of PostalPlace and there exists another process such that the other process is an instance of transportation and the agent is an agent of the other process and the object is an instrument for the other process and the other process ends up at the entity

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

KB Term:			Term intersection

English Word: