MeasureFn |
appearance as argument number 1 |
No TPTP formula. May not be expressible in strict first order. | chinese_format.kif 2434-2436 | |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 6352-6356 | |
No TPTP formula. May not be expressible in strict first order. | japanese_format.kif 1125-1128 | |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 6348-6348 | 域 測量, 1 and RealNumber |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 6349-6349 | 域 測量, 2 and UnitOfMeasure |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 6346-6346 | 例 測量 and BinaryFunction |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 6347-6347 | 例 測量 and TotalValuedRelation |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 6350-6350 | 範圍 測量 and PhysicalQuantity |
appearance as argument number 2 |
No TPTP formula. May not be expressible in strict first order. | chinese_format.kif 633-633 | |
No TPTP formula. May not be expressible in strict first order. | english_format.kif 636-636 | |
No TPTP formula. May not be expressible in strict first order. | french_format.kif 383-383 | |
No TPTP formula. May not be expressible in strict first order. | relations-it.txt 178-178 | |
No TPTP formula. May not be expressible in strict first order. | japanese_format.kif 2113-2113 | |
No TPTP formula. May not be expressible in strict first order. | portuguese_format.kif 335-335 | |
No TPTP formula. May not be expressible in strict first order. | relations-cz.txt 392-392 | |
No TPTP formula. May not be expressible in strict first order. | relations-de.txt 829-829 | |
No TPTP formula. May not be expressible in strict first order. | relations-hindi.txt 216-216 | |
No TPTP formula. May not be expressible in strict first order. | relations-ro.kif 405-405 | |
No TPTP formula. May not be expressible in strict first order. | relations-sv.txt 426-426 | |
No TPTP formula. May not be expressible in strict first order. | domainEnglishFormat.kif 36671-36671 | |
No TPTP formula. May not be expressible in strict first order. | chinese_format.kif 634-634 | |
No TPTP formula. May not be expressible in strict first order. | domainEnglishFormat.kif 36670-36670 | |
No TPTP formula. May not be expressible in strict first order. | domainEnglishFormat.kif 36669-36669 | |
No TPTP formula. May not be expressible in strict first order. | relations-tg.txt 353-353 |
antecedent |
No TPTP formula. May not be expressible in strict first order. | Geography.kif 7524-7530 | 例 SelfConnectedObject and LiquidDrop SelfConnectedObject 的 approximate diameter 是 測量 RealNumber and Micrometer 少於 500.0 and RealNumber 例 SelfConnectedObject and Droplet |
No TPTP formula. May not be expressible in strict first order. | Geography.kif 7440-7451 | 例 Object and ParticulateMatter 部分 SelfConnectedObject and Object SelfConnectedObject 的 approximate diameter 是 測量 RealNumber and Micrometer 比較多 10.0 and RealNumber 比較多 RealNumber and 2.5 Object0 例 Object0 and CoarseParticulateMatter 部分 Object0 and Object |
No TPTP formula. May not be expressible in strict first order. | Geography.kif 7469-7479 | 例 Object and ParticulateMatter 部分 SelfConnectedObject and Object SelfConnectedObject 的 approximate diameter 是 測量 RealNumber and Micrometer 大於或等於 RealNumber and 2.5 Object5 例 Object5 and FineParticulateMatter 部分 Object5 and Object |
No TPTP formula. May not be expressible in strict first order. | Geography.kif 3731-3733 | Object 對於 %3 courseWRT 實際北 方位 Object, Object and 北 |
No TPTP formula. May not be expressible in strict first order. | Geography.kif 3755-3757 | Object 對於 %3 courseWRT 實際北 方位 Object, Object and 東南 |
No TPTP formula. May not be expressible in strict first order. | Geography.kif 3739-3741 | Object 對於 %3 courseWRT 實際北 方位 Object, Object and 南 |
No TPTP formula. May not be expressible in strict first order. | Geography.kif 3759-3761 | Object 對於 %3 courseWRT 實際北 方位 Object, Object and 西南 |
No TPTP formula. May not be expressible in strict first order. | Geography.kif 3743-3745 | Object 對於 %3 courseWRT 實際北 方位 Object, Object and 西方 |
No TPTP formula. May not be expressible in strict first order. | Geography.kif 3763-3765 | Object 對於 %3 courseWRT 實際北 方位 Object, Object and 西北 |
No TPTP formula. May not be expressible in strict first order. | Geography.kif 3747-3749 | Object 對於 %3 courseWRT 實際北 方位 Object, Object and 北 |
No TPTP formula. May not be expressible in strict first order. | Geography.kif 3751-3753 | Object 對於 %3 courseWRT 實際北 方位 Object, Object and 東北 |
No TPTP formula. May not be expressible in strict first order. | Geography.kif 3735-3737 | Object 對於 %3 courseWRT 實際北 方位 Object, Object and 東 |
No TPTP formula. May not be expressible in strict first order. | Weather.kif 1702-1708 | 等於 FunctionQuantity and 測量 RealNumber and MilesPerHour 等於 FunctionQuantity and 速度 測量 RealNumber and 英里 and 測量 1 and 小時 |
No TPTP formula. May not be expressible in strict first order. | FinancialOntology.kif 3051-3062 | 金融工具 金融工具Price and RealNumber 例 協議 and 看漲期權 金融工具 是 協議 的 underlier 金融工具 是 對於 AutonomousAgent 的 price 測量 金融工具Price and UnitOfMeasure 例 UnitOfMeasure and UnitOfCurrency 測量 RealNumber and UnitOfMeasure 是 協議 的 strike 價錢 少於 金融工具Price and RealNumber AutonomousAgent 是 協議 的 out 資兂短缺 |
No TPTP formula. May not be expressible in strict first order. | FinancialOntology.kif 3002-3013 | 金融工具 金融工具Price and RealNumber 例 協議 and 看漲期權 金融工具 是 協議 的 underlier 金融工具 是 對於 AutonomousAgent 的 price 測量 金融工具Price and UnitOfMeasure 例 UnitOfMeasure and UnitOfCurrency 測量 RealNumber and UnitOfMeasure 是 協議 的 strike 價錢 少於 RealNumber and 金融工具Price AutonomousAgent 是 協議 的 in 金錢 |
No TPTP formula. May not be expressible in strict first order. | FinancialOntology.kif 3015-3026 | 金融工具 金融工具Price and RealNumber 例 協議 and 放選項 金融工具 是 協議 的 underlier 金融工具 是 對於 AutonomousAgent 的 price 測量 金融工具Price and UnitOfMeasure 例 UnitOfMeasure and UnitOfCurrency 測量 RealNumber and UnitOfMeasure 是 協議 的 strike 價錢 少於 金融工具Price and RealNumber AutonomousAgent 是 協議 的 in 金錢 |
No TPTP formula. May not be expressible in strict first order. | FinancialOntology.kif 3064-3075 | 金融工具 金融工具Price and RealNumber 例 協議 and 放選項 金融工具 是 協議 的 underlier 金融工具 是 對於 AutonomousAgent 的 price 測量 金融工具Price and UnitOfMeasure 例 UnitOfMeasure and UnitOfCurrency 測量 RealNumber and UnitOfMeasure 是 協議 的 strike 價錢 少於 RealNumber and 金融工具Price AutonomousAgent 是 協議 的 out 資兂短缺 |
No TPTP formula. May not be expressible in strict first order. | Medicine.kif 1783-1787 | hearingAcuity Human, 測量 -10 and Decibel and 測量 15 and Decibel attribute Human and NormalHearingSensitivity |
No TPTP formula. May not be expressible in strict first order. | Medicine.kif 1794-1798 | hearingAcuity Human, 測量 16 and Decibel and 測量 25 and Decibel attribute Human and BorderlineHearingSensitivity |
No TPTP formula. May not be expressible in strict first order. | Medicine.kif 1805-1809 | hearingAcuity Human, 測量 26 and Decibel and 測量 40 and Decibel attribute Human and MildHearingLoss |
No TPTP formula. May not be expressible in strict first order. | Medicine.kif 1815-1819 | hearingAcuity Human, 測量 41 and Decibel and 測量 55 and Decibel attribute Human and ModerateHearingLoss |
No TPTP formula. May not be expressible in strict first order. | Medicine.kif 1826-1830 | hearingAcuity Human, 測量 56 and Decibel and 測量 70 and Decibel attribute Human and ModeratelySevereHearingLoss |
No TPTP formula. May not be expressible in strict first order. | Medicine.kif 1837-1841 | hearingAcuity Human, 測量 71 and Decibel and 測量 90 and Decibel attribute Human and SevereHearingLoss |
No TPTP formula. May not be expressible in strict first order. | Medicine.kif 1848-1852 | hearingAcuity Human, 測量 91 and Decibel and 測量 200 and Decibel attribute Human and ProfoundHearingLoss |
No TPTP formula. May not be expressible in strict first order. | Mid-level-ontology.kif 13605-13611 | 測量 Physical and 測量 RealNumber and 公噸 測量 Physical and 測量 乘法 RealNumber and 2205.0 and 磅質量 |
Display limited to 25 items. Show next 25 | ||
Display limited to 25 items. Show next 25 |
consequent |
statement |
No TPTP formula. May not be expressible in strict first order. | Mid-level-ontology.kif 29358-29358 | 測量 3470.0 and 凱文度 是 錒 的 boiling 點 |
No TPTP formula. May not be expressible in strict first order. | Mid-level-ontology.kif 29206-29206 | 測量 2740.0 and 凱文度 是 鋁 的 boiling 點 |
No TPTP formula. May not be expressible in strict first order. | Mid-level-ontology.kif 29370-29370 | 測量 2880.0 and 凱文度 是 銤 的 boiling 點 |
No TPTP formula. May not be expressible in strict first order. | Mid-level-ontology.kif 29282-29282 | 測量 2023.0 and 凱文度 是 銻 的 boiling 點 |
No TPTP formula. May not be expressible in strict first order. | Mid-level-ontology.kif 29216-29216 | 測量 87.29 and 凱文度 是 氬 的 boiling 點 |
No TPTP formula. May not be expressible in strict first order. | Mid-level-ontology.kif 29246-29246 | 測量 886.0 and 凱文度 是 砷 的 boiling 點 |
No TPTP formula. May not be expressible in strict first order. | Mid-level-ontology.kif 29350-29350 | 測量 610.0 and 凱文度 是 砹 的 boiling 點 |
No TPTP formula. May not be expressible in strict first order. | Mid-level-ontology.kif 29292-29292 | 測量 1913.0 and 凱文度 是 鋇 的 boiling 點 |
No TPTP formula. May not be expressible in strict first order. | Mid-level-ontology.kif 29188-29188 | 測量 3243.0 and 凱文度 是 鈹 的 boiling 點 |
No TPTP formula. May not be expressible in strict first order. | Mid-level-ontology.kif 29346-29346 | 測量 1833.0 and 凱文度 是 鉍 的 boiling 點 |
No TPTP formula. May not be expressible in strict first order. | Mid-level-ontology.kif 29190-29190 | 測量 2823.0 and 凱文度 是 硼 的 boiling 點 |
No TPTP formula. May not be expressible in strict first order. | Mid-level-ontology.kif 29250-29250 | 測量 331.93 and 凱文度 是 溴 的 boiling 點 |
No TPTP formula. May not be expressible in strict first order. | Mid-level-ontology.kif 29276-29276 | 測量 1038.0 and 凱文度 是 鎘 的 boiling 點 |
No TPTP formula. May not be expressible in strict first order. | Mid-level-ontology.kif 29290-29290 | 測量 963.0 and 凱文度 是 銫 的 boiling 點 |
No TPTP formula. May not be expressible in strict first order. | Mid-level-ontology.kif 29220-29220 | 測量 1760.0 and 凱文度 是 鈣 的 boiling 點 |
No TPTP formula. May not be expressible in strict first order. | Mid-level-ontology.kif 29192-29192 | 測量 5100.0 and 凱文度 是 碳 的 boiling 點 |
No TPTP formula. May not be expressible in strict first order. | Mid-level-ontology.kif 29296-29296 | 測量 3530.0 and 凱文度 是 鈰 的 boiling 點 |
No TPTP formula. May not be expressible in strict first order. | Mid-level-ontology.kif 29214-29214 | 測量 238.55 and 凱文度 是 氯 的 boiling 點 |
No TPTP formula. May not be expressible in strict first order. | Mid-level-ontology.kif 29228-29228 | 測量 2755.0 and 凱文度 是 鉻 的 boiling 點 |
No TPTP formula. May not be expressible in strict first order. | Mid-level-ontology.kif 29234-29234 | 測量 3143.0 and 凱文度 是 鈷 的 boiling 點 |
No TPTP formula. May not be expressible in strict first order. | Mid-level-ontology.kif 29238-29238 | 測量 2868.0 and 凱文度 是 銅 的 boiling 點 |
No TPTP formula. May not be expressible in strict first order. | Mid-level-ontology.kif 29312-29312 | 測量 2608.0 and 凱文度 是 鏑 的 boiling 點 |
No TPTP formula. May not be expressible in strict first order. | Mid-level-ontology.kif 29316-29316 | 測量 2783.0 and 凱文度 是 鉺 的 boiling 點 |
No TPTP formula. May not be expressible in strict first order. | Mid-level-ontology.kif 29306-29306 | 測量 1870.0 and 凱文度 是 銪 的 boiling 點 |
No TPTP formula. May not be expressible in strict first order. | Mid-level-ontology.kif 29198-29198 | 測量 85.01 and 凱文度 是 氟 的 boiling 點 |
Display limited to 25 items. Show next 25 | ||
Display limited to 25 items. Show next 25 |