| appearance as argument number 1 |
|
| No TPTP formula. May not be expressible in strict first order. | chinese_format.kif 1387-1389 | |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 233-236 | |
| No TPTP formula. May not be expressible in strict first order. | japanese_format.kif 45-47 | |
| No TPTP formula. May not be expressible in strict first order. | spanish_format.kif 49-52 | |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 230-230 | 子类别的定义域 的 1 数量 是 关系 的 instance |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 231-231 | 子类别的定义域 的 2 数量 是 正整数 的 instance |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 232-232 | 子类别的定义域 的 3 数量 是 类 的 instance |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 229-229 | 子类别的定义域 是 三元谓语 的 instance |
| appearance as argument number 2 |
|
|
| No TPTP formula. May not be expressible in strict first order. | chinese_format.kif 293-293 | |
| No TPTP formula. May not be expressible in strict first order. | english_format.kif 298-298 | |
| No TPTP formula. May not be expressible in strict first order. | french_format.kif 169-169 | |
| No TPTP formula. May not be expressible in strict first order. | relations-it.txt 84-84 | |
| No TPTP formula. May not be expressible in strict first order. | japanese_format.kif 1989-1989 | |
| No TPTP formula. May not be expressible in strict first order. | portuguese_format.kif 121-121 | |
| No TPTP formula. May not be expressible in strict first order. | relations-cz.txt 178-178 | |
| No TPTP formula. May not be expressible in strict first order. | relations-de.txt 381-381 | |
| No TPTP formula. May not be expressible in strict first order. | relations-hindi.txt 124-124 | |
| No TPTP formula. May not be expressible in strict first order. | relations-ro.kif 189-189 | |
| No TPTP formula. May not be expressible in strict first order. | relations-sv.txt 176-176 | |
| No TPTP formula. May not be expressible in strict first order. | relations-cb.txt 118-118 | |
| No TPTP formula. May not be expressible in strict first order. | domainEnglishFormat.kif 20118-20118 | |
| No TPTP formula. May not be expressible in strict first order. | chinese_format.kif 294-294 | |
| No TPTP formula. May not be expressible in strict first order. | domainEnglishFormat.kif 20117-20117 | |
| No TPTP formula. May not be expressible in strict first order. | domainEnglishFormat.kif 20116-20116 | |
| No TPTP formula. May not be expressible in strict first order. | terms-de.txt 119-119 | |
| No TPTP formula. May not be expressible in strict first order. | relations-tg.txt 184-184 |
| antecedent |
|
|
| 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 244-250 | |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 426-431 | |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 238-242 |
| consequent |
|
|
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 238-242 |
| appearance as argument number 0 |
|
|
| No TPTP formula. May not be expressible in strict first order. | WMD.kif 87-87 | AgentOfOrganismFn 的 1 数量 是 生物 的 subclass |
| No TPTP formula. May not be expressible in strict first order. | Music.kif 931-931 | AlbumCopiesFn 的 2 数量 是 DataStorageDevice 的 subclass |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 7577-7577 | AmountsFn 的 1 数量 是 物质 的 subclass |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 1777-1777 | Attr 的 1 数量 是 客体 的 subclass |
| No TPTP formula. May not be expressible in strict first order. | Medicine.kif 6234-6234 | BodyAreaFn 的 1 数量 是 身体部位 的 subclass |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 14972-14972 | BodySideFn 的 2 数量 是 身体部位 的 subclass |
| No TPTP formula. May not be expressible in strict first order. | VirusProteinAndCellPart.kif 1169-1169 | 细胞部分 的 2 数量 是 细胞部分 的 subclass |
| No TPTP formula. May not be expressible in strict first order. | Music.kif 1047-1047 | ContestFn 的 1 数量 是 比赛 的 subclass |
| No TPTP formula. May not be expressible in strict first order. | Mid-level-ontology.kif 29725-29725 | CoveringFn 的 1 数量 是 身体部位 的 subclass |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 8589-8589 | 日函数 的 2 数量 是 月 的 subclass |
| No TPTP formula. May not be expressible in strict first order. | Mid-level-ontology.kif 115-115 | DeadFn 的 1 数量 是 有机物体 的 subclass |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 18239-18239 | DeadOrMissingBodyPartFn 的 1 数量 是 身体部位 的 subclass |
| No TPTP formula. May not be expressible in strict first order. | Mid-level-ontology.kif 18324-18324 | DepartmentOfFn 的 2 数量 是 物理 的 subclass |
| No TPTP formula. May not be expressible in strict first order. | Mid-level-ontology.kif 18395-18395 | DepartmentOfPreventingFn 的 2 数量 是 过程 的 subclass |
| No TPTP formula. May not be expressible in strict first order. | Mid-level-ontology.kif 9979-9979 | EdemaFn 的 1 数量 是 身体部位 的 subclass |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 15508-15508 | 版本函数 的 1 数量 是 有内用物体 的 subclass |
| No TPTP formula. May not be expressible in strict first order. | ComputingBrands.kif 4514-4514 | FailureFn 的 1 数量 是 有意图过程 的 subclass |
| No TPTP formula. May not be expressible in strict first order. | Food.kif 3667-3667 | FarmOfProductFn 的 1 数量 是 生物 的 subclass |
| No TPTP formula. May not be expressible in strict first order. | Economy.kif 3724-3724 | 财政年度开始 的 2 数量 是 年 的 subclass |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 14858-14858 | FoodForFn 的 1 数量 是 生物 的 subclass |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 5498-5498 | 概括交集函数 的 1 数量 是 集或类 的 subclass |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 5487-5487 | 概括结合函数 的 1 数量 是 集或类 的 subclass |
| No TPTP formula. May not be expressible in strict first order. | Geography.kif 6913-6913 | GeographicPartTypeFn 的 1 数量 是 地理区域 的 subclass |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 8614-8614 | 时函数 的 2 数量 是 日 的 subclass |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 18218-18218 | ImpairedBodyPartFn 的 1 数量 是 身体部位 的 subclass |
| 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