| appearance as argument number 1 |
|
| No TPTP formula. May not be expressible in strict first order. | chinese_format.kif 1502-1503 | |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 414-416 | |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 411-411 | The number 1 argument of disjoint relation is an instance of relation |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 412-412 | The number 2 argument of disjoint relation is an instance of relation |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 408-408 | disjoint relation is an instance of binary predicate |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 409-409 | disjoint relation is an instance of irreflexive relation |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 410-410 | disjoint relation is an instance of partial valued relation |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 413-413 | disjoint relation is internally related to disjoint |
| appearance as argument number 2 |
|
|
| No TPTP formula. May not be expressible in strict first order. | chinese_format.kif 289-289 | |
| No TPTP formula. May not be expressible in strict first order. | english_format.kif 297-297 | |
| No TPTP formula. May not be expressible in strict first order. | chinese_format.kif 290-290 | |
| No TPTP formula. May not be expressible in strict first order. | domainEnglishFormat.kif 19851-19851 | |
| No TPTP formula. May not be expressible in strict first order. | domainEnglishFormat.kif 19850-19850 | |
| No TPTP formula. May not be expressible in strict first order. | domainEnglishFormat.kif 19849-19849 |
| antecedent |
|
|
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 446-452 |
|
| consequent |
|
|
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 418-423 |
|
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 425-430 |
|
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 432-437 |
|
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 439-444 |
|
| appearance as argument number 0 |
|
|
| No TPTP formula. May not be expressible in strict first order. | Mid-level-ontology.kif 20471-20471 | ancestor organization and sub organization are disjoint |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 945-945 | contains and part are disjoint |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 4060-4060 | crosses and connected are disjoint |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 2505-2505 | decreases likelihood and independent probability are disjoint |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 3882-3882 | deprives norm and confers norm are disjoint |
| No TPTP formula. May not be expressible in strict first order. | Mid-level-ontology.kif 6464-6464 | disapproves and desires are disjoint |
| No TPTP formula. May not be expressible in strict first order. | Mid-level-ontology.kif 6448-6448 | dislikes and wants are disjoint |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 2503-2503 | increases likelihood and decreases likelihood are disjoint |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 2504-2504 | increases likelihood and independent probability are disjoint |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 1642-1642 | manner and attribute are disjoint |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 9030-9030 | meets spatially and overlaps spatially are disjoint |
| No TPTP formula. May not be expressible in strict first order. | Mid-level-ontology.kif 19795-19795 | mutual stranger and mutual acquaintance are disjoint |
| No TPTP formula. May not be expressible in strict first order. | ComputingBrands.kif 1648-1648 | referee and plays are disjoint |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 2419-2419 | resource and instrument are disjoint |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 2418-2418 | resource and result are disjoint |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 2420-2420 | result and instrument are disjoint |
| No TPTP formula. May not be expressible in strict first order. | Mid-level-ontology.kif 19810-19810 | spouse and domestic partner are disjoint |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 13393-13393 | stays and home are disjoint |
| No TPTP formula. May not be expressible in strict first order. | Mid-level-ontology.kif 19780-19780 | stranger and acquaintance are disjoint |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 655-655 | sub attribute and successor attribute are disjoint |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 621-621 | subsumed external concept and subsuming external concept are disjoint |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 619-619 | synonymous external concept and subsumed external concept are disjoint |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 620-620 | synonymous external concept and subsuming external concept are disjoint |
|
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