| 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 3417-3418 | |
| No TPTP formula. May not be expressible in strict first order. | japanese_format.kif 635-636 | |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 3413-3413 | Binary function is a subclass of function |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 3415-3415 | Binary function is a subclass of inheritable relation |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 3414-3414 | 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 2410-2410 | Aborted is an instance of binary function |
| No TPTP formula. May not be expressible in strict first order. | MilitaryProcesses.kif 2509-2509 | Aborted launch is an instance of binary function |
| No TPTP formula. May not be expressible in strict first order. | MilitaryProcesses.kif 2430-2430 | Aborted mission is an instance of binary function |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 4735-4735 | Addition is an instance of binary function |
| No TPTP formula. May not be expressible in strict first order. | Music.kif 926-926 | Album copies function is an instance of binary function |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 7623-7623 | Amounts fn is an instance of binary function |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 1784-1784 | Attr is an instance of binary function |
| No TPTP formula. May not be expressible in strict first order. | People.kif 68-68 | Births per thousand is an instance of binary function |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 15123-15123 | Body side fn is an instance of binary function |
| No TPTP formula. May not be expressible in strict first order. | Geography.kif 851-851 | Border is an instance of binary function |
| No TPTP formula. May not be expressible in strict first order. | VirusProteinAndCellPart.kif 1175-1175 | Cell part is an instance of binary function |
| No TPTP formula. May not be expressible in strict first order. | People.kif 440-440 | Children born per woman is an instance of binary function |
| No TPTP formula. May not be expressible in strict first order. | UXExperimentalTerms.kif 3319-3319 | Click_through rate is an instance of binary function |
| No TPTP formula. May not be expressible in strict first order. | Music.kif 1044-1044 | Contest function is an instance of binary function |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 8699-8699 | Day is an instance of binary function |
| No TPTP formula. May not be expressible in strict first order. | People.kif 101-101 | Deaths per thousand is an instance of binary function |
| No TPTP formula. May not be expressible in strict first order. | People.kif 227-227 | Deaths per thousand live births is an instance of binary function |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 6669-6669 | Density is an instance of binary function |
| No TPTP formula. May not be expressible in strict first order. | Mid-level-ontology.kif 19893-19893 | Department is an instance of binary function |
| No TPTP formula. May not be expressible in strict first order. | Mid-level-ontology.kif 19961-19961 | Department of preventing fn is an instance of binary function |
| No TPTP formula. May not be expressible in strict first order. | Geography.kif 646-646 | Directional subregion is an instance of binary function |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 4767-4767 | 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 3736-3736 | 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 3737-3737 | 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 5306-5306 | 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 3420-3422 |
|
|
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