No TPTP formula. May not be expressible in strict first order.	Merge.kif 9116-9120	如果 时距 是 三月 month 的 instance 和 另一个 时距 是 A四月 month 的 instance， 然后 那个 时距 接着 那个 另外 时距
No TPTP formula. May not be expressible in strict first order.	Merge.kif 9144-9148	如果 时距 是 五月 month 的 instance 和 另一个 时距 是 六月 month 的 instance， 然后 那个 时距 接着 那个 另外 时距
No TPTP formula. May not be expressible in strict first order.	Merge.kif 9229-9233	如果 时距 是 十一月 month 的 instance 和 另一个 时距 是 十二月 month 的 instance， 然后 那个 时距 接着 那个 另外 时距
No TPTP formula. May not be expressible in strict first order.	Merge.kif 9215-9219	如果 时距 是 十月 month 的 instance 和 另一个 时距 是 十一月 month 的 instance， 然后 那个 时距 接着 那个 另外 时距
No TPTP formula. May not be expressible in strict first order.	Merge.kif 9201-9205	如果 时距 是 九月 month 的 instance 和 另一个 时距 是 十月 month 的 instance， 然后 那个 时距 接着 那个 另外 时距
No TPTP formula. May not be expressible in strict first order.	FinancialOntology.kif 293-306	如果 过程 是 开户 的 instance 和 那个 过程 是 located 在 金融机构 和 那个 金融机构 是 金融机构 的 instance 和 有认知的主事 是 那个 过程 的 agent 和 那个 过程 出现 的 time equal 那个 过程Time， 然后 有存在 金融账户 和 那个 金融账户Period 这样 那个 金融账户Period 是 那个 金融账户 的 agreement 週期 和 那个 过程Time 接着 那个 金融账户Period 和 那个 金融账户 是 金融账户 的 instance 和 那个 金融账户 是被 那个 金融机构 held 和 那个 有认知的主事 持有 account 那个 金融账户
No TPTP formula. May not be expressible in strict first order.	FinancialOntology.kif 1952-1959	如果 物理 是 正在下单 的 instance 和 那个 物理 出现 的 time equal 时距， 然后 有存在 另一个 物理 和 另一个 时距 这样 那个 另外 物理 出现 的 time equal 那个 另外 时距 和 那个 时距 接着 那个 另外 时距
No TPTP formula. May not be expressible in strict first order.	Merge.kif 8705-8710	如果 时距 是 正整数 second 的 instance 和 另一个 时距 是 另一个 正整数 second 的 instance 和 (那个 另外 正整数 和 那个 正整数) equal 1， 然后 那个 时距 接着 那个 另外 时距
No TPTP formula. May not be expressible in strict first order.	Medicine.kif 5997-6017	如果 时距 是 TimePeriod 的 instance 和 那个 时距 的 duration 是 实数 分钟 和 那个 实数 是 greaterThan 5.0 和 实体 是 人类 的 instance 和 不存在 过程 这样 那个 过程 是 呼吸 的 instance 和 那个 过程 出现 的 time 在 那个 时距 时段内发生 和 那个 实体 是 那个 过程 的 patient， 然后 有存在 另一个 实体 这样 那个 另外 实体 是 死亡 的 instance 和 那个 实体 经历了 那个 另外 实体 和 那个 时距 接着 那个 另外 实体 出现 的 time 的声明 has 容易 的语气
No TPTP formula. May not be expressible in strict first order.	FinancialOntology.kif 3212-3228	如果 过程 是 上扬 的 instance 和 物理 是 那个 过程 的 patient 和 那个 过程 出现 的 time equal 施事体 和 测量单位 是 UnitOfCurrency 的 instance 和 那个 物理 是 对于 那个 施事体 的 price 实数 那个 测量单位 ， 然后 有存在 另一个 过程， 另一个 施事体， and 和 另一个 实数 这样 那个 另外 过程 是 股市交易 的 instance 和 那个 物理 是 那个 另外 过程 的 patient 和 那个 另外 过程 出现 的 time equal 那个 另外 施事体 和 那个 另外 施事体 接着 那个 施事体 和 那个 物理 是 对于 那个 另外 施事体 的 price 那个 另外 实数 那个 测量单位 和 那个 另外 实数 是 lessThan 那个 实数
No TPTP formula. May not be expressible in strict first order.	TransportDetail.kif 174-182	如果 过程 是 ValetParking 的 instance 和 实体 是 那个 过程 的 patient 和 另一个 过程 是 到达 的 instance 和 那个 实体 是 那个 另外 过程 的 patient， 然后 那个 另外 过程 出现 的 time 的结束 接着 那个 过程 出现 的 time 的开始
No TPTP formula. May not be expressible in strict first order.	Merge.kif 8770-8775	如果 时距 是 整数 year 的 instance 和 另一个 时距 是 另一个 整数 year 的 instance 和 (那个 另外 整数 和 那个 整数) equal 1， 然后 那个 时距 接着 那个 另外 时距
No TPTP formula. May not be expressible in strict first order.	FinancialOntology.kif 104-118	如果 校验 的价值 是 货币测量 和 金融账户 是 那个 校验 的 check 帐户 和 过程 是 处理检查 的 instance 和 那个 校验 是 那个 过程 的 patient 和 那个 过程 出现 的 time equal 那个 过程Time， 然后 有存在 金融交易 和 那个 金融交易Time 这样 那个 金融交易 是 退出 的 instance 和 那个 校验 是导致 那个 金融交易 的 instrument 和 那个 金融交易 出现 的 time equal 那个 金融交易Time 和 那个 过程Time 接着 那个 金融交易Time 和 那个 货币测量 是 那个 金融交易 的 transaction 总额 和 那个 金融账户 是 那个 金融交易 的源头
No TPTP formula. May not be expressible in strict first order.	FinancialOntology.kif 120-135	如果 客体 的价值 是 货币测量 和 过程 是 处理检查 的 instance 和 那个 客体 是 那个 过程 的 patient 和 那个 过程 在 金融账户 的 currency 结束 和 那个 金融账户 是 金融账户 的 instance 和 那个 过程 出现 的 time equal 那个 过程Time， 然后 有存在 金融交易 和 那个 金融交易Time 这样 那个 金融交易 是 存款 的 instance 和 那个 客体 是导致 那个 金融交易 的 instrument 和 那个 金融交易 出现 的 time equal 那个 金融交易Time 和 那个 过程Time 接着 那个 金融交易Time 和 那个 货币测量 是 那个 金融交易 的 transaction 总额 和 那个 金融交易 在 那个 金融账户 的 currency 结束
No TPTP formula. May not be expressible in strict first order.	QoSontology.kif 427-438	如果 电脑程序 是 关机块 的 shutdown 和 电脑程序 是 电脑程序 的 instance 和 那个 关机块 是 那个 电脑程序 的执行 program 和 那个 电脑程序 出现 的 time equal 时距， 然后 有存在 另一个 电脑程序 和 另一个 时距 这样 那个 另外 电脑程序 是 电脑程序 的 instance 和 那个 电脑程序 是 那个 另外 电脑程序 的执行 program 和 那个 另外 电脑程序 出现 的 time equal 那个 另外 时距 和 那个 另外 时距 接着 那个 时距
No TPTP formula. May not be expressible in strict first order.	QoSontology.kif 387-398	如果 电脑程序 是 启动块 的 startup 和 电脑程序 是 电脑程序 的 instance 和 那个 启动块 是 那个 电脑程序 的执行 program 和 那个 电脑程序 出现 的 time equal 时距， 然后 有存在 另一个 电脑程序 和 另一个 时距 这样 那个 另外 电脑程序 是 电脑程序 的 instance 和 那个 电脑程序 是 那个 另外 电脑程序 的执行 program 和 那个 另外 电脑程序 出现 的 time equal 那个 另外 时距 和 那个 时距 接着 那个 另外 时距
No TPTP formula. May not be expressible in strict first order.	Merge.kif 8361-8365	如果 时距 的结束 equal 另一个 时距 的开始， 然后 那个 时距 接着 那个 另外 时距
No TPTP formula. May not be expressible in strict first order.	Merge.kif 9417-9429	如果 分拆 时距 为 的 那个 时距TYPE equal 第三 有点 时距， 然后 对所有 第四 时距 和 第五 时距 如果 那个 第四 时距 是 第三 有点 时距 的 instance 和 那个 第五 时距 是 那个 第三 有点 时距 的 instance 和 那个 第四 时距 不 equal 那个 第五 时距， 然后 那个 第四 时距 接着 那个 第五 时距 或 那个 第五 时距 接着 那个 第四 时距 或 那个 第四 时距 比那个 第五 时距发生的earlier 或 那个 第五 时距 比那个 第四 时距发生的earlier
No TPTP formula. May not be expressible in strict first order.	Merge.kif 9445-9455	如果 分拆 时距 为 的 那个 时距TYPE equal 第三 有点 时距， 然后 对所有 第四 时距 如果 那个 第四 时距 是 第三 有点 时距 的 instance 和 那个 第四 时距 不 finishes了才到 那个 时距， 然后 有存在 第五 时距 这样 那个 第五 时距 是 那个 第三 有点 时距 的 instance 和 那个 第四 时距 接着 那个 第五 时距
No TPTP formula. May not be expressible in strict first order.	Merge.kif 9457-9467	如果 分拆 时距 为 的 那个 时距TYPE equal 第三 有点 时距， 然后 对所有 第四 时距 如果 那个 第四 时距 是 第三 有点 时距 的 instance 和 那个 第四 时距 不 starts了才到 那个 时距 ， 然后 有存在 第五 时距 这样 那个 第五 时距 是 那个 第三 有点 时距 的 instance 和 那个 第五 时距 接着 那个 第四 时距
No TPTP formula. May not be expressible in strict first order.	Medicine.kif 6128-6137	如果 BoneFracture 是 客体 的 attribute 在 时距 holdsDuring， 然后 有存在 过程 和 另一个 客体 这样 那个 过程 是 分开 的 instance 和 那个 另外 客体 是 那个 过程 的 patient 和 那个 另外 客体 是 骨骼 的 instance 和 那个 另外 客体 是 那个 客体 的 part 和 那个 过程 出现 的 time 接着 那个 时距
No TPTP formula. May not be expressible in strict first order.	Medicine.kif 6036-6043	如果 BurnInjury 是 客体 的 attribute 在 时距 holdsDuring， 然后 有存在 物理 这样 那个 物理 是 燃烧 的 instance 和 那个 物理 是 located 在 那个 客体 和 那个 物理 出现 的 time 接着 那个 时距
No TPTP formula. May not be expressible in strict first order.	Mid-level-ontology.kif 16410-16426	如果 Dizzy 是 实体 的 attribute 在 时间位置 holdsDuring， 然后 那个 实体 believes 如果 有存在 那个 时间位置2 这样 那个 时间位置2 在 那个 时间位置 时段内发生 和 站立 是 那个 实体 的 attribute 在 那个 时间位置2 holdsDuring， 然后 有存在 第三 实体 这样 那个 第三 实体 是 落下 的 instance 和 那个 实体 经历了 那个 第三 实体 和 那个 时间位置2 接着 那个 第三 实体 出现 的 time 在 那个 时间位置 holdsDuring
No TPTP formula. May not be expressible in strict first order.	Mid-level-ontology.kif 19201-19206	如果 时距 是 秋季 的 instance， 然后 有存在 另一个 时距 这样 那个 另外 时距 是 夏季 的 instance 和 那个 另外 时距 接着 那个 时距
No TPTP formula. May not be expressible in strict first order.	Mid-level-ontology.kif 19208-19213	如果 时距 是 秋季 的 instance， 然后 有存在 另一个 时距 这样 那个 另外 时距 是 冬季 的 instance 和 那个 时距 接着 那个 另外 时距
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