No TPTP formula. May not be expressible in strict first order.	MilitaryPersons.kif 195-201	如果 无国籍人 是 实体 的 attribute 在 时间位置 holdsDuring 和 另一个 实体 是 国家 的 instance， 然后 那个 实体 不 是 那个 另外 实体 的 citizen 在 那个 时间位置 holdsDuring
No TPTP formula. May not be expressible in strict first order.	Merge.kif 16346-16351	如果 实体 和 另一个 实体 之间有 legalRelation 在 时间位置 holdsDuring 和 那个 实体 是 生物 的 instance 和 那个 另外 实体 是 生物 的 instance， 然后 那个 另外 实体 是 那个 实体 的 relative 在 那个 时间位置 holdsDuring
No TPTP formula. May not be expressible in strict first order.	Mid-level-ontology.kif 7561-7568	如果 实体 是 另一个 实体 的 member 在 时间位置 holdsDuring 和 那个 实体 是 人类 的 instance 和 那个 另外 实体 是 一群人 的 instance， 然后 那个 实体 是 那个 另外 实体 的 member 在 那个 时间位置 holdsDuring
No TPTP formula. May not be expressible in strict first order.	Media.kif 1900-1904	如果 实体 publishes 类 在 时间位置 holdsDuring 和 那个 类 是 书 的 subclass， 然后 图书出版商 是 那个 实体 的 attribute 在 那个 时间位置 holdsDuring
No TPTP formula. May not be expressible in strict first order.	Media.kif 1888-1892	如果 实体 publishes 类 在 时间位置 holdsDuring 和 那个 类 是 音乐作品 的 subclass， 然后 音乐出版商 是 那个 实体 的 attribute 在 那个 时间位置 holdsDuring
No TPTP formula. May not be expressible in strict first order.	Media.kif 1912-1916	如果 实体 publishes 类 在 时间位置 holdsDuring 和 那个 类 是 报纸 的 subclass， 然后 报纸出版社 是 那个 实体 的 attribute 在 那个 时间位置 holdsDuring
No TPTP formula. May not be expressible in strict first order.	Media.kif 1906-1910	如果 实体 publishes 类 在 时间位置 holdsDuring 和 那个 类 是 期刊 的 subclass， 然后 定期出版商 是 那个 实体 的 attribute 在 那个 时间位置 holdsDuring
No TPTP formula. May not be expressible in strict first order.	Media.kif 1894-1898	如果 实体 publishes 类 在 时间位置 holdsDuring 和 那个 类 是 文本 的 subclass， 然后 信息产业 是 那个 实体 的 attribute 在 那个 时间位置 holdsDuring
No TPTP formula. May not be expressible in strict first order.	Merge.kif 3889-3893	如果 公式 在 时间位置 holdsDuring 和 那个 公式 entails 另一个 公式， 然后 那个 另外 公式 在 那个 时间位置 holdsDuring
No TPTP formula. May not be expressible in strict first order.	Merge.kif 14359-14366	如果 实体 的发育形态 是 属性 在 时距 holdsDuring 和 另一个 属性 是 那个 属性 的后续属性， 然后 有存在 另一个 时距 这样 那个 另外 时距 比那个 时距发生的earlier 和 那个 实体 的发育形态 是 那个 另外 属性 在 那个 另外 时距 holdsDuring
No TPTP formula. May not be expressible in strict first order.	Merge.kif 7976-7980	如果 公式 在 时间位置 holdsDuring 和 另一个 时间位置 时段 是 那个 时间位置 时段 的一 part， 然后 那个 公式 在 那个 另外 时间位置 holdsDuring
No TPTP formula. May not be expressible in strict first order.	FinancialOntology.kif 3529-3534	如果 银行卡 是 过期的卡 的 instance 在 时间位置 holdsDuring 和 金融账户 是 那个 银行卡 的 card 帐户， 然后 ActiveAgreement 不 是 那个 银行卡 的 attribute 在 那个 时间位置 holdsDuring
No TPTP formula. May not be expressible in strict first order.	Economy.kif 2583-2592	如果 地缘政治区域 对于 有点 时距 在周期 货币测量 import 全部 和 有点 时距 是 年 的 subclass 或 那个 有点 时距 是 那个 地缘政治区域 的 fiscal 年 的 subclass， 然后 有存在 时间位置 这样 那个 时间位置 是 那个 有点 时距 的 instance 和 那个 货币测量 是 那个 地缘政治区域 的 annual 总共输入 在 那个 时间位置 holdsDuring
No TPTP formula. May not be expressible in strict first order.	Government.kif 546-553	如果 有点 时距 是 地缘政治区域 的 independence 日期 和 时间位置 是 有点 时距 的 instance， 然后 不存在 实体 这样 那个 地缘政治区域 是 那个 实体 的 dependent 在 那个 时间位置 之后 holdsDuring
No TPTP formula. May not be expressible in strict first order.	Mid-level-ontology.kif 23709-23718	如果 %每个 有点 客体 是 另一个 有点 客体 的 initially part 和 物理 是 有点 客体 的 instance， 然后 有存在 实体 这样 那个 实体 是 另一个 有点 客体 的 instance 和 那个 物理 是 那个 实体 的 part 在 那个 物理 出现 的 time 的开始 holdsDuring
No TPTP formula. May not be expressible in strict first order.	Mid-level-ontology.kif 23736-23744	如果 有点 客体 的例子总是 另一个 有点 客体 的 initially part 的例子 和 物理 是 另一个 有点 客体 的 instance， 然后 有存在 实体 这样 那个 实体 是 有点 客体 的 instance 和 那个 实体 是 那个 物理 的 part 在 那个 物理 出现 的 time 的开始 holdsDuring
No TPTP formula. May not be expressible in strict first order.	Mid-level-ontology.kif 21494-21505	如果 过程 是 中止 的 instance 和 实体 是 那个 过程 的 patient 和 那个 实体 是 女人 的 instance， 然后 孕 是 那个 实体 的 attribute 在 那个 过程 出现 的 time 的开始 holdsDuring 和 孕 不 是 那个 实体 的 attribute 在 那个 过程 出现 的 time 的结束 holdsDuring
No TPTP formula. May not be expressible in strict first order.	Medicine.kif 6257-6275	如果 过程 是 Amputating 的 instance 和 实体 是 那个 过程 的 patient 和 客体 是 肢 的 instance， 然后 有存在 另一个 客体 和 第三 客体 这样 那个 另外 客体 是 那个 客体 的 part 和 那个 第三 客体 是 那个 另外 客体 的 part 和 那个 第三 客体 是 骨骼 的 instance 和 那个 另外 客体 是 那个 实体 的 part 在 紧接 那个 过程 出现 的 time before holdsDuring 和 那个 另外 客体 不 是 那个 实体 的 part 在 紧接 那个 过程 出现 的 time before holdsDuring
No TPTP formula. May not be expressible in strict first order.	Medicine.kif 966-975	如果 过程 是 Anesthetizing 的 instance 和 实体 是 那个 过程 的 patient， 然后 无意识 是 那个 实体 的 attribute 和 痛 不 是 那个 实体 的 attribute 在 那个 过程 出现 的 time holdsDuring
No TPTP formula. May not be expressible in strict first order.	Medicine.kif 949-958	如果 过程 是 Anesthetizing 的 instance 和 实体 是 那个 过程 的 patient， 然后 无意识 是 那个 实体 的 attribute 或 痛 不 是 那个 实体 的 attribute 在 那个 过程 出现 的 time holdsDuring
No TPTP formula. May not be expressible in strict first order.	Mid-level-ontology.kif 29608-29620	如果 过程 是 Apologizing 的 instance 和 那个 过程G 是 那个 过程 的 agent 和 那个 过程 在 另一个 施事体 结束， 然后 有存在 那个 过程CT 这样 那个 另外 施事体 suffers 从 那个 过程CT 和 那个 过程G 是 那个 过程CT 的 agent 和 那个 过程G doesn't wants 那个 过程CT 在 那个 过程 出现 的 time holdsDuring
No TPTP formula. May not be expressible in strict first order.	Mid-level-ontology.kif 1042-1055	如果 过程 是 任命 的 instance 和 实体 是 那个 过程 的 patient， 然后 有存在 另一个 实体 和 第三 实体 这样 那个 实体 doesn't 在 那个 第三 实体 任职 那个 另外 实体 在 那个 过程 出现 的 time 的开始 holdsDuring 和 那个 实体 在 那个 第三 实体 任职 那个 另外 实体 在 紧接 那个 过程 出现 的 time after holdsDuring
No TPTP formula. May not be expressible in strict first order.	Medicine.kif 6304-6313	如果 过程 是 Asphyxiation 的 instance 和 施事体 经历了 那个 过程， 然后 不存在 实体 这样 那个 实体 是 呼吸 的 instance 和 那个 过程 经历了 那个 实体 在 那个 过程 出现 的 time holdsDuring
No TPTP formula. May not be expressible in strict first order.	Medicine.kif 1008-1019	如果 过程 是 LocalAnesthetizing 的 instance 和 那个 过程 是 located 在 客体 和 那个 客体 是 身体部位 的 instance 和 那个 客体 是 另一个 客体 的 part 和 那个 另外 客体 是 那个 过程 的 patient， 然后 PainFn 那个 客体 不 是 那个 另外 客体 的 attribute 在 那个 过程 出现 的 time holdsDuring
No TPTP formula. May not be expressible in strict first order.	Medicine.kif 983-992	如果 过程 是 Sedating 的 instance 和 实体 是 那个 过程 的 patient， 然后 Conscious 是 那个 实体 的 attribute 和 焦虑 不 是 那个 实体 的 attribute 在 那个 过程 出现 的 time holdsDuring
Display limited to 25 items. Show next 25
Display limited to 25 items. Show next 25

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