| appearance as argument number 1 |
|
| s__documentation(s__inList__m,s__ChineseLanguage,'这是类似 List 的 element 和 instance。 (inList ?OBJ ?LIST) 的意思是 ?OBJ 是在 ?LIST List 里。例如： (inList Tuesday (ListFn Monday Tuesday Wednesday)) 是真的')
|
Merge.kif 3300-3302 | |
| s__documentation(s__inList__m,s__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 3297-3299 | |
| s__domain(s__inList__m,1,s__Entity)
|
Merge.kif 3295-3295 | |
| s__domain(s__inList__m,2,s__List)
|
Merge.kif 3296-3296 | |
| s__instance(s__inList__m,s__AsymmetricRelation)
|
Merge.kif 3293-3293 | |
| s__instance(s__inList__m,s__BinaryPredicate)
|
Merge.kif 3291-3291 | |
| s__instance(s__inList__m,s__IrreflexiveRelation)
|
Merge.kif 3292-3292 | |
| s__instance(s__inList__m,s__PartialValuedRelation)
|
Merge.kif 3294-3294 |
| appearance as argument number 2 |
|
|
| s__format(s__ChineseLanguage,s__inList__m,'%1 %n 是 %2 的 member') | chinese_format.kif 131-131 | |
| s__format(s__EnglishLanguage,s__inList__m,'%1 is %n a member of %2')
|
english_format.kif 92-92 | |
| s__format(s__FrenchLanguage,s__inList__m,'%1 est %n un membre de %2')
|
french_format.kif 87-87 | |
| s__format(s__ItalianLanguage,s__inList__m,'%1 � %n un � membro di %2')
|
relations-it.txt 147-147 | |
| s__format(s__PortugueseLanguage,s__inList__m,'%1 e %n um membro de %2')
|
portuguese_format.kif 39-39 | |
| s__format(s__ar__m,s__inList__m,'%1 هو %n عُضْو في %2')
|
arabic_format.kif 37-37 | |
| s__format(s__cz__m,s__inList__m,'%1 %p{je} %n{nen�} a member of %2')
|
relations-cz.txt 103-103 | |
| s__format(s__de__m,s__inList__m,'%1 ist ein Mitglied von %2')
|
relations-de.txt 157-157 | |
| s__format(s__hi__m,s__inList__m,'%1 %2 kaa sadasya %n hai')
|
relations-hindi.txt 186-186 | |
| s__format(s__tg__m,s__inList__m,'%1 %n ay ang kasapi ng %2')
|
relations-tg.txt 298-298 | |
| s__subrelation(s__albumTrack__m,s__inList__m)
|
Music.kif 335-335 | |
| s__termFormat(s__ChineseLanguage,s__inList__m,'在列表内')
|
chinese_format.kif 132-132 | |
| s__termFormat(s__EnglishLanguage,s__inList__m,'in list')
|
domainEnglishFormat.kif 5449-5449 | |
| s__termFormat(s__ar__m,s__inList__m,'«عُضْو في»')
|
arabic_format.kif 487-487 | |
| s__termFormat(s__tg__m,s__inList__m,'sa mula')
|
relations-tg.txt 299-299 |
| antecedent |
|
|
| ( ! [V__ITEM,V__RESULTS] : ((s__inList(V__ITEM,V__RESULTS) & s__instance(V__RESULTS,s__SRPResults)) => (? [V__SRP] : (s__instance(V__SRP,s__SearchResultsPage) & s__component(V__RESULTS,V__SRP)))) )
|
UXExperimentalTerms.kif 2698-2705 | |
| ( ! [V__ITEM,V__RESULTS] : ((s__inList(V__ITEM,V__RESULTS) & s__instance(V__RESULTS,s__SRPResults)) => (s__instance(V__ITEM,s__WebListing) | s__instance(V__ITEM,s__WebPage))) )
|
UXExperimentalTerms.kif 2690-2696 | |
| ( ! [V__AGENT,V__ROW1,V__OBJ] : ((s__instance(s__considers__m,s__IntentionalRelation) & s__considers(V__AGENT,V__ROW1) & s__inList(V__OBJ,s__ListFn_1(V__ROW1))) => s__inScopeOfInterest(V__AGENT,V__OBJ)) )
|
Merge.kif 2846-2851 | |
| ( ! [V__OBJ1,V__OBJ2,V__ATTR1,V__ROW1,V__ATTR2] : ((s__orientation(V__OBJ1,V__OBJ2,V__ATTR1) & s__contraryAttribute_1(V__ROW1) & s__inList(V__ATTR1,s__ListFn_1(V__ROW1)) & s__inList(V__ATTR2,s__ListFn_1(V__ROW1)) & (~ (V__ATTR1 = V__ATTR2))) => (~ s__orientation(V__OBJ1,V__OBJ2,V__ATTR2))) )
|
Merge.kif 17185-17193 | |
| ( ! [V__ROW1,V__Process1,V__Process2,V__Number1,V__Number2] : ((s__processList_1(V__ROW1) & s__inList(V__Process1,s__ListFn_1(V__ROW1)) & s__inList(V__Process2,s__ListFn_1(V__ROW1)) & (s__ListOrderFn(s__ListFn_1(V__ROW1) ,V__Number1) = V__Process1) & (s__ListOrderFn(s__ListFn_1(V__ROW1) ,V__Number2) = V__Process2) & s__lessThan(V__Number1,V__Number2)) => s__earlier(s__WhenFn(V__Process1) ,s__WhenFn(V__Process2))) )
|
QoSontology.kif 675-683 | |
| ( ! [V__USER,V__LIST,V__ACCESSING,V__ACESSING] : ((s__viewedItemList(V__USER,V__LIST) & s__inList(V__ACCESSING,V__LIST)) => (s__instance(V__ACCESSING,s__AccessingWebPage) & s__agent(V__ACESSING,V__USER) & (? [V__DEST] : (s__instance(V__DEST,s__WebPage) & s__destination(V__ACCESSING,s__WebPage))))) )
|
UXExperimentalTerms.kif 961-971 | |
| ( ! [V__ITEM,V__LIST] : (s__inList(V__ITEM,V__LIST) => (? [V__NUMBER] : (s__ListOrderFn(V__LIST,V__NUMBER) = V__ITEM))) )
|
Merge.kif 3304-3307 |
| consequent |
|
|
| ( ! [V__LIST1,V__AVERAGE,V__LASTPLACE] : (s__average(V__LIST1,V__AVERAGE) <=> (? [V__LIST2] : ((s__ListLengthFn(V__LIST2) = s__ListLengthFn(V__LIST1)) & (s__ListOrderFn(V__LIST2,1) = s__ListOrderFn(V__LIST1,1)) & (! [V__ITEMFROM2] : (s__inList(V__ITEMFROM2,V__LIST2) => (? [V__POSITION,V__POSITIONMINUSONE,V__ITEMFROM1,V__PRIORFROM2] : (s__greaterThan(V__POSITION,1) & s__lessThanOrEqualTo(V__POSITION,s__ListLengthFn(V__LIST2)) & (s__ListOrderFn(V__LIST2,V__ITEMFROM2) = V__POSITION) & s__inList(V__ITEMFROM1,V__LIST1) & (V__POSITION = s__ListOrderFn(V__LIST1,V__ITEMFROM1)) & s__inList(V__PRIORFROM2,V__LIST2) & (V__POSITIONMINUSONE = s__SubtractionFn(V__POSITION,1)) & (V__POSITIONMINUSONE = s__ListOrderFn(V__LIST2,V__PRIORFROM2)) & (V__ITEMFROM2 = s__AdditionFn(V__ITEMFROM1,V__PRIORFROM2)))))) & (V__LASTPLACE = s__ListLengthFn(V__LIST2)) & (V__AVERAGE = s__DivisionFn(s__ListOrderFn(V__LIST2,V__LASTPLACE) ,V__LASTPLACE))))) )
|
People.kif 285-306 | |
| No TPTP formula. May not be expressible in strict first order. | People.kif 411-442 | |
| No TPTP formula. May not be expressible in strict first order. | People.kif 323-353 | |
| No TPTP formula. May not be expressible in strict first order. | People.kif 367-398 | |
| ( ! [V__A,V__P] : (s__albumArtist(V__A,V__P) => (? [V__R,V__M] : (s__instance(V__R,s__Recording) & s__inList(V__R,V__A) & s__record(V__R,V__M) & s__agent(V__M,V__P)))) )
|
Music.kif 274-281 | |
| ( ! [V__D,V__A,V__DS,V__X] : (((V__D = s__AlbumCopiesFn(V__A,V__DS)) & s__instance(V__X,V__D)) => (! [V__S] : (s__inList(V__S,V__A) => (? [V__C] : (s__copy(V__C,V__S) & s__stored(V__C,V__D)))))) )
|
Music.kif 936-946 | |
| ( ! [V__ATTR,V__A,V__M] : ((s__instance(V__ATTR,s__RecordingAttribute) & s__albumType(V__A,V__ATTR)) => (! [V__R] : (s__inList(V__R,V__M) => s__attribute(V__R,V__A)))) )
|
Music.kif 291-298 | |
| ( ! [V__OBJ,V__PART,V__NUM] : ((s__instance(V__OBJ,s__DigitalDataStorageDevice) & s__part(V__PART,V__OBJ) & s__instance(V__PART,s__DigitalData)) => (? [V__SCHEME,V__LIST] : (s__codeMapping(V__SCHEME,V__PART,V__NUM) & s__represents(V__LIST,V__SCHEME) & (s__inList(V__NUM,V__LIST) => s__instance(V__NUM,s__BinaryNumber))))) )
|
Media.kif 801-812 | |
| ( ! [V__LIST,V__AVERAGE] : (s__average(V__LIST,V__AVERAGE) => (! [V__LISTITEM] : (s__inList(V__LISTITEM,V__LIST) => s__instance(V__LISTITEM,s__RealNumber)))) )
|
Merge.kif 5452-5457 | |
| ( ! [V__ROW1,V__ELEMENT] : (s__contraryAttribute_1(V__ROW1) => (s__inList(V__ELEMENT,s__ListFn_1(V__ROW1)) => s__instance(V__ELEMENT,s__Attribute))) )
|
Merge.kif 516-520 | |
| ( ! [V__CLASS,V__ROW1] : (s__disjointDecomposition_2(V__CLASS,V__ROW1) => (! [V__ITEM] : (s__inList(V__ITEM,s__ListFn_1(V__ROW1)) => s__subclass(V__ITEM,V__CLASS)))) )
|
Merge.kif 3133-3138 | |
| ( ! [V__CLASS,V__ROW1] : (s__disjointDecomposition_2(V__CLASS,V__ROW1) => (! [V__ITEM1,V__ITEM2] : ((s__inList(V__ITEM1,s__ListFn_1(V__ROW1)) & s__inList(V__ITEM2,s__ListFn_1(V__ROW1)) & (~ (V__ITEM1 = V__ITEM2))) => s__disjoint(V__ITEM1,V__ITEM2)))) )
|
Merge.kif 3140-3149 | |
| ( ! [V__ROW1,V__ELEMENT] : (s__disjointDecomposition_1(V__ROW1) => (s__inList(V__ELEMENT,s__ListFn_1(V__ROW1)) => s__instance(V__ELEMENT,s__Class))) )
|
Merge.kif 616-620 | |
| ( ! [V__ROW1,V__NUMBER,V__ELEMENT] : ((s__GreatestCommonDivisorFn_1(V__ROW1) = V__NUMBER) => (s__inList(V__ELEMENT,s__ListFn_1(V__ROW1)) => s__instance(V__ELEMENT,s__Number))) )
|
Merge.kif 5003-5008 | |
| ( ! [V__ROW1,V__NUMBER] : ((s__GreatestCommonDivisorFn_1(V__ROW1) = V__NUMBER) => (! [V__ELEMENT] : (s__inList(V__ELEMENT,s__ListFn_1(V__ROW1)) => (s__RemainderFn(V__ELEMENT,V__NUMBER) = 0)))) )
|
Merge.kif 5010-5015 | |
| ( ! [V__ROW1,V__NUMBER] : ((s__GreatestCommonDivisorFn_1(V__ROW1) = V__NUMBER) => (~ (? [V__GREATER] : (s__greaterThan(V__GREATER,V__NUMBER) & (! [V__ELEMENT] : (s__inList(V__ELEMENT,s__ListFn_1(V__ROW1)) => (s__RemainderFn(V__ELEMENT,V__GREATER) = 0))))))) )
|
Merge.kif 5017-5025 | |
| ( ! [V__ROW1,V__NUMBER,V__ELEMENT] : ((s__LeastCommonMultipleFn_1(V__ROW1) = V__NUMBER) => (s__inList(V__ELEMENT,s__ListFn_1(V__ROW1)) => s__instance(V__ELEMENT,s__Number))) )
|
Merge.kif 5082-5087 | |
| ( ! [V__ROW1,V__NUMBER] : ((s__LeastCommonMultipleFn_1(V__ROW1) = V__NUMBER) => (! [V__ELEMENT] : (s__inList(V__ELEMENT,s__ListFn_1(V__ROW1)) => (s__RemainderFn(V__NUMBER,V__ELEMENT) = 0)))) )
|
Merge.kif 5089-5094 | |
| ( ! [V__ROW1,V__NUMBER] : ((s__LeastCommonMultipleFn_1(V__ROW1) = V__NUMBER) => (~ (? [V__LESS] : (s__lessThan(V__LESS,V__NUMBER) & (! [V__ELEMENT] : (s__inList(V__ELEMENT,s__ListFn_1(V__ROW1)) => (s__RemainderFn(V__LESS,V__ELEMENT) = 0))))))) )
|
Merge.kif 5096-5104 | |
| ( ! [V__CLASS,V__ROW1,V__ATTR] : (s__exhaustiveAttribute_2(V__CLASS,V__ROW1) => (s__inList(V__ATTR,s__ListFn_1(V__ROW1)) => s__instance(V__ATTR,s__Attribute))) )
|
Merge.kif 554-558 | |
| ( ! [V__CLASS,V__ROW1] : (s__exhaustiveAttribute_2(V__CLASS,V__ROW1) => (! [V__ATTR1] : (s__instance(V__ATTR1,V__CLASS) => (? [V__ATTR2] : (s__inList(V__ATTR2,s__ListFn_1(V__ROW1)) & (V__ATTR1 = V__ATTR2)))))) )
|
Merge.kif 560-568 | |
| ( ! [V__CLASS,V__ROW1] : (s__exhaustiveDecomposition_2(V__CLASS,V__ROW1) => (! [V__OBJ] : (s__instance(V__OBJ,V__CLASS) => (? [V__ITEM] : (s__inList(V__ITEM,s__ListFn_1(V__ROW1)) & s__instance(V__OBJ,V__ITEM)))))) )
|
Merge.kif 3123-3131 | |
| ( ! [V__ROW1,V__ELEMENT] : (s__exhaustiveDecomposition_1(V__ROW1) => (s__inList(V__ELEMENT,s__ListFn_1(V__ROW1)) => s__instance(V__ELEMENT,s__Class))) )
|
Merge.kif 599-603 | |
| ( ! [V__L] : (s__instance(V__L,s__Album) => (! [V__X] : (s__inList(V__X,V__L) => s__instance(V__X,s__Recording)))) )
|
Music.kif 53-58 | |
| ( ! [V__SVC] : (s__instance(V__SVC,s__ShuttleService) => (? [V__LIST,V__VEHICLE,V__AGENT] : (s__agent(V__SVC,V__AGENT) & s__possesses(V__AGENT,V__VEHICLE) & s__instance(V__VEHICLE,s__Automobile) & s__instance(V__LIST,s__List) & (! [V__X] : (s__inList(V__X,V__LIST) => (s__instance(V__X,s__PostalPlace) & (? [V__TRANSPORT] : (s__instance(V__TRANSPORT,s__Transportation) & s__agent(V__TRANSPORT,V__AGENT) & s__instrument(V__TRANSPORT,V__VEHICLE) & s__destination(V__TRANSPORT,V__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