| appearance as argument number 1 |
|
| No TPTP formula. May not be expressible in strict first order. | chinese_format.kif 2353-2355 | |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 5925-5928 | |
| No TPTP formula. May not be expressible in strict first order. | japanese_format.kif 1030-1032 | |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 5922-5922 | The number 1 argument of path length is an instance of graph path |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 5923-5923 | The number 2 argument of path length is an instance of positive integer |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 5921-5921 | path length is an instance of binary predicate |
| appearance as argument number 2 |
|
|
| No TPTP formula. May not be expressible in strict first order. | chinese_format.kif 753-753 | |
| No TPTP formula. May not be expressible in strict first order. | english_format.kif 755-755 | |
| No TPTP formula. May not be expressible in strict first order. | french_format.kif 454-454 | |
| No TPTP formula. May not be expressible in strict first order. | relations-it.txt 217-217 | |
| No TPTP formula. May not be expressible in strict first order. | japanese_format.kif 2162-2162 | |
| No TPTP formula. May not be expressible in strict first order. | portuguese_format.kif 406-406 | |
| No TPTP formula. May not be expressible in strict first order. | relations-cz.txt 467-467 | |
| No TPTP formula. May not be expressible in strict first order. | relations-de.txt 972-972 | |
| No TPTP formula. May not be expressible in strict first order. | relations-hindi.txt 255-255 | |
| No TPTP formula. May not be expressible in strict first order. | relations-ro.kif 476-476 | |
| No TPTP formula. May not be expressible in strict first order. | relations-sv.txt 519-519 | |
| No TPTP formula. May not be expressible in strict first order. | relations-tg.txt 409-409 | |
| No TPTP formula. May not be expressible in strict first order. | chinese_format.kif 754-754 | |
| No TPTP formula. May not be expressible in strict first order. | domainEnglishFormat.kif 44785-44785 | |
| No TPTP formula. May not be expressible in strict first order. | domainEnglishFormat.kif 44784-44784 | |
| No TPTP formula. May not be expressible in strict first order. | terms-de.txt 298-298 |
| consequent |
|
|
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 6101-6107 |
|
| statement |
|
|
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 6109-6116 | There don't exist a graph path and another graph path such that the graph path is an instance of the set of paths that partition a graph into two separate graphs and the other graph path is an instance of the set of minimal paths that partition the graph into two separate graphs and the length of the graph path is a positive integer and the length of the other graph path is another positive integer and the positive integer is less than the other positive integer |
|
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