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

Formal Language: 



KB Term:  Term intersection
English Word: 

Sigma KEE - ListLengthFn
ListLengthFn

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


No TPTP formula. May not be expressible in strict first order. chinese_format.kif 1967-1969
No TPTP formula. May not be expressible in strict first order. Merge.kif 2976-2979
No TPTP formula. May not be expressible in strict first order. Merge.kif 2973-2973 The number 1 argument of list length is an instance of list
No TPTP formula. May not be expressible in strict first order. Merge.kif 2972-2972 List length is an instance of total valued relation
No TPTP formula. May not be expressible in strict first order. Merge.kif 2971-2971 List length is an instance of unary function
No TPTP formula. May not be expressible in strict first order. Merge.kif 2974-2974 The range of list length is an instance of nonnegative integer

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


No TPTP formula. May not be expressible in strict first order. chinese_format.kif 265-265
No TPTP formula. May not be expressible in strict first order. english_format.kif 270-270
No TPTP formula. May not be expressible in strict first order. domainEnglishFormat.kif 34673-34673
No TPTP formula. May not be expressible in strict first order. chinese_format.kif 266-266
No TPTP formula. May not be expressible in strict first order. domainEnglishFormat.kif 34672-34672
No TPTP formula. May not be expressible in strict first order. domainEnglishFormat.kif 34671-34671

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


No TPTP formula. May not be expressible in strict first order. Merge.kif 3178-3182
No TPTP formula. May not be expressible in strict first order. Merge.kif 3236-3243
No TPTP formula. May not be expressible in strict first order. Merge.kif 3211-3215
No TPTP formula. May not be expressible in strict first order. Merge.kif 3217-3227
No TPTP formula. May not be expressible in strict first order. Merge.kif 3042-3061
No TPTP formula. May not be expressible in strict first order. Weather.kif 1486-1497
No TPTP formula. May not be expressible in strict first order. Weather.kif 1453-1465

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


No TPTP formula. May not be expressible in strict first order. People.kif 383-416 A year is an instance of the year the yearEAR and the male life expectancy at birth of a geopolitical area and the year is equal to a real number if and only if there exist a list, another integer,, , a symbolic string,, , an entity,, , another entity and a third entity such that the list is an instance of list and length of the list is an instance of the other integer and for all the listITEM and the real number is an average of the list
No TPTP formula. May not be expressible in strict first order. People.kif 429-462 A year is an instance of the year an integer and the female life expectancy at birth of a geopolitical area and the year is equal to a real number if and only if there exist a list, another integer,, , a symbolic string,, , an entity,, , another entity and a third entity such that the list is an instance of list and length of the list is an instance of the other integer and for all the listITEM and the real number is an average of the list
No TPTP formula. May not be expressible in strict first order. People.kif 336-368 A year is an instance of the year an integer and the life expectancy at birth of a geopolitical area and the year is equal to a real number if and only if there exist a list, another integer,, , a symbolic string,, , an entity,, , another entity and a third entity such that the list is an instance of list and length of the list is an instance of the other integer and for all the listITEM and the real number is an average of the list
No TPTP formula. May not be expressible in strict first order. People.kif 298-319 A real number is an average of a list if and only if there exist another list and a positive integer 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 another positive integer and the positive integer is equal to length of the other list and the real number is equal to the positive integerth element of the other list and the positive integer
No TPTP formula. May not be expressible in strict first order. Merge.kif 3236-3243
No TPTP formula. May not be expressible in strict first order. Merge.kif 3217-3227
No TPTP formula. May not be expressible in strict first order. Merge.kif 3042-3061
No TPTP formula. May not be expressible in strict first order. Weather.kif 1475-1484
No TPTP formula. May not be expressible in strict first order. Weather.kif 1453-1465
No TPTP formula. May not be expressible in strict first order. UXExperimentalTerms.kif 3927-3945
No TPTP formula. May not be expressible in strict first order. Merge.kif 3007-3014
No TPTP formula. May not be expressible in strict first order. Merge.kif 3171-3176
No TPTP formula. May not be expressible in strict first order. Weather.kif 2223-2240
No TPTP formula. May not be expressible in strict first order. Weather.kif 2328-2345
No TPTP formula. May not be expressible in strict first order. Weather.kif 2293-2310
No TPTP formula. May not be expressible in strict first order. Weather.kif 2258-2275
No TPTP formula. May not be expressible in strict first order. Weather.kif 1904-1921

statement
-------------------------


No TPTP formula. May not be expressible in strict first order. Merge.kif 2996-2999 For all @ROW and another entity length of (@ROW and the other entity) is equal to (length of (@ROW)+1)
No TPTP formula. May not be expressible in strict first order. Merge.kif 3001-3005 For all @ROW and another entity length of (@ROW and the other entity)th element of (@ROW and the other entity) is equal to the other entity


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 is open source software produced by Articulate Software and its partners