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 6377-6381 | |
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 6373-6373 | The number 1 argument of measure is an instance of real number |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 6374-6374 | The number 2 argument of measure is an instance of unit of measure |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 6371-6371 | Measure is an instance of binary function |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 6372-6372 | Measure is an instance of total valued relation |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 6375-6375 | The range of measure is an instance of physical quantity |
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 36680-36680 | |
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 36679-36679 | |
No TPTP formula. May not be expressible in strict first order. | domainEnglishFormat.kif 36678-36678 | |
No TPTP formula. May not be expressible in strict first order. | terms-de.txt 245-245 | |
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 7861-7867 | A self connected object is an instance of liquid drop and the approximate diameter of the self connected object is a real number micrometer(s) and 500.0 is less than the real number if and only if the self connected object is an instance of droplet |
No TPTP formula. May not be expressible in strict first order. | Geography.kif 7777-7788 | An object is an instance of PM and a self connected object is a part of the object and the approximate diameter of the self connected object is a real number micrometer(s) and 10.0 is greater than the real number and the real number is greater than 2.5 if and only if there exists the object10 such that the object10 is an instance of PM10 and the object10 is a part of the object |
No TPTP formula. May not be expressible in strict first order. | Geography.kif 7806-7816 | An object is an instance of PM and a self connected object is a part of the object and the approximate diameter of the self connected object is a real number micrometer(s) and the real number is greater than or equal to 2.5 if and only if there exists the object25 such that the object25 is an instance of PM2.5 and the object25 is a part of the object |
No TPTP formula. May not be expressible in strict first order. | Geography.kif 3889-3891 | An object courseWRT true north another object for 0.0 angular degree(s) if and only if the object is north to the other object |
No TPTP formula. May not be expressible in strict first order. | Geography.kif 3913-3915 | An object courseWRT true north another object for 135.0 angular degree(s) if and only if the object is southeast to the other object |
No TPTP formula. May not be expressible in strict first order. | Geography.kif 3897-3899 | An object courseWRT true north another object for 180.0 angular degree(s) if and only if the object is south to the other object |
No TPTP formula. May not be expressible in strict first order. | Geography.kif 3917-3919 | An object courseWRT true north another object for 225.0 angular degree(s) if and only if the object is southwest to the other object |
No TPTP formula. May not be expressible in strict first order. | Geography.kif 3901-3903 | An object courseWRT true north another object for 270.0 angular degree(s) if and only if the object is west to the other object |
No TPTP formula. May not be expressible in strict first order. | Geography.kif 3921-3923 | An object courseWRT true north another object for 315.0 angular degree(s) if and only if the object is northwest to the other object |
No TPTP formula. May not be expressible in strict first order. | Geography.kif 3905-3907 | An object courseWRT true north another object for 360.0 angular degree(s) if and only if the object is north to the other object |
No TPTP formula. May not be expressible in strict first order. | Geography.kif 3909-3911 | An object courseWRT true north another object for 45.0 angular degree(s) if and only if the object is northeast to the other object |
No TPTP formula. May not be expressible in strict first order. | Geography.kif 3893-3895 | An object courseWRT true north another object for 90.0 angular degree(s) if and only if the object is east to the other object |
No TPTP formula. May not be expressible in strict first order. | Weather.kif 2426-2432 | equal a function quantity and a real number miles per hour(s) if and only if equal the function quantity and the real number mile(s) per 1 hour duration(s) |
No TPTP formula. May not be expressible in strict first order. | FinancialOntology.kif 3068-3079 | There exist a financial instrument, the financial instrumentPrice and another real number such that an agreement is an instance of call option and the financial instrument is an underlier of the agreement and the financial instrument is price the financial instrumentPrice an unit of measure(s) for an agent and the unit of measure is an instance of unit of currency and the other real number the unit of measure(s) is a strike price of the agreement and the financial instrumentPrice is less than the other real number if and only if the agent is an out of the money of the agreement |
No TPTP formula. May not be expressible in strict first order. | FinancialOntology.kif 3019-3030 | There exist a financial instrument, the financial instrumentPrice and another real number such that an agreement is an instance of call option and the financial instrument is an underlier of the agreement and the financial instrument is price the financial instrumentPrice an unit of measure(s) for an agent and the unit of measure is an instance of unit of currency and the other real number the unit of measure(s) is a strike price of the agreement and the other real number is less than the financial instrumentPrice if and only if the agent is an in the money of the agreement |
No TPTP formula. May not be expressible in strict first order. | FinancialOntology.kif 3032-3043 | There exist a financial instrument, the financial instrumentPrice and another real number such that an agreement is an instance of put option and the financial instrument is an underlier of the agreement and the financial instrument is price the financial instrumentPrice an unit of measure(s) for an agent and the unit of measure is an instance of unit of currency and the other real number the unit of measure(s) is a strike price of the agreement and the financial instrumentPrice is less than the other real number if and only if the agent is an in the money of the agreement |
No TPTP formula. May not be expressible in strict first order. | FinancialOntology.kif 3081-3092 | There exist a financial instrument, the financial instrumentPrice and another real number such that an agreement is an instance of put option and the financial instrument is an underlier of the agreement and the financial instrument is price the financial instrumentPrice an unit of measure(s) for an agent and the unit of measure is an instance of unit of currency and the other real number the unit of measure(s) is a strike price of the agreement and the other real number is less than the financial instrumentPrice if and only if the agent is an out of the money of the agreement |
No TPTP formula. May not be expressible in strict first order. | Medicine.kif 1776-1780 | A human can hear frequency of -10 dB(A)(s) at 15 dB(A)(s) decibels if and only if normal hearing sensitivity is an attribute of the human |
No TPTP formula. May not be expressible in strict first order. | Medicine.kif 1787-1791 | A human can hear frequency of 16 dB(A)(s) at 25 dB(A)(s) decibels if and only if borderline hearing sensitivity is an attribute of the human |
No TPTP formula. May not be expressible in strict first order. | Medicine.kif 1798-1802 | A human can hear frequency of 26 dB(A)(s) at 40 dB(A)(s) decibels if and only if mild hearing loss is an attribute of the human |
No TPTP formula. May not be expressible in strict first order. | Medicine.kif 1808-1812 | A human can hear frequency of 41 dB(A)(s) at 55 dB(A)(s) decibels if and only if moderate hearing loss is an attribute of the human |
No TPTP formula. May not be expressible in strict first order. | Medicine.kif 1819-1823 | A human can hear frequency of 56 dB(A)(s) at 70 dB(A)(s) decibels if and only if moderately severe hearing loss is an attribute of the human |
No TPTP formula. May not be expressible in strict first order. | Medicine.kif 1830-1834 | A human can hear frequency of 71 dB(A)(s) at 90 dB(A)(s) decibels if and only if severe hearing loss is an attribute of the human |
No TPTP formula. May not be expressible in strict first order. | Medicine.kif 1841-1845 | A human can hear frequency of 91 dB(A)(s) at 200 dB(A)(s) decibels if and only if profound hearing loss is an attribute of the human |
No TPTP formula. May not be expressible in strict first order. | Mid-level-ontology.kif 14944-14950 | The measure of a physical is a real number metric ton(s) if and only if the measure of the physical is the real number and 2205.0 pound mass(s) |
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 31277-31277 | 3470.0 Kelvin degree(s) is a boiling point of actinium |
No TPTP formula. May not be expressible in strict first order. | Mid-level-ontology.kif 31125-31125 | 2740.0 Kelvin degree(s) is a boiling point of aluminum |
No TPTP formula. May not be expressible in strict first order. | Mid-level-ontology.kif 31289-31289 | 2880.0 Kelvin degree(s) is a boiling point of americium |
No TPTP formula. May not be expressible in strict first order. | Mid-level-ontology.kif 31201-31201 | 2023.0 Kelvin degree(s) is a boiling point of antimony |
No TPTP formula. May not be expressible in strict first order. | Mid-level-ontology.kif 31135-31135 | 87.29 Kelvin degree(s) is a boiling point of argon |
No TPTP formula. May not be expressible in strict first order. | Mid-level-ontology.kif 31165-31165 | 886.0 Kelvin degree(s) is a boiling point of arsenic |
No TPTP formula. May not be expressible in strict first order. | Mid-level-ontology.kif 31269-31269 | 610.0 Kelvin degree(s) is a boiling point of astatine |
No TPTP formula. May not be expressible in strict first order. | Mid-level-ontology.kif 31211-31211 | 1913.0 Kelvin degree(s) is a boiling point of barium |
No TPTP formula. May not be expressible in strict first order. | Mid-level-ontology.kif 31107-31107 | 3243.0 Kelvin degree(s) is a boiling point of beryllium |
No TPTP formula. May not be expressible in strict first order. | Mid-level-ontology.kif 31265-31265 | 1833.0 Kelvin degree(s) is a boiling point of bismuth |
No TPTP formula. May not be expressible in strict first order. | Mid-level-ontology.kif 31109-31109 | 2823.0 Kelvin degree(s) is a boiling point of boron |
No TPTP formula. May not be expressible in strict first order. | Mid-level-ontology.kif 31169-31169 | 331.93 Kelvin degree(s) is a boiling point of bromine |
No TPTP formula. May not be expressible in strict first order. | Mid-level-ontology.kif 31195-31195 | 1038.0 Kelvin degree(s) is a boiling point of cadmium |
No TPTP formula. May not be expressible in strict first order. | Mid-level-ontology.kif 31209-31209 | 963.0 Kelvin degree(s) is a boiling point of caesium |
No TPTP formula. May not be expressible in strict first order. | Mid-level-ontology.kif 31139-31139 | 1760.0 Kelvin degree(s) is a boiling point of calcium |
No TPTP formula. May not be expressible in strict first order. | Mid-level-ontology.kif 31111-31111 | 5100.0 Kelvin degree(s) is a boiling point of carbon |
No TPTP formula. May not be expressible in strict first order. | Mid-level-ontology.kif 31215-31215 | 3530.0 Kelvin degree(s) is a boiling point of cerium |
No TPTP formula. May not be expressible in strict first order. | Mid-level-ontology.kif 31133-31133 | 238.55 Kelvin degree(s) is a boiling point of chlorine |
No TPTP formula. May not be expressible in strict first order. | Mid-level-ontology.kif 31147-31147 | 2755.0 Kelvin degree(s) is a boiling point of chromium |
No TPTP formula. May not be expressible in strict first order. | Mid-level-ontology.kif 31153-31153 | 3143.0 Kelvin degree(s) is a boiling point of cobalt |
No TPTP formula. May not be expressible in strict first order. | Mid-level-ontology.kif 31157-31157 | 2868.0 Kelvin degree(s) is a boiling point of copper |
No TPTP formula. May not be expressible in strict first order. | Mid-level-ontology.kif 31231-31231 | 2608.0 Kelvin degree(s) is a boiling point of dysprosium |
No TPTP formula. May not be expressible in strict first order. | Mid-level-ontology.kif 31235-31235 | 2783.0 Kelvin degree(s) is a boiling point of erbium |
No TPTP formula. May not be expressible in strict first order. | Mid-level-ontology.kif 31225-31225 | 1870.0 Kelvin degree(s) is a boiling point of europium |
No TPTP formula. May not be expressible in strict first order. | Mid-level-ontology.kif 31117-31117 | 85.01 Kelvin degree(s) is a boiling point of fluorine |
Display limited to 25 items. Show next 25 | ||
Display limited to 25 items. Show next 25 |
![]() |
![]() |