forall
|
|
Sigma KEE - forall
appearance as argument number 2
|
|
No TPTP formula. May not be expressible in strict first order. |
domainEnglishFormat.kif 65833-65833 |
|
antecedent
|
|
No TPTP formula. May not be expressible in strict first order. |
Merge.kif 17254-17262 |
An entity is an instance of human and for all another entity the other entity doesn't employ the entity holds during a time position if and only if unemployed person is an attribute of the entity holds during the time position |
No TPTP formula. May not be expressible in strict first order. |
Geography.kif 1522-1530 |
|
No TPTP formula. May not be expressible in strict first order. |
Merge.kif 5993-6006 |
|
No TPTP formula. May not be expressible in strict first order. |
Merge.kif 5979-5991 |
|
No TPTP formula. May not be expressible in strict first order. |
UXExperimentalTerms.kif 3202-3215 |
|
No TPTP formula. May not be expressible in strict first order. |
UXExperimentalTerms.kif 2887-2903 |
|
No TPTP formula. May not be expressible in strict first order. |
UXExperimentalTerms.kif 2845-2870 |
|
No TPTP formula. May not be expressible in strict first order. |
UXExperimentalTerms.kif 2922-2940 |
|
No TPTP formula. May not be expressible in strict first order. |
UXExperimentalTerms.kif 1033-1060 |
|
No TPTP formula. May not be expressible in strict first order. |
UXExperimentalTerms.kif 2956-2983 |
|
No TPTP formula. May not be expressible in strict first order. |
UXExperimentalTerms.kif 2999-3026 |
|
No TPTP formula. May not be expressible in strict first order. |
Mid-level-ontology.kif 7351-7365 |
|
No TPTP formula. May not be expressible in strict first order. |
UXExperimentalTerms.kif 4241-4267 |
|
No TPTP formula. May not be expressible in strict first order. |
UXExperimentalTerms.kif 4175-4190 |
|
No TPTP formula. May not be expressible in strict first order. |
UXExperimentalTerms.kif 3333-3356 |
|
No TPTP formula. May not be expressible in strict first order. |
UXExperimentalTerms.kif 3668-3704 |
|
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 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 403-436 |
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 310-342 |
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 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 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 7758-7766 |
An object is larger than another object if and only if for all a real number, another real number and an unit of measure |
No TPTP formula. May not be expressible in strict first order. |
Merge.kif 1297-1302 |
A collection is a proper sub-collection of another collection if and only if for all a physical |
No TPTP formula. May not be expressible in strict first order. |
Hotel.kif 171-176 |
|
No TPTP formula. May not be expressible in strict first order. |
Hotel.kif 233-238 |
|
No TPTP formula. May not be expressible in strict first order. |
Hotel.kif 218-223 |
|
No TPTP formula. May not be expressible in strict first order. |
Mid-level-ontology.kif 4990-4998 |
|
No TPTP formula. May not be expressible in strict first order. |
Merge.kif 17688-17697 |
|
No TPTP formula. May not be expressible in strict first order. |
Government.kif 1132-1152 |
|
No TPTP formula. May not be expressible in strict first order. |
Hotel.kif 147-154 |
|
No TPTP formula. May not be expressible in strict first order. |
Merge.kif 4861-4872 |
|
No TPTP formula. May not be expressible in strict first order. |
Merge.kif 4874-4888 |
|
No TPTP formula. May not be expressible in strict first order. |
Merge.kif 4946-4956 |
|
No TPTP formula. May not be expressible in strict first order. |
Merge.kif 4958-4972 |
|
No TPTP formula. May not be expressible in strict first order. |
Music.kif 936-946 |
|
No TPTP formula. May not be expressible in strict first order. |
Merge.kif 9894-9901 |
|
No TPTP formula. May not be expressible in strict first order. |
UXExperimentalTerms.kif 992-1008 |
|
No TPTP formula. May not be expressible in strict first order. |
Mid-level-ontology.kif 12930-12941 |
|
No TPTP formula. May not be expressible in strict first order. |
Food.kif 1012-1026 |
|
No TPTP formula. May not be expressible in strict first order. |
UXExperimentalTerms.kif 3376-3408 |
|
No TPTP formula. May not be expressible in strict first order. |
UXExperimentalTerms.kif 3428-3455 |
|
No TPTP formula. May not be expressible in strict first order. |
UXExperimentalTerms.kif 3475-3507 |
|
| Display limited to 25 items. Show next 25 |
| Display limited to 25 items. Show next 25 |
statement
|
|
No TPTP formula. May not be expressible in strict first order. |
Government.kif 1241-1248 |
For all ?AGENT, ?VOTER,, , ?ELECTION and ?VOTING contains information exclusive male suffrage |
No TPTP formula. May not be expressible in strict first order. |
Government.kif 923-931 |
For all ?COUNTRY, ?ELECTION,, , ?VOTING and ?VOTER contains information voter citizenship requirement |
No TPTP formula. May not be expressible in strict first order. |
Government.kif 1092-1103 |
For all ?POLITY, ?AGENT,, , ?ELECTION,, , ?VOTINGAGE and ?AGE contains information universal suffrage law |
No TPTP formula. May not be expressible in strict first order. |
Government.kif 1160-1174 |
For all ?POLITY, ?VOTER,, , ?ELECTION,, , ?VOTINGAGE and ?AGE contains information compulsory suffrage law |
No TPTP formula. May not be expressible in strict first order. |
Media.kif 1970-1978 |
There exists a time interval such that the time interval is an instance of time interval and the time interval finishes the time of existence of Jesus of Nazareth and the time interval starts the time of existence of Twelve apostles and for all an entity |
|