| appearance as argument number 1 |
|
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 628-629 | |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 624-627 | |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 622-622 | The number 1 argument of partition is an instance of class |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 623-623 | The number 2 argument of partition is an instance of class |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 620-620 | partition is an instance of predicate |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 621-621 | 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 188-188 | |
| No TPTP formula. May not be expressible in strict first order. | french_format.kif 178-178 | |
| No TPTP formula. May not be expressible in strict first order. | relations-it.txt 213-213 | |
| No TPTP formula. May not be expressible in strict first order. | portuguese_format.kif 130-130 | |
| No TPTP formula. May not be expressible in strict first order. | arabic_format.kif 123-123 | |
| No TPTP formula. May not be expressible in strict first order. | relations-cz.txt 187-187 | |
| No TPTP formula. May not be expressible in strict first order. | relations-de.txt 408-408 | |
| No TPTP formula. May not be expressible in strict first order. | relations-hindi.txt 251-251 | |
| No TPTP formula. May not be expressible in strict first order. | relations-tg.txt 405-405 | |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 586-586 | exhaustive decomposition is internally related to partition |
| No TPTP formula. May not be expressible in strict first order. | chinese_format.kif 312-312 | "划分" is the printable form of partition in ChineseLanguage |
| No TPTP formula. May not be expressible in strict first order. | domainEnglishFormat.kif 7849-7849 | "partition" is the printable form of partition in english language |
| No TPTP formula. May not be expressible in strict first order. | arabic_format.kif 573-573 | "«بِالكَامِل مُجَزَّأ إلى»" is the printable form of partition in ar |
| antecedent |
|
|
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 631-635 | @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 10973-10973 | Ambulating is exhaustively partitioned into walking and running |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 14921-14921 | 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 14920-14920 | 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 14368-14368 | Animal is exhaustively partitioned into vertebrate and invertebrate |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 16967-16967 | Argument is exhaustively partitioned into deductive argument and inductive argument |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 1734-1734 | 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 7327-7327 | Care organization is exhaustively partitioned into hospital organization and medical clinic |
| No TPTP formula. May not be expressible in strict first order. | MilitaryProcesses.kif 1015-1015 | Chairman publication is exhaustively partitioned into chairman instruction and chairman manual |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 12275-12275 | Chemical process is exhaustively partitioned into chemical synthesis and chemical decomposition |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 12835-12835 | 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 4116-4116 | Currency is exhaustively partitioned into currency bill and currency coin |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 16989-16989 | 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 840-840 | Entity is exhaustively partitioned into physical and abstract |
| No TPTP formula. May not be expressible in strict first order. | Mid-level-ontology.kif 10535-10535 | 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 2013-2013 | Firearm is exhaustively partitioned into rifle and pistol |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 13892-13892 | Geographic area is exhaustively partitioned into water area and land area |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 18096-18096 | 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 5890-5890 | 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 1551-1551 | Gun is exhaustively partitioned into artillery gun and firearm |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 14603-14603 | Human is exhaustively partitioned into man and woman |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 1464-1464 | Human language is exhaustively partitioned into natural language and constructed language |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 1465-1465 | 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 2.99c (>= 2017/11/20) is open source software produced by Articulate Software and its partners