| appearance as argument number 1 |
|
| No TPTP formula. May not be expressible in strict first order. | chinese_format.kif 2709-2710 | |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 8164-8165 | |
| No TPTP formula. May not be expressible in strict first order. | japanese_format.kif 1432-1434 | |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 8161-8161 | 之前或同时 的 1 数量 是 时点 的 instance |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 8162-8162 | 之前或同时 的 2 数量 是 时点 的 instance |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 8158-8158 | 之前或同时 是 二元谓语 的 instance |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 8160-8160 | 之前或同时 是 偏序关系 的 instance |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 8159-8159 | 之前或同时 是 时间关系 的 instance |
| appearance as argument number 2 |
|
|
| No TPTP formula. May not be expressible in strict first order. | chinese_format.kif 425-425 | |
| No TPTP formula. May not be expressible in strict first order. | english_format.kif 431-431 | |
| No TPTP formula. May not be expressible in strict first order. | french_format.kif 247-247 | |
| No TPTP formula. May not be expressible in strict first order. | relations-it.txt 33-33 | |
| No TPTP formula. May not be expressible in strict first order. | japanese_format.kif 2041-2041 | |
| No TPTP formula. May not be expressible in strict first order. | portuguese_format.kif 199-199 | |
| No TPTP formula. May not be expressible in strict first order. | relations-cz.txt 252-252 | |
| No TPTP formula. May not be expressible in strict first order. | relations-de.txt 553-553 | |
| No TPTP formula. May not be expressible in strict first order. | relations-hindi.txt 77-77 | |
| No TPTP formula. May not be expressible in strict first order. | relations-ro.kif 268-268 | |
| No TPTP formula. May not be expressible in strict first order. | relations-sv.txt 269-269 | |
| No TPTP formula. May not be expressible in strict first order. | relations-cb.txt 67-67 | |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 8121-8121 | 之前 是 之前或同时 的 subrelation |
| No TPTP formula. May not be expressible in strict first order. | chinese_format.kif 426-426 | |
| No TPTP formula. May not be expressible in strict first order. | domainEnglishFormat.kif 10547-10547 | |
| No TPTP formula. May not be expressible in strict first order. | domainEnglishFormat.kif 10546-10546 | |
| No TPTP formula. May not be expressible in strict first order. | domainEnglishFormat.kif 10545-10545 | |
| No TPTP formula. May not be expressible in strict first order. | relations-tg.txt 83-83 |
| antecedent |
|
|
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 8222-8226 | |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 8291-8301 | |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 8167-8171 |
| consequent |
|
|
| No TPTP formula. May not be expressible in strict first order. | FinancialOntology.kif 655-667 | |
| No TPTP formula. May not be expressible in strict first order. | Mid-level-ontology.kif 30680-30686 | |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 3836-3843 | |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 8132-8144 | |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 8173-8177 | |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 8216-8220 |
|
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