UnitOfCurrency |
appearance as argument number 1 |
No TPTP formula. May not be expressible in strict first order. | chinese_format.kif 2422-2423 | |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 6310-6311 | |
No TPTP formula. May not be expressible in strict first order. | japanese_format.kif 1110-1112 | |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 6308-6308 | UnitOfCurrency 是 NonCompositeUnitOfMeasure 的 subclass |
appearance as argument number 2 |
No TPTP formula. May not be expressible in strict first order. | Economy.kif 2883-2883 | 阿富汗阿富汗尼 是 UnitOfCurrency 的 instance |
No TPTP formula. May not be expressible in strict first order. | Economy.kif 2943-2943 | 阿尔巴尼亚列克 是 UnitOfCurrency 的 instance |
No TPTP formula. May not be expressible in strict first order. | Economy.kif 2947-2947 | 阿尔及利亚第纳尔 是 UnitOfCurrency 的 instance |
No TPTP formula. May not be expressible in strict first order. | Economy.kif 2951-2951 | 安哥拉宽扎 是 UnitOfCurrency 的 instance |
No TPTP formula. May not be expressible in strict first order. | Economy.kif 2955-2955 | 阿根廷南部 是 UnitOfCurrency 的 instance |
No TPTP formula. May not be expressible in strict first order. | Economy.kif 2959-2959 | 亚美尼亚德拉姆 是 UnitOfCurrency 的 instance |
No TPTP formula. May not be expressible in strict first order. | Economy.kif 2963-2963 | 澳元 是 UnitOfCurrency 的 instance |
No TPTP formula. May not be expressible in strict first order. | Economy.kif 2967-2967 | 奥地利先令 是 UnitOfCurrency 的 instance |
No TPTP formula. May not be expressible in strict first order. | Economy.kif 2971-2971 | 阿塞拜疆马纳特 是 UnitOfCurrency 的 instance |
No TPTP formula. May not be expressible in strict first order. | Economy.kif 2975-2975 | 巴哈马元 是 UnitOfCurrency 的 instance |
No TPTP formula. May not be expressible in strict first order. | Economy.kif 2979-2979 | Bahraini第纳尔 是 UnitOfCurrency 的 instance |
No TPTP formula. May not be expressible in strict first order. | Economy.kif 2983-2983 | 孟加拉国塔卡 是 UnitOfCurrency 的 instance |
No TPTP formula. May not be expressible in strict first order. | Economy.kif 2987-2987 | 巴巴多斯元 是 UnitOfCurrency 的 instance |
No TPTP formula. May not be expressible in strict first order. | Economy.kif 2991-2991 | 白俄罗斯语rubel 是 UnitOfCurrency 的 instance |
No TPTP formula. May not be expressible in strict first order. | Economy.kif 2995-2995 | 比利时法郎 是 UnitOfCurrency 的 instance |
No TPTP formula. May not be expressible in strict first order. | Economy.kif 2999-2999 | 伯利兹美元 是 UnitOfCurrency 的 instance |
No TPTP formula. May not be expressible in strict first order. | Economy.kif 3003-3003 | 贝宁法郎 是 UnitOfCurrency 的 instance |
No TPTP formula. May not be expressible in strict first order. | Economy.kif 3007-3007 | 百慕大元 是 UnitOfCurrency 的 instance |
No TPTP formula. May not be expressible in strict first order. | Economy.kif 3011-3011 | 不丹ngultrum 是 UnitOfCurrency 的 instance |
No TPTP formula. May not be expressible in strict first order. | Economy.kif 3015-3015 | 玻利维亚玻利维亚诺 是 UnitOfCurrency 的 instance |
No TPTP formula. May not be expressible in strict first order. | Economy.kif 3019-3019 | 博茨瓦纳普拉 是 UnitOfCurrency 的 instance |
No TPTP formula. May not be expressible in strict first order. | Economy.kif 3023-3023 | 巴西真实 是 UnitOfCurrency 的 instance |
No TPTP formula. May not be expressible in strict first order. | Economy.kif 2886-2886 | 英镑 是 UnitOfCurrency 的 instance |
No TPTP formula. May not be expressible in strict first order. | Economy.kif 3027-3027 | 文莱美元 是 UnitOfCurrency 的 instance |
No TPTP formula. May not be expressible in strict first order. | Economy.kif 3031-3031 | 保加利亚列弗 是 UnitOfCurrency 的 instance |
Display limited to 25 items. Show next 25 | ||
Display limited to 25 items. Show next 25 |
appearance as argument number 3 |
No TPTP formula. May not be expressible in strict first order. | Economy.kif 3615-3615 | 货币代码 的 2 数量 是 UnitOfCurrency 的 instance |
No TPTP formula. May not be expressible in strict first order. | Economy.kif 3653-3653 | 汇率 的 1 数量 是 UnitOfCurrency 的 instance |
No TPTP formula. May not be expressible in strict first order. | Economy.kif 3639-3639 | 期间货币汇率 的 1 数量 是 UnitOfCurrency 的 instance |
No TPTP formula. May not be expressible in strict first order. | Economy.kif 2873-2873 | 货币类型 的 2 数量 是 UnitOfCurrency 的 instance |
antecedent |
No TPTP formula. May not be expressible in strict first order. | FinancialOntology.kif 3051-3062 | 有存在 金融工具, 那个 金融工具Price, and 和 另一个 实数 这样 协议 是 看涨期权 的 instance 和 那个 金融工具 是 那个 协议 的 underlier 和 那个 金融工具 是 对于 施事体 的 price 那个 金融工具Price 测量单位 和 那个 测量单位 是 UnitOfCurrency 的 instance 和 那个 另外 实数 那个 测量单位 是 那个 协议 的 strike 价钱 和 那个 金融工具Price 是 lessThan 那个 另外 实数 若且唯若 那个 施事体 是 那个 协议 的 out 资兂短缺 |
No TPTP formula. May not be expressible in strict first order. | FinancialOntology.kif 3002-3013 | 有存在 金融工具, 那个 金融工具Price, and 和 另一个 实数 这样 协议 是 看涨期权 的 instance 和 那个 金融工具 是 那个 协议 的 underlier 和 那个 金融工具 是 对于 施事体 的 price 那个 金融工具Price 测量单位 和 那个 测量单位 是 UnitOfCurrency 的 instance 和 那个 另外 实数 那个 测量单位 是 那个 协议 的 strike 价钱 和 那个 另外 实数 是 lessThan 那个 金融工具Price 若且唯若 那个 施事体 是 那个 协议 的 in 金钱 |
No TPTP formula. May not be expressible in strict first order. | FinancialOntology.kif 3015-3026 | 有存在 金融工具, 那个 金融工具Price, and 和 另一个 实数 这样 协议 是 放选项 的 instance 和 那个 金融工具 是 那个 协议 的 underlier 和 那个 金融工具 是 对于 施事体 的 price 那个 金融工具Price 测量单位 和 那个 测量单位 是 UnitOfCurrency 的 instance 和 那个 另外 实数 那个 测量单位 是 那个 协议 的 strike 价钱 和 那个 金融工具Price 是 lessThan 那个 另外 实数 若且唯若 那个 施事体 是 那个 协议 的 in 金钱 |
No TPTP formula. May not be expressible in strict first order. | FinancialOntology.kif 3064-3075 | 有存在 金融工具, 那个 金融工具Price, and 和 另一个 实数 这样 协议 是 放选项 的 instance 和 那个 金融工具 是 那个 协议 的 underlier 和 那个 金融工具 是 对于 施事体 的 price 那个 金融工具Price 测量单位 和 那个 测量单位 是 UnitOfCurrency 的 instance 和 那个 另外 实数 那个 测量单位 是 那个 协议 的 strike 价钱 和 那个 另外 实数 是 lessThan 那个 金融工具Price 若且唯若 那个 施事体 是 那个 协议 的 out 资兂短缺 |
No TPTP formula. May not be expressible in strict first order. | FinancialOntology.kif 2008-2029 |
|
No TPTP formula. May not be expressible in strict first order. | FinancialOntology.kif 2031-2052 |
|
No TPTP formula. May not be expressible in strict first order. | Merge.kif 6388-6392 | |
No TPTP formula. May not be expressible in strict first order. | UXExperimentalTerms.kif 354-365 | |
No TPTP formula. May not be expressible in strict first order. | FinancialOntology.kif 686-699 |
|
No TPTP formula. May not be expressible in strict first order. | FinancialOntology.kif 701-714 | |
No TPTP formula. May not be expressible in strict first order. | FinancialOntology.kif 759-775 |
|
No TPTP formula. May not be expressible in strict first order. | FinancialOntology.kif 3234-3250 |
|
No TPTP formula. May not be expressible in strict first order. | FinancialOntology.kif 1192-1207 |
|
No TPTP formula. May not be expressible in strict first order. | FinancialOntology.kif 3838-3852 |
|
No TPTP formula. May not be expressible in strict first order. | FinancialOntology.kif 3815-3827 | |
No TPTP formula. May not be expressible in strict first order. | UXExperimentalTerms.kif 415-423 |
|
No TPTP formula. May not be expressible in strict first order. | FinancialOntology.kif 3212-3228 |
|
No TPTP formula. May not be expressible in strict first order. | Catalog.kif 430-445 |
|
consequent |