| appearance as argument number 1 |
|
| No TPTP formula. May not be expressible in strict first order. | chinese_format.kif 1490-1491 | |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 302-304 | |
| No TPTP formula. May not be expressible in strict first order. | japanese_format.kif 50-52 | |
| No TPTP formula. May not be expressible in strict first order. | spanish_format.kif 55-57 | |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 300-300 | 域 範圍, 1 and Function |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 301-301 | 域 範圍, 2 and Class |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 299-299 | 例 範圍 and AsymmetricRelation |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 298-298 | 例 範圍 and BinaryPredicate |
| appearance as argument number 2 |
|
|
| No TPTP formula. May not be expressible in strict first order. | chinese_format.kif 313-313 | |
| No TPTP formula. May not be expressible in strict first order. | english_format.kif 318-318 | |
| No TPTP formula. May not be expressible in strict first order. | french_format.kif 179-179 | |
| No TPTP formula. May not be expressible in strict first order. | relations-it.txt 238-238 | |
| No TPTP formula. May not be expressible in strict first order. | japanese_format.kif 1999-1999 | |
| No TPTP formula. May not be expressible in strict first order. | portuguese_format.kif 131-131 | |
| No TPTP formula. May not be expressible in strict first order. | relations-cz.txt 180-180 | |
| No TPTP formula. May not be expressible in strict first order. | relations-de.txt 410-410 | |
| No TPTP formula. May not be expressible in strict first order. | relations-hindi.txt 276-276 | |
| No TPTP formula. May not be expressible in strict first order. | relations-ro.kif 199-199 | |
| No TPTP formula. May not be expressible in strict first order. | relations-sv.txt 189-189 | |
| No TPTP formula. May not be expressible in strict first order. | relations-tg.txt 430-430 | |
| No TPTP formula. May not be expressible in strict first order. | chinese_format.kif 314-314 | |
| No TPTP formula. May not be expressible in strict first order. | domainEnglishFormat.kif 48790-48790 | |
| No TPTP formula. May not be expressible in strict first order. | domainEnglishFormat.kif 48789-48789 |
| antecedent |
|
|
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 3387-3391 | |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 306-310 | |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 318-324 | |
| 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 312-316 |
| consequent |
|
|
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 312-316 |
| appearance as argument number 0 |
|
|
| No TPTP formula. May not be expressible in strict first order. | UXExperimentalTerms.kif 3227-3227 | 範圍 ABPFn and CurrencyMeasure |
| No TPTP formula. May not be expressible in strict first order. | UXExperimentalTerms.kif 3272-3272 | 範圍 ASPFn and CurrencyMeasure |
| No TPTP formula. May not be expressible in strict first order. | MilitaryProcesses.kif 2413-2413 | 範圍 中止 and Process |
| No TPTP formula. May not be expressible in strict first order. | MilitaryProcesses.kif 2510-2510 | 範圍 中止發射 and 起飛 |
| No TPTP formula. May not be expressible in strict first order. | MilitaryProcesses.kif 2432-2432 | 範圍 任務中止 and 軍事行動 |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 4757-4757 | 範圍 絕對值 and NonnegativeRealNumber |
| No TPTP formula. May not be expressible in strict first order. | Cars.kif 1280-1280 | 範圍 AccelerationFn and FunctionQuantity |
| No TPTP formula. May not be expressible in strict first order. | FinancialOntology.kif 2331-2331 | 範圍 帳戶 and 金融賬戶 |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 4708-4708 | 範圍 加成 and RealNumber |
| No TPTP formula. May not be expressible in strict first order. | QoSontology.kif 224-224 | 範圍 地址 and 實際地址 |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 8877-8877 | 範圍 AfternoonFn and 下午 |
| No TPTP formula. May not be expressible in strict first order. | Geography.kif 3045-3045 | 範圍 協議組織 and Organization |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 7590-7590 | 範圍 AmountsFn and List |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 5254-5254 | 範圍 ArcCosineFn and RealNumber |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 5264-5264 | 範圍 ArcSineFn and RealNumber |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 5244-5244 | 範圍 ArcTangentFn and RealNumber |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 781-781 | 範圍 任務 and Entity |
| No TPTP formula. May not be expressible in strict first order. | UXExperimentalTerms.kif 3195-3195 | 範圍 AuctionGMBFn and CurrencyMeasure |
| No TPTP formula. May not be expressible in strict first order. | Military.kif 924-924 | 範圍 可用於兵役男性 and Integer |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 3267-3267 | 範圍 AverageFn and RealNumber |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 892-892 | 範圍 背部 and SelfConnectedObject |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 8025-8025 | 範圍 開始 and TimePoint |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 5934-5934 | 範圍 開始節點 and GraphNode |
| No TPTP formula. May not be expressible in strict first order. | People.kif 674-674 | 範圍 BeliefGroupMemberFn and InternalAttribute |
| No TPTP formula. May not be expressible in strict first order. | UXExperimentalTerms.kif 2914-2914 | 範圍 BidCountFn and NonnegativeInteger |
| 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