| appearance as argument number 1 |
|
| No TPTP formula. May not be expressible in strict first order. | chinese_format.kif 2825-2827 | |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 9569-9572 | |
| No TPTP formula. May not be expressible in strict first order. | japanese_format.kif 1567-1569 | |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 9565-9565 | Le nombre 1 argument de connects est une instance de objet |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 9566-9566 | Le nombre 2 argument de connects est une instance de objet |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 9567-9567 | Le nombre 3 argument de connects est une instance de objet |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 9563-9563 | connects est une instance de relation spatial |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 9564-9564 | connects est une instance de pr�dicat ternaire |
| appearance as argument number 2 |
|
|
| No TPTP formula. May not be expressible in strict first order. | chinese_format.kif 363-363 | |
| No TPTP formula. May not be expressible in strict first order. | english_format.kif 366-366 | |
| No TPTP formula. May not be expressible in strict first order. | french_format.kif 210-210 | |
| No TPTP formula. May not be expressible in strict first order. | relations-it.txt 54-54 | |
| No TPTP formula. May not be expressible in strict first order. | japanese_format.kif 2017-2017 | |
| No TPTP formula. May not be expressible in strict first order. | portuguese_format.kif 162-162 | |
| No TPTP formula. May not be expressible in strict first order. | relations-cb.txt 88-88 | |
| No TPTP formula. May not be expressible in strict first order. | relations-cz.txt 217-217 | |
| No TPTP formula. May not be expressible in strict first order. | relations-de.txt 483-483 | |
| No TPTP formula. May not be expressible in strict first order. | relations-hindi.txt 95-95 | |
| No TPTP formula. May not be expressible in strict first order. | relations-ro.kif 230-230 | |
| No TPTP formula. May not be expressible in strict first order. | relations-sv.txt 227-227 | |
| No TPTP formula. May not be expressible in strict first order. | relations-tg.txt 124-124 | |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 16228-16228 | connectsEngineeringComponents est une sous-relation de connects |
| No TPTP formula. May not be expressible in strict first order. | chinese_format.kif 364-364 | |
| No TPTP formula. May not be expressible in strict first order. | domainEnglishFormat.kif 16661-16661 | |
| No TPTP formula. May not be expressible in strict first order. | domainEnglishFormat.kif 16660-16660 | |
| No TPTP formula. May not be expressible in strict first order. | relations-tg.txt 125-125 |
| antecedent |
|
|
| No TPTP formula. May not be expressible in strict first order. | Transportation.kif 2903-2909 | |
| No TPTP formula. May not be expressible in strict first order. | Geography.kif 5305-5310 | |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 9598-9600 | |
| No TPTP formula. May not be expressible in strict first order. | Geography.kif 5288-5290 | |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 9582-9588 | |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 9574-9576 |
| consequent |
|
|
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 9590-9596 | |
| No TPTP formula. May not be expressible in strict first order. | Mid-level-ontology.kif 15124-15134 | |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 12381-12387 | |
| No TPTP formula. May not be expressible in strict first order. | Mid-level-ontology.kif 5624-5633 | |
| No TPTP formula. May not be expressible in strict first order. | Mid-level-ontology.kif 15100-15112 |
|
| No TPTP formula. May not be expressible in strict first order. | Medicine.kif 5132-5145 | |
| No TPTP formula. May not be expressible in strict first order. | Geography.kif 5380-5395 |
|
| No TPTP formula. May not be expressible in strict first order. | Anatomy.kif 1745-1756 | |
| No TPTP formula. May not be expressible in strict first order. | Anatomy.kif 1695-1706 | |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 9578-9580 | |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 9598-9600 | |
| No TPTP formula. May not be expressible in strict first order. | Mid-level-ontology.kif 11205-11211 | |
| No TPTP formula. May not be expressible in strict first order. | Mid-level-ontology.kif 15078-15084 | |
| No TPTP formula. May not be expressible in strict first order. | Geography.kif 5599-5605 | |
| No TPTP formula. May not be expressible in strict first order. | Geography.kif 5322-5328 | |
| No TPTP formula. May not be expressible in strict first order. | Geography.kif 5498-5505 | |
| No TPTP formula. May not be expressible in strict first order. | Geography.kif 5489-5496 | |
| No TPTP formula. May not be expressible in strict first order. | Mid-level-ontology.kif 15303-15311 | |
| No TPTP formula. May not be expressible in strict first order. | Mid-level-ontology.kif 11734-11742 |
|
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 15136-15142 |
|
| No TPTP formula. May not be expressible in strict first order. | Mid-level-ontology.kif 11354-11360 | |
| No TPTP formula. May not be expressible in strict first order. | Geography.kif 4783-4789 | |
| No TPTP formula. May not be expressible in strict first order. | Mid-level-ontology.kif 9476-9482 | |
| No TPTP formula. May not be expressible in strict first order. | Mid-level-ontology.kif 3630-3641 | |
| No TPTP formula. May not be expressible in strict first order. | Sports.kif 1247-1264 |
|
| 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