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

Formal Language: 



KB Term:  Term intersection
English Word: 

  =>

Sigma KEE - =>
=>

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


No TPTP formula. May not be expressible in strict first order. Merge.kif 5405-5409
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 7350-7364
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 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 7780-7788 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 4989-4997
No TPTP formula. May not be expressible in strict first order. Merge.kif 17710-17719
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. Media.kif 2137-2150
No TPTP formula. May not be expressible in strict first order. Merge.kif 9916-9923
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. Geography.kif 7142-7162
No TPTP formula. May not be expressible in strict first order. Mid-level-ontology.kif 12929-12940
No TPTP formula. May not be expressible in strict first order. Merge.kif 10244-10259
No TPTP formula. May not be expressible in strict first order. Food.kif 1012-1026

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

appearance as argument number 0
-------------------------


No TPTP formula. May not be expressible in strict first order. Merge.kif 5421-5425
No TPTP formula. May not be expressible in strict first order. Merge.kif 5405-5409
No TPTP formula. May not be expressible in strict first order. Hotel.kif 2768-2770
No TPTP formula. May not be expressible in strict first order. UXExperimentalTerms.kif 632-640
No TPTP formula. May not be expressible in strict first order. Mid-level-ontology.kif 20751-20757
No TPTP formula. May not be expressible in strict first order. Hotel.kif 599-604
No TPTP formula. May not be expressible in strict first order. Hotel.kif 939-944
No TPTP formula. May not be expressible in strict first order. UXExperimentalTerms.kif 193-199
No TPTP formula. May not be expressible in strict first order. Government.kif 706-713
No TPTP formula. May not be expressible in strict first order. Mid-level-ontology.kif 14071-14076
No TPTP formula. May not be expressible in strict first order. Mid-level-ontology.kif 14099-14105
No TPTP formula. May not be expressible in strict first order. Mid-level-ontology.kif 14090-14097
No TPTP formula. May not be expressible in strict first order. Mid-level-ontology.kif 14054-14057
No TPTP formula. May not be expressible in strict first order. Government.kif 738-753
No TPTP formula. May not be expressible in strict first order. Music.kif 280-287
No TPTP formula. May not be expressible in strict first order. Music.kif 312-314
No TPTP formula. May not be expressible in strict first order. Music.kif 261-270
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 16851-16860
No TPTP formula. May not be expressible in strict first order. Merge.kif 7740-7745
No TPTP formula. May not be expressible in strict first order. Merge.kif 7736-7738
No TPTP formula. May not be expressible in strict first order. Merge.kif 7717-7719
No TPTP formula. May not be expressible in strict first order. Mid-level-ontology.kif 23251-23257

Display limited to 25 items. Show next 25

Display limited to 25 items. Show next 25


Show simplified definition (without tree view)
Show simplified definition (with tree view)

Show without tree


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