| appearance as argument number 1 |
|
| No TPTP formula. May not be expressible in strict first order. | chinese_format.kif 1999-1999 | |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 3336-3337 | |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 3332-3332 | Binary function is a subclass of function |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 3334-3334 | Binary function is a subclass of inheritable relation |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 3333-3333 | Binary function is a subclass of ternary relation |
| appearance as argument number 2 |
|
|
| No TPTP formula. May not be expressible in strict first order. | domainEnglishFormat.kif 280-280 | |
| No TPTP formula. May not be expressible in strict first order. | domainEnglishFormat.kif 279-279 | |
| No TPTP formula. May not be expressible in strict first order. | domainEnglishFormat.kif 278-278 | |
| No TPTP formula. May not be expressible in strict first order. | MilitaryProcesses.kif 2409-2409 | Aborted is an instance of binary function |
| No TPTP formula. May not be expressible in strict first order. | MilitaryProcesses.kif 2475-2475 | Aborted launch is an instance of binary function |
| No TPTP formula. May not be expressible in strict first order. | MilitaryProcesses.kif 2429-2429 | Aborted mission is an instance of binary function |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 4617-4617 | Addition is an instance of binary function |
| No TPTP formula. May not be expressible in strict first order. | Music.kif 921-921 | Album copies function is an instance of binary function |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 7483-7483 | AmountsFn is an instance of binary function |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 1720-1720 | Attr is an instance of binary function |
| No TPTP formula. May not be expressible in strict first order. | People.kif 94-94 | Births per thousand is an instance of binary function |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 14706-14706 | BodySideFn is an instance of binary function |
| No TPTP formula. May not be expressible in strict first order. | Geography.kif 693-693 | Border is an instance of binary function |
| No TPTP formula. May not be expressible in strict first order. | VirusProteinAndCellPart.kif 654-654 | Cell part is an instance of binary function |
| No TPTP formula. May not be expressible in strict first order. | People.kif 453-453 | Children born per woman is an instance of binary function |
| No TPTP formula. May not be expressible in strict first order. | UXExperimentalTerms.kif 3527-3527 | Click-through rate is an instance of binary function |
| No TPTP formula. May not be expressible in strict first order. | Music.kif 1035-1035 | Contest function is an instance of binary function |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 8494-8494 | Day is an instance of binary function |
| No TPTP formula. May not be expressible in strict first order. | People.kif 125-125 | Deaths per thousand is an instance of binary function |
| No TPTP formula. May not be expressible in strict first order. | People.kif 246-246 | Deaths per thousand live births is an instance of binary function |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 6554-6554 | Density is an instance of binary function |
| No TPTP formula. May not be expressible in strict first order. | Mid-level-ontology.kif 17732-17732 | Department is an instance of binary function |
| No TPTP formula. May not be expressible in strict first order. | Mid-level-ontology.kif 17769-17769 | DepartmentOfPreventingFn is an instance of binary function |
| No TPTP formula. May not be expressible in strict first order. | Geography.kif 476-476 | Directional subregion is an instance of binary function |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 4649-4649 | Division is an instance of binary function |
| Display limited to 25 items. Show next 25 | ||
| Display limited to 25 items. Show next 25 |
| appearance as argument number 3 |
|
|
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 3655-3655 | The number 1 argument of distributes is an instance of binary function |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 3656-3656 | The number 2 argument of distributes is an instance of binary function |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 5184-5184 | The number 1 argument of identity element is an instance of binary function |
| antecedent |
|
|
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 3339-3341 |
|
|
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