Sigma KB Term Intersection

No TPTP formula. May not be expressible in strict first order.	Mid-level-ontology.kif 30030-30060	如果过程是 BreakingRecord 的 instance 和施事体是那个过程的 agent，然后有存在集合，类,，，另一个过程,，，时点,，，格角色,，，客体， and 和实体这样那个集合是集合的 instance 和那个施事体是那个集合的 element 和那个类是过程的 subclass 和那个客体是地区的 instance 和那个时点是时点的 instance 和那个实体是数量的 instance 和那个另外过程是那个类的 instance 和那个过程提到那个实体和那个实体提到那个另外过程和那个施事体对于那个另外过程在事件那个格角色 plays 角色和那个另外过程是 located 在那个客体和不存在另一个实体和第三实体这样那个另外实体是那个集合的 instance 和那个另外实体不 equal 那个施事体和那个第三实体是那个类的 instance 和那个另外实体对于那个第三实体在事件那个格角色 plays 角色和那个第三实体是 located 在那个客体在那个时点和那个过程出现的 time 的结束间的时段 holdsDuring
No TPTP formula. May not be expressible in strict first order.	Merge.kif 12014-12026	如果过程是决定的 instance 和有认知的主事是那个过程的 agent 和集合是集合的 instance 和那个集合是那个过程的 patient 和实体是那个集合的 element，然后那个有认知的主事 believes 有存在另一个实体这样那个实体是那个另外实体的 instance 和那个另外实体是有意图过程的 subclass 和那个有认知的主事能够担当主事的角色做那个另外实体
No TPTP formula. May not be expressible in strict first order.	Merge.kif 2148-2148	集合是集或类的 subclass
No TPTP formula. May not be expressible in strict first order.	Merge.kif 5516-5516	空集是集合的 subclass
No TPTP formula. May not be expressible in strict first order.	Merge.kif 5527-5527	非空集是集合的 subclass
No TPTP formula. May not be expressible in strict first order.	Merge.kif 5537-5537	有限集合是集合的 subclass
No TPTP formula. May not be expressible in strict first order.	engineering.kif 205-205	方程组是集合的 subclass

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