ListLengthFn
|
|
Sigma KEE - 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 3030-3033 |
|
No TPTP formula. May not be expressible in strict first order. |
japanese_format.kif 599-601 |
|
No TPTP formula. May not be expressible in strict first order. |
Merge.kif 3027-3027 |
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 3026-3026 |
List length is an instance of total valued relation |
No TPTP formula. May not be expressible in strict first order. |
Merge.kif 3025-3025 |
List length is an instance of unary function |
No TPTP formula. May not be expressible in strict first order. |
Merge.kif 3028-3028 |
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. |
french_format.kif 151-151 |
|
No TPTP formula. May not be expressible in strict first order. |
relations-it.txt 168-168 |
|
No TPTP formula. May not be expressible in strict first order. |
japanese_format.kif 1979-1979 |
|
No TPTP formula. May not be expressible in strict first order. |
portuguese_format.kif 103-103 |
|
No TPTP formula. May not be expressible in strict first order. |
relations-cz.txt 160-160 |
|
No TPTP formula. May not be expressible in strict first order. |
relations-de.txt 341-341 |
|
No TPTP formula. May not be expressible in strict first order. |
relations-hindi.txt 57-57 |
|
No TPTP formula. May not be expressible in strict first order. |
relations-ro.kif 170-170 |
|
No TPTP formula. May not be expressible in strict first order. |
relations-sv.txt 157-157 |
|
No TPTP formula. May not be expressible in strict first order. |
relations-tg.txt 335-335 |
|
No TPTP formula. May not be expressible in strict first order. |
domainEnglishFormat.kif 34702-34702 |
|
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 34701-34701 |
|
No TPTP formula. May not be expressible in strict first order. |
domainEnglishFormat.kif 34700-34700 |
|
No TPTP formula. May not be expressible in strict first order. |
terms-de.txt 109-109 |
|
No TPTP formula. May not be expressible in strict first order. |
relations-tg.txt 336-336 |
|
antecedent
|
|
No TPTP formula. May not be expressible in strict first order. |
Merge.kif 3232-3236 |
|
No TPTP formula. May not be expressible in strict first order. |
Merge.kif 3290-3297 |
|
No TPTP formula. May not be expressible in strict first order. |
Merge.kif 3265-3269 |
|
No TPTP formula. May not be expressible in strict first order. |
Merge.kif 3271-3281 |
|
No TPTP formula. May not be expressible in strict first order. |
Merge.kif 3096-3115 |
|
No TPTP formula. May not be expressible in strict first order. |
Weather.kif 2316-2327 |
|
No TPTP formula. May not be expressible in strict first order. |
Weather.kif 2283-2295 |
|
consequent
|
|
No TPTP formula. May not be expressible in strict first order. |
People.kif 357-390 |
A year is an instance of the year the yearEAR and equal the male life expectancy at birth of a geopolitical area and the year and 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 403-436 |
A year is an instance of the year an integer and equal the female life expectancy at birth of a geopolitical area and the year and 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 310-342 |
A year is an instance of the year an integer and equal the life expectancy at birth of a geopolitical area and the year and 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 272-293 |
A real number is an average of a list if and only if there exist another list and a positive integer such that equal length of the other list and length of the list and equal 1th element of the other list and 1th element of the list and for all another positive integer and equal the positive integer and length of the other list and equal the real number and 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 3290-3297 |
|
No TPTP formula. May not be expressible in strict first order. |
Merge.kif 3271-3281 |
|
No TPTP formula. May not be expressible in strict first order. |
Merge.kif 3096-3115 |
|
No TPTP formula. May not be expressible in strict first order. |
Weather.kif 2305-2314 |
|
No TPTP formula. May not be expressible in strict first order. |
Weather.kif 2283-2295 |
|
No TPTP formula. May not be expressible in strict first order. |
UXExperimentalTerms.kif 3721-3739 |
|
No TPTP formula. May not be expressible in strict first order. |
Merge.kif 3061-3068 |
|
No TPTP formula. May not be expressible in strict first order. |
Merge.kif 3225-3230 |
|
No TPTP formula. May not be expressible in strict first order. |
Weather.kif 3052-3069 |
|
No TPTP formula. May not be expressible in strict first order. |
Weather.kif 3157-3174 |
|
No TPTP formula. May not be expressible in strict first order. |
Weather.kif 3122-3139 |
|
No TPTP formula. May not be expressible in strict first order. |
Weather.kif 3087-3104 |
|
No TPTP formula. May not be expressible in strict first order. |
Weather.kif 2733-2750 |
|
|