| appearance as argument number 1 |
|
| No TPTP formula. May not be expressible in strict first order. | chinese_format.kif 1380-1385 | |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 205-213 | |
| No TPTP formula. May not be expressible in strict first order. | japanese_format.kif 38-44 | |
| No TPTP formula. May not be expressible in strict first order. | spanish_format.kif 40-48 | |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 202-202 | 域 域, 1 and Relation |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 203-203 | 域 域, 2 and PositiveInteger |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 204-204 | 域 域, 3 and Class |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 201-201 | 例 域 and TernaryPredicate |
| appearance as argument number 2 |
|
|
| No TPTP formula. May not be expressible in strict first order. | chinese_format.kif 291-291 | |
| No TPTP formula. May not be expressible in strict first order. | english_format.kif 296-296 | |
| No TPTP formula. May not be expressible in strict first order. | french_format.kif 168-168 | |
| No TPTP formula. May not be expressible in strict first order. | relations-it.txt 82-82 | |
| No TPTP formula. May not be expressible in strict first order. | japanese_format.kif 1988-1988 | |
| No TPTP formula. May not be expressible in strict first order. | portuguese_format.kif 120-120 | |
| No TPTP formula. May not be expressible in strict first order. | relations-cz.txt 177-177 | |
| No TPTP formula. May not be expressible in strict first order. | relations-de.txt 378-378 | |
| No TPTP formula. May not be expressible in strict first order. | relations-hindi.txt 122-122 | |
| No TPTP formula. May not be expressible in strict first order. | relations-ro.kif 188-188 | |
| No TPTP formula. May not be expressible in strict first order. | relations-sv.txt 175-175 | |
| No TPTP formula. May not be expressible in strict first order. | relations-cb.txt 116-116 | |
| No TPTP formula. May not be expressible in strict first order. | domainEnglishFormat.kif 20127-20127 | |
| No TPTP formula. May not be expressible in strict first order. | chinese_format.kif 292-292 | |
| No TPTP formula. May not be expressible in strict first order. | domainEnglishFormat.kif 20126-20126 | |
| No TPTP formula. May not be expressible in strict first order. | domainEnglishFormat.kif 20125-20125 | |
| No TPTP formula. May not be expressible in strict first order. | terms-de.txt 118-118 | |
| No TPTP formula. May not be expressible in strict first order. | relations-tg.txt 180-180 |
| antecedent |
|
|
| No TPTP formula. May not be expressible in strict first order. | Mid-level-ontology.kif 32339-32346 | |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 2993-2998 | |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 215-221 | |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 412-417 | |
| No TPTP formula. May not be expressible in strict first order. | Mid-level-ontology.kif 17761-17765 | |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 180-184 |
| consequent |
|
|
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 180-184 | |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 3370-3380 | |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 3413-3423 | |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 3433-3443 |
| appearance as argument number 0 |
|
|
| No TPTP formula. May not be expressible in strict first order. | UXExperimentalTerms.kif 3225-3225 | 域 ABPFn, 1 and Collection |
| No TPTP formula. May not be expressible in strict first order. | UXExperimentalTerms.kif 3270-3270 | 域 ASPFn, 1 and Collection |
| No TPTP formula. May not be expressible in strict first order. | MilitaryProcesses.kif 2411-2411 | 域 中止, 1 and AutonomousAgent |
| No TPTP formula. May not be expressible in strict first order. | MilitaryProcesses.kif 2412-2412 | 域 中止, 2 and Process |
| No TPTP formula. May not be expressible in strict first order. | MilitaryProcesses.kif 2509-2509 | 域 中止發射, 2 and 起飛 |
| No TPTP formula. May not be expressible in strict first order. | MilitaryProcesses.kif 2431-2431 | 域 任務中止, 2 and 軍事行動 |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 4752-4752 | 域 絕對值, 1 and RealNumber |
| No TPTP formula. May not be expressible in strict first order. | Cars.kif 1274-1274 | 域 AccelerationFn, 1 and FunctionQuantity |
| No TPTP formula. May not be expressible in strict first order. | Cars.kif 1275-1275 | 域 AccelerationFn, 2 and TimeDuration |
| No TPTP formula. May not be expressible in strict first order. | Cars.kif 1276-1276 | 域 AccelerationFn, 3 and Object |
| No TPTP formula. May not be expressible in strict first order. | Cars.kif 1277-1277 | 域 AccelerationFn, 4 and DirectionalAttribute |
| No TPTP formula. May not be expressible in strict first order. | FinancialOntology.kif 2330-2330 | 域 帳戶, 1 and 金融資產 |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 4702-4702 | 域 加成, 1 and RealNumber |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 4703-4703 | 域 加成, 2 and RealNumber |
| No TPTP formula. May not be expressible in strict first order. | QoSontology.kif 223-223 | 域 地址, 1 and 電腦文件 |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 8872-8872 | 域 AfternoonFn, 1 and Day |
| No TPTP formula. May not be expressible in strict first order. | Geography.kif 3044-3044 | 域 協議組織, 1 and 協議 |
| No TPTP formula. May not be expressible in strict first order. | Music.kif 930-930 | 域 AlbumCopiesFn, 1 and Album |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 7584-7584 | 域 AmountsFn, 2 and CorpuscularObject |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 7585-7585 | 域 AmountsFn, 3 and UnitOfMass |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 5249-5249 | 域 ArcCosineFn, 1 and RealNumber |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 5259-5259 | 域 ArcSineFn, 1 and RealNumber |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 5239-5239 | 域 ArcTangentFn, 1 and RealNumber |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 779-779 | 域 任務, 1 and Function |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 780-780 | 域 任務, 2 and Entity |
| 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