| appearance as argument number 1 |
|
| No TPTP formula. May not be expressible in strict first order. | chinese_format.kif 2158-2161 | |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 4457-4461 | |
| No TPTP formula. May not be expressible in strict first order. | japanese_format.kif 815-819 | |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 4454-4454 | The number 1 argument of names is an instance of symbolic string |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 4455-4455 | The number 2 argument of names is an instance of entity |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 4453-4453 | names is an instance of binary predicate |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 4452-4452 | names is a subrelation of refers |
| appearance as argument number 2 |
|
|
| No TPTP formula. May not be expressible in strict first order. | chinese_format.kif 309-309 | |
| No TPTP formula. May not be expressible in strict first order. | english_format.kif 314-314 | |
| No TPTP formula. May not be expressible in strict first order. | french_format.kif 177-177 | |
| No TPTP formula. May not be expressible in strict first order. | japanese_format.kif 1997-1997 | |
| No TPTP formula. May not be expressible in strict first order. | portuguese_format.kif 129-129 | |
| No TPTP formula. May not be expressible in strict first order. | relations-ro.kif 197-197 | |
| No TPTP formula. May not be expressible in strict first order. | Media.kif 3408-3408 | agent name is a subrelation of names |
| No TPTP formula. May not be expressible in strict first order. | Mid-level-ontology.kif 24855-24855 | alias is a subrelation of names |
| No TPTP formula. May not be expressible in strict first order. | Mid-level-ontology.kif 29118-29118 | conventional long name is a subrelation of names |
| No TPTP formula. May not be expressible in strict first order. | Mid-level-ontology.kif 29129-29129 | conventional short name is a subrelation of names |
| No TPTP formula. May not be expressible in strict first order. | Mid-level-ontology.kif 16098-16098 | family name is a subrelation of names |
| No TPTP formula. May not be expressible in strict first order. | QoSontology.kif 2337-2337 | filename is a subrelation of names |
| No TPTP formula. May not be expressible in strict first order. | Mid-level-ontology.kif 16089-16089 | former name is a subrelation of names |
| No TPTP formula. May not be expressible in strict first order. | Media.kif 3274-3274 | full name is a subrelation of names |
| No TPTP formula. May not be expressible in strict first order. | Mid-level-ontology.kif 16115-16115 | given name is a subrelation of names |
| No TPTP formula. May not be expressible in strict first order. | Mid-level-ontology.kif 16130-16130 | local long name is a subrelation of names |
| No TPTP formula. May not be expressible in strict first order. | Mid-level-ontology.kif 16135-16135 | local short name is a subrelation of names |
| No TPTP formula. May not be expressible in strict first order. | Mid-level-ontology.kif 16111-16111 | middle name is a subrelation of names |
| No TPTP formula. May not be expressible in strict first order. | Media.kif 3321-3321 | name index order is a subrelation of names |
| No TPTP formula. May not be expressible in strict first order. | QoSontology.kif 2227-2227 | password is a subrelation of names |
| No TPTP formula. May not be expressible in strict first order. | Mid-level-ontology.kif 16076-16076 | titles is a subrelation of names |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 4463-4463 | unique identifier is a subrelation of names |
| No TPTP formula. May not be expressible in strict first order. | QoSontology.kif 2189-2189 | user name is a subrelation of names |
| No TPTP formula. May not be expressible in strict first order. | domainEnglishFormat.kif 39682-39682 | user name is a subrelation of names |
| Display limited to 25 items. Show next 25 | ||
| Display limited to 25 items. Show next 25 |
| antecedent |
|
|
| No TPTP formula. May not be expressible in strict first order. | Media.kif 3390-3395 |
|
| No TPTP formula. May not be expressible in strict first order. | Media.kif 3358-3364 |
|
| No TPTP formula. May not be expressible in strict first order. | Media.kif 3323-3328 |
|
| No TPTP formula. May not be expressible in strict first order. | Media.kif 3413-3417 |
|
| No TPTP formula. May not be expressible in strict first order. | Media.kif 3430-3434 |
|
| No TPTP formula. May not be expressible in strict first order. | Media.kif 3464-3468 |
|
| consequent |
|
|
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 13411-13416 |
|
| No TPTP formula. May not be expressible in strict first order. | Mid-level-ontology.kif 26294-26305 |
|
| No TPTP formula. May not be expressible in strict first order. | Mid-level-ontology.kif 26307-26317 |
|
| No TPTP formula. May not be expressible in strict first order. | Mid-level-ontology.kif 26246-26248 |
|
| No TPTP formula. May not be expressible in strict first order. | Medicine.kif 3219-3227 |
|
| No TPTP formula. May not be expressible in strict first order. | Media.kif 31-33 |
|
| statement |
|
|
| No TPTP formula. May not be expressible in strict first order. | Media.kif 2508-2511 | Serbia has &ames$"name" "Republic of Serbia" and a time position is an instance of the day 5 of month the month June holds during after the time position |
| No TPTP formula. May not be expressible in strict first order. | Media.kif 2535-2538 | A time position is an instance of the day 3 of month the month June and Montenegro has &ames$"name" "Montenegro" holds during after the time position |
| appearance as argument number 0 |
|
|
| No TPTP formula. May not be expressible in strict first order. | engineering.kif 962-962 | Autonomous mobile robot has &ames$"name" "AMR" |
| No TPTP formula. May not be expressible in strict first order. | CountriesAndRegions.kif 2497-2497 | Adana turkey has &ames$"name" "Adana" |
| No TPTP formula. May not be expressible in strict first order. | CountriesAndRegions.kif 2499-2499 | Addis ababa ethiopia has &ames$"name" "Addis Ababa" |
| No TPTP formula. May not be expressible in strict first order. | CountriesAndRegions.kif 2501-2501 | Aden yemen has &ames$"name" "Aden" |
| No TPTP formula. May not be expressible in strict first order. | CountriesAndRegions.kif 2503-2503 | Adora west bank has &ames$"name" "Adora" |
| No TPTP formula. May not be expressible in strict first order. | Economy.kif 352-352 | Advanced developing country has &ames$"name" "Advanced Developing Country" |
| No TPTP formula. May not be expressible in strict first order. | CountriesAndRegions.kif 4155-4155 | Afghanistan has &ames$"name" "Afghanistan" |
| No TPTP formula. May not be expressible in strict first order. | Geography.kif 3647-3647 | Africa has &ames$"name" "Africa" |
| No TPTP formula. May not be expressible in strict first order. | CountriesAndRegions.kif 2505-2505 | Afula israel has &ames$"name" "Afula" |
| No TPTP formula. May not be expressible in strict first order. | CountriesAndRegions.kif 2507-2507 | Agri turkey has &ames$"name" "Agri" |
| No TPTP formula. May not be expressible in strict first order. | CountriesAndRegions.kif 2509-2509 | Ain defla algeria has &ames$"name" "Ain Defla" |
| No TPTP formula. May not be expressible in strict first order. | CountriesAndRegions.kif 2511-2511 | Ain el hajar algeria has &ames$"name" "Ain el Hajar" |
| No TPTP formula. May not be expressible in strict first order. | CountriesAndRegions.kif 2513-2513 | Ajaccio france has &ames$"name" "Ajaccio" |
| No TPTP formula. May not be expressible in strict first order. | CountriesAndRegions.kif 2515-2515 | Al balamand lebanon has &ames$"name" "Al_Balamand " |
| No TPTP formula. May not be expressible in strict first order. | CountriesAndRegions.kif 4059-4059 | Albania has &ames$"name" "Albania" |
| No TPTP formula. May not be expressible in strict first order. | CountriesAndRegions.kif 2517-2517 | Alei sinai gaza strip has &ames$"name" "Alei Sinai" |
| No TPTP formula. May not be expressible in strict first order. | CountriesAndRegions.kif 2519-2519 | Alei zahav west bank has &ames$"name" "Alei Zahav" |
| No TPTP formula. May not be expressible in strict first order. | CountriesAndRegions.kif 2521-2521 | Aley lebanon has &ames$"name" "Aley" |
| No TPTP formula. May not be expressible in strict first order. | CountriesAndRegions.kif 3941-3941 | Algeria has &ames$"name" "Algeria" |
| No TPTP formula. May not be expressible in strict first order. | CountriesAndRegions.kif 2523-2523 | Algiers algeria has &ames$"name" "Algiers" |
| No TPTP formula. May not be expressible in strict first order. | CountriesAndRegions.kif 2525-2525 | Alkhan yurt russia has &ames$"name" "Alkhan_Yurt" |
| No TPTP formula. May not be expressible in strict first order. | CountriesAndRegions.kif 2527-2527 | Alon moreh west bank has &ames$"name" "Alon Moreh" |
| No TPTP formula. May not be expressible in strict first order. | CountriesAndRegions.kif 2529-2529 | Ambon indonesia has &ames$"name" "Ambon" |
| No TPTP formula. May not be expressible in strict first order. | Sports.kif 825-825 | Foot ball US has &ames$"name" "American Football" |
| No TPTP formula. May not be expressible in strict first order. | CountriesAndRegions.kif 4189-4189 | American samoa has &ames$"name" "American Samoa" |
| 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 3.0 is open source software produced by Articulate Software and its partners