| appearance as argument number 1 |
|
| No TPTP formula. May not be expressible in strict first order. | chinese_format.kif 1517-1518 | |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 585-588 | |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 582-582 | The number 1 argument of partition is an instance of class |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 583-583 | The number 2 argument of partition is an instance of class |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 580-580 | partition is an instance of predicate |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 581-581 | partition is an instance of variable arity relation |
| appearance as argument number 2 |
|
|
| No TPTP formula. May not be expressible in strict first order. | chinese_format.kif 311-311 | |
| No TPTP formula. May not be expressible in strict first order. | english_format.kif 319-319 | |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 550-550 | exhaustive decomposition is internally related to partition |
| No TPTP formula. May not be expressible in strict first order. | chinese_format.kif 312-312 | |
| No TPTP formula. May not be expressible in strict first order. | domainEnglishFormat.kif 44556-44556 | |
| No TPTP formula. May not be expressible in strict first order. | domainEnglishFormat.kif 44555-44555 |
| antecedent |
|
|
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 590-594 | @ROW is exhaustively partitioned into @ROW if and only if @ROW is covered by @ROW and @ROW is disjointly decomposed into @ROW |
| appearance as argument number 0 |
|
|
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 10447-10447 | Ambulating is exhaustively partitioned into walking and running |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 13903-13903 | Anatomical structure is exhaustively partitioned into animal anatomical structure and plant anatomical structure |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 13902-13902 | Anatomical structure is exhaustively partitioned into body part and abnormal anatomical structure |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 13447-13447 | Animal is exhaustively partitioned into vertebrate and invertebrate |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 15683-15683 | Argument is exhaustively partitioned into deductive argument and inductive argument |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 1610-1610 | Attribute is exhaustively partitioned into internal attribute and relational attribute |
| No TPTP formula. May not be expressible in strict first order. | WMD.kif 82-82 | Biochemical agent is exhaustively partitioned into biological agent and chemical agent |
| No TPTP formula. May not be expressible in strict first order. | WMD.kif 107-107 | Biochemical weapon is exhaustively partitioned into biological weapon and chemical weapon |
| No TPTP formula. May not be expressible in strict first order. | WMD.kif 157-157 | Biological agent is exhaustively partitioned into toxin and toxic organism |
| No TPTP formula. May not be expressible in strict first order. | Mid-level-ontology.kif 7314-7314 | Care organization is exhaustively partitioned into hospital organization and medical clinic |
| No TPTP formula. May not be expressible in strict first order. | MilitaryProcesses.kif 1026-1026 | Chairman publication is exhaustively partitioned into chairman instruction and chairman manual |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 11623-11623 | Chemical process is exhaustively partitioned into chemical synthesis and chemical decomposition |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 12121-12121 | Communication is exhaustively partitioned into stating, supposing, directing, committing, expressing, and declaring |
| No TPTP formula. May not be expressible in strict first order. | Mid-level-ontology.kif 4122-4122 | Currency is exhaustively partitioned into currency bill and currency coin |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 15703-15703 | Deductive argument is exhaustively partitioned into valid deductive argument and invalid deductive argument |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 781-781 | Entity is exhaustively partitioned into physical and abstract |
| No TPTP formula. May not be expressible in strict first order. | Mid-level-ontology.kif 10580-10580 | Expressing is exhaustively partitioned into gesture and expressing in language |
| No TPTP formula. May not be expressible in strict first order. | Mid-level-ontology.kif 2014-2014 | Firearm is exhaustively partitioned into rifle and pistol |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 13046-13046 | Geographic area is exhaustively partitioned into water area and land area |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 16609-16609 | Geometric figure is exhaustively partitioned into geometric point, one dimensional figure, two dimensional figure, and three dimensional figure |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 5519-5519 | Graph element is exhaustively partitioned into graph node and graph arc |
| No TPTP formula. May not be expressible in strict first order. | Mid-level-ontology.kif 1552-1552 | Gun is exhaustively partitioned into artillery gun and firearm |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 13636-13636 | Human is exhaustively partitioned into man and woman |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 1331-1331 | Human language is exhaustively partitioned into natural language and constructed language |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 1332-1332 | Human language is exhaustively partitioned into spoken human language and manual human language |
| 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