No TPTP formula. May not be expressible in strict first order.	Merge.kif 16493-16501	If an organism is a parent of another organism and the organism is a parent of a third organism and a fourth organism is a parent of the other organism and the fourth organism is a parent of the third organism and the other organism is not equal to the third organism and the organism is not equal to the fourth organism, then the other organism is a sibling of the third organism
No TPTP formula. May not be expressible in strict first order.	Merge.kif 942-947	If an object is a part of another object and the other object is not a part of the object, then the object is a proper part of the other object
No TPTP formula. May not be expressible in strict first order.	Merge.kif 606-612	If a class is exhaustively partitioned into another class and a third class and an entity is an instance of the class and the entity is not an instance of the other class, then the entity is an instance of the third class
No TPTP formula. May not be expressible in strict first order.	Merge.kif 11104-11114	If an object is path along which a motion occurs and the motion originates at another object and the motion ends up at a third object and the length of the object is a real number an unit of measure(s) and the distance between the other object and the third object is another real number the unit of measure(s) and the real number is not greater than the other real number and a fourth object is a part of the object, then the fourth object is between the other object and the third object
No TPTP formula. May not be expressible in strict first order.	Merge.kif 12826-12832	If a physical is a patient of a process and the physical exists during the end of the time of existence of the process and the physical doesn't exist during the beginning of the time of existence of the process, then the process is an instance of creation
No TPTP formula. May not be expressible in strict first order.	Mid-level-ontology.kif 1280-1287	If one end of an object is another object and one end of the object is a third object and the other object is not equal to the third object, then the other object doesn't meet the third object
No TPTP formula. May not be expressible in strict first order.	Mid-level-ontology.kif 1271-1278	If one end of an object is another object and one end of the object is a third object and the other object is not equal to the third object, then the other object and the third object doesn't overlapsSpatially
No TPTP formula. May not be expressible in strict first order.	Mid-level-ontology.kif 1295-1315	If one end of an object is another object and one end of the object is a third object and a fourth object is a part of the other object and a fifth object is a part of the third object and an unit of measure is an instance of unit of length and the distance between the fourth object and the fifth object is a real number the unit of measure(s) and the other object is not equal to the third object, then there don't exist the objectP1, the objectP2 and another real number such that the objectP1 is not a part of the other object and the objectP2 is not a part of the third object and the distance between the objectP1 and the objectP2 is the other real number the unit of measure(s) and the other real number is greater than the real number
No TPTP formula. May not be expressible in strict first order.	Merge.kif 17969-17984	If one end of an object is another object and one end of the object is a third object and the other object is not equal to the third object and the distance between the other object and the third object is a real number an unit of measure(s), then there don't exist the objectP1, the objectP2 and another real number such that one end of the object is the objectP1 and one end of the object is the objectP2 and the objectP1 is not equal to the objectP2 and the distance between the objectP1 and the objectP2 is the other real number the unit of measure(s) and the other real number is greater than the real number
No TPTP formula. May not be expressible in strict first order.	Mid-level-ontology.kif 14148-14162	If an agreement the attribute contract and the agreement is a party to agreement of a cognitive agent and the agreement is a party to agreement of another cognitive agent and a process is an instance of intentional process and the cognitive agent is an agent of the process and the process expresses the content of a proposition and the agreement is not a consistent of the proposition, then the statement there exists an entity such that the entity is an instance of legal action and the other cognitive agent is the plaintiff in the entity and the cognitive agent is the defendant in the entity has the modal force of possibility
No TPTP formula. May not be expressible in strict first order.	Merge.kif 17928-17953	If the relative angle between an object and another object is a real number and one end of the object is a third object and one end of the object is a fourth object and the third object is not equal to the fourth object and the length of the object is the real number1 an unit of measure(s) and the length of the other object is the real number2 the unit of measure(s) and the distance between the third object and a fifth object is the real number3 the unit of measure(s) and one end of the other object is the fifth object and one end of the other object is a sixth object and the fifth object is not equal to the sixth object and the third object doesn't meet the fifth object, then the real number is equal to the arccosine of ((the real number3 and the real number3 and the real number1 and the real number1) and the real number2 and the real number2) and 2.0 and the real number1 and the real number2
No TPTP formula. May not be expressible in strict first order.	Merge.kif 9767-9773	If a side of a self connected object is another self connected object and an object is a part of the self connected object and the object is not connected to the other self connected object, then there exists a positional attribute such that the other self connected object is the positional attribute to the object
No TPTP formula. May not be expressible in strict first order.	Merge.kif 15188-15209	If a class is a subclass of tissue and another class is a subclass of tissue and an object is an instance of the class and another object is an instance of the other class and a third object is an instance of human and the object is a part of the third object and the other object is a part of the third object and the class is not equal to the other class and the class is not a subclass of the other class and the other class is not a subclass of the class and the object is adjacent to the other object, then the statement there exists an entity such that the entity is an instance of connective tissue and the entity is between the object and the other object has the modal force of likely
No TPTP formula. May not be expressible in strict first order.	Media.kif 3268-3273	If the title of an entity in a language is a symbolic string and the original title of the entity in another language is another symbolic string and the language is not equal to the other language, then the title of the entity translated into the language is the symbolic string
No TPTP formula. May not be expressible in strict first order.	Merge.kif 9752-9757	If the top of a self connected object is another self connected object and an object is a part of the self connected object and the object is not connected to the other self connected object, then the object is below to the other self connected object
No TPTP formula. May not be expressible in strict first order.	Mid-level-ontology.kif 22831-22848	If a kind of process is a typical action of a a kind of agent and an entity is an instance of a kind of agent and a real number is equal to the probability of there exists another entity such that the other entity is an instance of a kind of process and the entity is an agent of the other entity and another real number is equal to the probability of there doesn't exist a third entity such that the third entity is an instance of the kind of process and the entity is an agent of the third entity, then the real number is greater than the other real number
No TPTP formula. May not be expressible in strict first order.	Medicine.kif 5933-5944	If the typical volume of blood of a a kind of mammal is a real number an unit of measure(s) and a kind of mammalI is an instance of the kind of mammal and disease or syndrome is not an attribute of another entity and the other entity has the real number2 the unit of measure(s) of blood holds during a time position, then the approximate value of the real number2 is the real number
No TPTP formula. May not be expressible in strict first order.	Mid-level-ontology.kif 23639-23656	If a a kind of object is typically a part of a another kind of object and an entity is an instance of a kind of object and the kind of objectPROB is equal to the probability of there exists another entity such that the other entity is an instance of another kind of object and the entity is a part of the other entity and another real number is equal to the probability of there doesn't exist a third entity such that the third entity is an instance of the other kind of object and the entity is a part of the third entity, then the kind of objectPROB is greater than the other real number
No TPTP formula. May not be expressible in strict first order.	Cars.kif 1453-1470	If a a kind of process is typically a part of a another kind of process and an entity is an instance of a kind of process and the kind of processPROB is equal to the probability of there exists another entity such that the other entity is an instance of another kind of process and the entity is a part of the other entity and another real number is equal to the probability of there doesn't exist a third entity such that the third entity is an instance of the other kind of process and the entity is a part of the third entity, then the kind of processPROB is greater than the other real number
No TPTP formula. May not be expressible in strict first order.	Mid-level-ontology.kif 23676-23693	If a a kind of object typically has a part another kind of object and an entity is an instance of a kind of object and another kind of objectPROB is equal to the probability of there exists another entity such that the other entity is an instance of the other kind of object and the other entity is a part of the entity and another real number is equal to the probability of there doesn't exist a third entity such that the third entity is an instance of the other kind of object and the third entity is a part of the entity, then the other kind of objectPROB is greater than the other real number
No TPTP formula. May not be expressible in strict first order.	Cars.kif 1493-1510	If a a kind of process typically contains a another kind of process and an entity is an instance of a kind of process and another kind of processPROB is equal to the probability of there exists another entity such that the other entity is an instance of the other kind of process and the other entity is a part of the entity and another real number is equal to the probability of there doesn't exist a third entity such that the third entity is an instance of the other kind of process and the third entity is a part of the entity, then the other kind of processPROB is greater than the other real number
No TPTP formula. May not be expressible in strict first order.	Mid-level-ontology.kif 24644-24654	If the unit number of a postal place is a symbolic string and there doesn't exist another symbolic string such that the other symbolic string is the floor of the postal place, then there exists a physical such that the physical is an instance of room and the physical has name the symbolic string and the physical is located at the postal place
No TPTP formula. May not be expressible in strict first order.	Mid-level-ontology.kif 26068-26079	If an entity is a member of public and another entity is a member of public and the entity is not equal to the other entity holds during a time position, then there exists a third entity such that the entity desires the third entity and the other entity desires the third entity holds during the time position
No TPTP formula. May not be expressible in strict first order.	Merge.kif 3895-3899	If a formula holds during a time position, then the formula doesn't hold during the time position

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