| 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 578-581 | |
| No TPTP formula. May not be expressible in strict first order. | japanese_format.kif 82-84 | |
| No TPTP formula. May not be expressible in strict first order. | spanish_format.kif 94-96 | |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 575-575 | The number 1 argument of partition is an instance of class |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 576-576 | The number 2 argument of partition is an instance of class |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 573-573 | partition is an instance of predicate |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 574-574 | 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 316-316 | |
| 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. | japanese_format.kif 1998-1998 | |
| 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. | 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-ro.kif 198-198 | |
| No TPTP formula. May not be expressible in strict first order. | relations-sv.txt 188-188 | |
| 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 543-543 | exhaustive decomposition is internally related to partition |
| No TPTP formula. May not be expressible in strict first order. | chinese_format.kif 312-312 | exhaustive decomposition is internally related to partition |
| No TPTP formula. May not be expressible in strict first order. | domainEnglishFormat.kif 44569-44569 | exhaustive decomposition is internally related to partition |
| No TPTP formula. May not be expressible in strict first order. | domainEnglishFormat.kif 44568-44568 | exhaustive decomposition is internally related to partition |
| No TPTP formula. May not be expressible in strict first order. | terms-de.txt 129-129 | exhaustive decomposition is internally related to partition |
| antecedent |
|
|
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 599-605 |
|
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 595-597 |
|
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 583-587 |
|
| consequent |
|
|
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 589-593 |
|
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 595-597 |
|
| appearance as argument number 0 |
|
|
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 11279-11279 | Ambulating is exhaustively partitioned into walking and running |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 15068-15068 | 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 15067-15067 | 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 14600-14600 | Animal is exhaustively partitioned into vertebrate and invertebrate |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 16988-16988 | Argument is exhaustively partitioned into deductive argument and inductive argument |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 1712-1712 | 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 108-108 | 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 8792-8792 | Care organization is exhaustively partitioned into hospital organization and medical clinic |
| No TPTP formula. May not be expressible in strict first order. | MilitaryProcesses.kif 1027-1027 | Chairman publication is exhaustively partitioned into chairman instruction and chairman manual |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 12658-12658 | Chemical process is exhaustively partitioned into chemical synthesis and chemical decomposition |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 13190-13190 | 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 4028-4028 | Currency is exhaustively partitioned into currency bill and coin |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 17008-17008 | 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 809-809 | Entity is exhaustively partitioned into physical and abstract |
| No TPTP formula. May not be expressible in strict first order. | Mid-level-ontology.kif 14274-14274 | 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 1851-1851 | Firearm is exhaustively partitioned into long gun and hand gun |
| No TPTP formula. May not be expressible in strict first order. | Mid-level-ontology.kif 9319-9319 | Garden is exhaustively partitioned into residential garden and public garden |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 14185-14185 | Geographic area is exhaustively partitioned into water area and land area |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 17964-17964 | 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 5845-5845 | 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 1228-1228 | Gun is exhaustively partitioned into artillery gun and firearm |
| No TPTP formula. May not be expressible in strict first order. | Economy.kif 5620-5620 | Hardwood is exhaustively partitioned into softwood |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 14798-14798 | Human is exhaustively partitioned into man and woman |
| 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