Proposition(命题) |
appearance as argument number 1 |
No TPTP formula. May not be expressible in strict first order. | chinese_format.kif 2031-2038 | |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 3556-3570 | |
No TPTP formula. May not be expressible in strict first order. | japanese_format.kif 673-682 | |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 3555-3555 | 命题 是 抽象体 的 subclass |
appearance as argument number 2 |
No TPTP formula. May not be expressible in strict first order. | Mid-level-ontology.kif 26913-26913 | AmericansWithDisabilitiesAct 是 命题 的 instance |
No TPTP formula. May not be expressible in strict first order. | Medicine.kif 3155-3155 | AmericansWithDisabilitiesAct-US 是 命题 的 instance |
No TPTP formula. May not be expressible in strict first order. | Government.kif 2406-2406 | 反恐怖主义和有效的死刑法 是 命题 的 instance |
No TPTP formula. May not be expressible in strict first order. | Government.kif 2404-2404 | 移民和国籍法- section219-US 是 命题 的 instance |
No TPTP formula. May not be expressible in strict first order. | Government.kif 2401-2401 | 移民和国籍行为 是 命题 的 instance |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 16880-16880 | 前提函数 的 range 是 命题 的实例 |
No TPTP formula. May not be expressible in strict first order. | Mid-level-ontology.kif 13957-13957 | 协议 是 命题 的 subclass |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 16812-16812 | 争论 是 命题 的 subclass |
No TPTP formula. May not be expressible in strict first order. | FinancialOntology.kif 3882-3882 | 银行对帐单 是 命题 的 subclass |
No TPTP formula. May not be expressible in strict first order. | Catalog.kif 31-31 | Catalog 是 命题 的 subclass |
No TPTP formula. May not be expressible in strict first order. | Mid-level-ontology.kif 22773-22773 | 分类方案 是 命题 的 subclass |
No TPTP formula. May not be expressible in strict first order. | Government.kif 647-647 | 宪法 是 命题 的 subclass |
No TPTP formula. May not be expressible in strict first order. | FinancialOntology.kif 1639-1639 | 经济指标 是 命题 的 subclass |
No TPTP formula. May not be expressible in strict first order. | engineering.kif 150-150 | 方程 是 命题 的 subclass |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 16769-16769 | 研究领域 是 命题 的 subclass |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 5622-5622 | 图 是 命题 的 subclass |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 5819-5819 | 图元素 是 命题 的 subclass |
No TPTP formula. May not be expressible in strict first order. | Hotel.kif 2725-2725 | HotelPackage 是 命题 的 subclass |
No TPTP formula. May not be expressible in strict first order. | Mid-level-ontology.kif 13786-13786 | LyricalContent 是 命题 的 subclass |
No TPTP formula. May not be expressible in strict first order. | Hotel.kif 1541-1541 | MealPlan 是 命题 的 subclass |
No TPTP formula. May not be expressible in strict first order. | engineering.kif 69-69 | 模型 是 命题 的 subclass |
No TPTP formula. May not be expressible in strict first order. | engineering.kif 1266-1266 | 多极假设 是 命题 的 subclass |
No TPTP formula. May not be expressible in strict first order. | Mid-level-ontology.kif 13733-13733 | 音乐 是 命题 的 subclass |
No TPTP formula. May not be expressible in strict first order. | Mid-level-ontology.kif 27185-27185 | Policy 是 命题 的 subclass |
No TPTP formula. May not be expressible in strict first order. | Catalog.kif 184-184 | PricingScheme 是 命题 的 subclass |
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. | Geography.kif 3012-3012 | 文献 的 1 数量 是 命题 的 instance |
No TPTP formula. May not be expressible in strict first order. | ComputingBrands.kif 4412-4412 | accountInformation 的 2 数量 是 命题 的 instance |
No TPTP formula. May not be expressible in strict first order. | Government.kif 698-698 | 协议采用日期 的 1 数量 是 命题 的 instance |
No TPTP formula. May not be expressible in strict first order. | Mid-level-ontology.kif 14067-14067 | agreementClause 的 1 数量 是 命题 的 instance |
No TPTP formula. May not be expressible in strict first order. | Government.kif 758-758 | 协议有效期间 的 1 数量 是 命题 的 instance |
No TPTP formula. May not be expressible in strict first order. | Government.kif 729-729 | 协议修订日期 的 1 数量 是 命题 的 instance |
No TPTP formula. May not be expressible in strict first order. | Government.kif 731-731 | 协议修订日期 的 3 数量 是 命题 的 instance |
No TPTP formula. May not be expressible in strict first order. | Hotel.kif 787-787 | capacityByArrangement 的 2 数量 是 命题 的 instance |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 16896-16896 | 结论 的 2 数量 是 命题 的 instance |
No TPTP formula. May not be expressible in strict first order. | Mid-level-ontology.kif 26930-26930 | conforms 的 2 数量 是 命题 的 instance |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 16904-16904 | 一贯 的 1 数量 是 命题 的 instance |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 16905-16905 | 一贯 的 2 数量 是 命题 的 instance |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 1358-1358 | 包含信息 的 2 数量 是 命题 的 instance |
No TPTP formula. May not be expressible in strict first order. | Geography.kif 3070-3070 | 日期开放供签署 的 1 数量 是 命题 的 instance |
No TPTP formula. May not be expressible in strict first order. | Mid-level-ontology.kif 7137-7137 | 投保 的 1 数量 是 命题 的 instance |
No TPTP formula. May not be expressible in strict first order. | Music.kif 1454-1454 | originalExpressedInLanguage 的 1 数量 是 命题 的 instance |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 16872-16872 | 前提 的 2 数量 是 命题 的 instance |
No TPTP formula. May not be expressible in strict first order. | Catalog.kif 170-170 | propositionOwner 的 2 数量 是 命题 的 instance |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 4598-4598 | 体现 的 2 数量 是 命题 的 instance |
No TPTP formula. May not be expressible in strict first order. | Hotel.kif 2971-2971 | reservedPackage 的 2 数量 是 命题 的 instance |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 4637-4637 | 子命题 的 1 数量 是 命题 的 instance |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 4638-4638 | 子命题 的 2 数量 是 命题 的 instance |
appearance as argument number 5 |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 1670-1670 | 抽象体 分拆成不相交的 数量, 属性, 关系, 命题, 和 串列 |
antecedent |
No TPTP formula. May not be expressible in strict first order. | Mid-level-ontology.kif 29974-29984 | |
No TPTP formula. May not be expressible in strict first order. | Catalog.kif 172-178 | |
No TPTP formula. May not be expressible in strict first order. | Geography.kif 3025-3032 | |
No TPTP formula. May not be expressible in strict first order. | Geography.kif 3018-3023 | |
No TPTP formula. May not be expressible in strict first order. | MilitaryProcesses.kif 684-690 | |
No TPTP formula. May not be expressible in strict first order. | Catalog.kif 64-76 |
consequent |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 16973-16979 | |
No TPTP formula. May not be expressible in strict first order. | Law.kif 180-188 | |
No TPTP formula. May not be expressible in strict first order. | Government.kif 653-661 | |
No TPTP formula. May not be expressible in strict first order. | Government.kif 663-671 | |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 15447-15452 | |
No TPTP formula. May not be expressible in strict first order. | UXExperimentalTerms.kif 2204-2213 |