| appearance as argument number 1 |
|
| No TPTP formula. May not be expressible in strict first order. | chinese_format.kif 1964-1966 | |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 2981-2984 | |
| No TPTP formula. May not be expressible in strict first order. | japanese_format.kif 596-598 | |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 2977-2977 | 找出表列顺序的函数 的 1 数量 是 串列 的 instance |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 2978-2978 | 找出表列顺序的函数 的 2 数量 是 正整数 的 instance |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 2975-2975 | 找出表列顺序的函数 是 二元函数 的 instance |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 2976-2976 | 找出表列顺序的函数 是 部分值关系 的 instance |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 2979-2979 | 找出表列顺序的函数 的 range 是 实体 的实例 |
| appearance as argument number 2 |
|
|
| No TPTP formula. May not be expressible in strict first order. | chinese_format.kif 263-263 | |
| No TPTP formula. May not be expressible in strict first order. | english_format.kif 268-268 | |
| No TPTP formula. May not be expressible in strict first order. | french_format.kif 150-150 | |
| No TPTP formula. May not be expressible in strict first order. | relations-it.txt 169-169 | |
| No TPTP formula. May not be expressible in strict first order. | japanese_format.kif 1978-1978 | |
| No TPTP formula. May not be expressible in strict first order. | portuguese_format.kif 102-102 | |
| No TPTP formula. May not be expressible in strict first order. | relations-cz.txt 159-159 | |
| No TPTP formula. May not be expressible in strict first order. | relations-de.txt 338-338 | |
| No TPTP formula. May not be expressible in strict first order. | relations-hindi.txt 207-207 | |
| No TPTP formula. May not be expressible in strict first order. | relations-ro.kif 169-169 | |
| No TPTP formula. May not be expressible in strict first order. | relations-sv.txt 156-156 | |
| No TPTP formula. May not be expressible in strict first order. | relations-tg.txt 337-337 | |
| No TPTP formula. May not be expressible in strict first order. | chinese_format.kif 264-264 | |
| No TPTP formula. May not be expressible in strict first order. | domainEnglishFormat.kif 34697-34697 | |
| No TPTP formula. May not be expressible in strict first order. | domainEnglishFormat.kif 34696-34696 | |
| No TPTP formula. May not be expressible in strict first order. | domainEnglishFormat.kif 34695-34695 | |
| No TPTP formula. May not be expressible in strict first order. | terms-de.txt 108-108 | |
| No TPTP formula. May not be expressible in strict first order. | relations-tg.txt 338-338 |
| antecedent |
|
|
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 476-484 | |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 18446-18451 | |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 18429-18434 | |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 18463-18468 | |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 3219-3223 | |
| No TPTP formula. May not be expressible in strict first order. | Weather.kif 1838-1845 | |
| No TPTP formula. May not be expressible in strict first order. | Media.kif 2106-2113 | |
| No TPTP formula. May not be expressible in strict first order. | Media.kif 2093-2103 | |
| No TPTP formula. May not be expressible in strict first order. | Geography.kif 427-431 | |
| No TPTP formula. May not be expressible in strict first order. | Geography.kif 467-474 | |
| No TPTP formula. May not be expressible in strict first order. | Weather.kif 1935-1944 | |
| No TPTP formula. May not be expressible in strict first order. | Weather.kif 1806-1811 | |
| No TPTP formula. May not be expressible in strict first order. | QoSontology.kif 694-710 | |
| No TPTP formula. May not be expressible in strict first order. | UXExperimentalTerms.kif 799-817 |
|
| consequent |
|
|
| No TPTP formula. May not be expressible in strict first order. | People.kif 272-293 | 实数 是 串列 的 average 若且唯若 有存在 另一个 串列 和 正整数 这样 那个 另外 串列 的长度 equal 那个 串列 的长度 和 那个 另外 串列 的第 1 几个元素 equal 那个 串列 的第 1 几个元素 和 对所有 另一个 正整数
|
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 2998-3003 | |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 3005-3010 | |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 3252-3256 | |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 295-302 | |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 3083-3102 |
|
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 3179-3188 | |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 3190-3202 | |
| No TPTP formula. May not be expressible in strict first order. | Weather.kif 1486-1497 | |
| No TPTP formula. May not be expressible in strict first order. | Weather.kif 1453-1465 | |
| No TPTP formula. May not be expressible in strict first order. | Media.kif 2093-2103 | |
| No TPTP formula. May not be expressible in strict first order. | Media.kif 2075-2090 | |
| No TPTP formula. May not be expressible in strict first order. | Media.kif 2137-2150 | |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 3232-3237 | |
| No TPTP formula. May not be expressible in strict first order. | UXExperimentalTerms.kif 2388-2404 |
|
| No TPTP formula. May not be expressible in strict first order. | Media.kif 2210-2223 | |
| No TPTP formula. May not be expressible in strict first order. | Media.kif 2174-2187 | |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 3212-3217 | |
| No TPTP formula. May not be expressible in strict first order. | Media.kif 2125-2134 | |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 519-531 | |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 3113-3116 | |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 2910-2915 | |
| No TPTP formula. May not be expressible in strict first order. | Media.kif 2198-2207 | |
| No TPTP formula. May not be expressible in strict first order. | Media.kif 2161-2170 |
| statement |
|
|
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 3042-3046 | 对所有 @ROW 和 另一个 实体 (@ROW 和 那个 另外 实体) 的第 (@ROW 和 那个 另外 实体) 的长度 几个元素 equal 那个 另外 实体 |
|
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