No TPTP formula. May not be expressible in strict first order.	Cars.kif 3124-3141	If the number of coils in a wire coil is an integer, then there exist a collection and the collection2F such that the collection is an instance of collection and the integer is a member count of the collection and for all an object if the object is a member of the collection, then the collection2F is an attribute of the object and the collection2F is an instance of closed two dimensional figure and the object is a part of the wire coil and there doesn't exist the object2 such that the object2 and the object overlapsSpatially and the object2 is a member of the collection
No TPTP formula. May not be expressible in strict first order.	Merge.kif 10061-10066	If an object completely fills a hole, then for all another object if the other object is connected to the hole, then the other object is connected to the object
No TPTP formula. May not be expressible in strict first order.	Merge.kif 3855-3860	If an object is a copy of another object, then for all an attribute if the attribute is an attribute of the object, then the attribute is an attribute of the other object
No TPTP formula. May not be expressible in strict first order.	Music.kif 243-249	If a human has discography a discography, then for all a music recording if the music recording is a member of the discography, then there exists a kind of making music such that the human performed the music recording
No TPTP formula. May not be expressible in strict first order.	Merge.kif 2950-2955	If a class is disjointly decomposed into @ROW, then for all a third class if the third class is a member of (@ROW), then the third class is a subclass of the class
No TPTP formula. May not be expressible in strict first order.	Merge.kif 2957-2966	If a class is disjointly decomposed into @ROW, then for all a third class and a fourth class if the third class is a member of (@ROW) and the fourth class is a member of (@ROW) and the third class is not equal to the fourth class, then the third class is disjoint from the fourth class
No TPTP formula. May not be expressible in strict first order.	Dining.kif 492-505	If an agent requires customers to wear an ambience, then the statement there exist an entity and another entity such that the entity is an instance of outfit and the agent believes the entity is the ambience and for all a third entity and a fourth entity the agent is a customer of the third entity and the third entity located at time the other entity for the agent and the fourth entity is a member of the entity and the third entity wears the fourth entity holds during the other entity has the modal force of obligation
No TPTP formula. May not be expressible in strict first order.	Merge.kif 8020-8027	If the beginning of a time interval is equal to a time point, then for all another time point if the other time point is a part of the time interval and the other time point is not equal to the time point, then the time point happens before the other time point
No TPTP formula. May not be expressible in strict first order.	Merge.kif 8038-8045	If the end of a time interval is equal to a time point, then for all another time point if the other time point is a part of the time interval and the other time point is not equal to the time point, then the other time point happens before the time point
No TPTP formula. May not be expressible in strict first order.	Merge.kif 16313-16321	If the immediate family of a human is equal to a family group, then for all an organism if the organism is a member of the family group, then there exists another organism such that the other organism is a parent of the organism or the organism is a parent of the other organism
No TPTP formula. May not be expressible in strict first order.	Merge.kif 6091-6097	If the set of minimal paths that partition a graph into two separate graphs is equal to a kind of graph path, then there exists a positive integer such that for all another graph path if the other graph path is an instance of a kind of graph path, then the length of the other graph path is the positive integer
No TPTP formula. May not be expressible in strict first order.	Merge.kif 9469-9479	If decomposition of a time interval into the time intervalTYPEs is equal to another kind of time interval, then for all a time position if the time position is an instance of time point and the time position is a part of the time interval, then there exists another time position such that the other time position is an instance of another kind of time interval and the time position is a part of the other time position
No TPTP formula. May not be expressible in strict first order.	Merge.kif 9417-9429	If decomposition of a time interval into the time intervalTYPEs is equal to another kind of time interval, then for all a third time interval and a fourth time interval if the third time interval is an instance of another kind of time interval and the fourth time interval is an instance of the other kind of time interval and the third time interval is not equal to the fourth time interval, then the third time interval meets the fourth time interval or the fourth time interval meets the third time interval or the third time interval happens earlier than the fourth time interval or the fourth time interval happens earlier than the third time interval
No TPTP formula. May not be expressible in strict first order.	Merge.kif 9405-9415	If decomposition of a time interval into the time intervalTYPEs is equal to another kind of time interval, then for all a third time interval and a fourth time interval if the third time interval is an instance of the time intervalTYPE and the fourth time interval is an instance of another kind of time interval, then there exists a time duration such that duration of the third time interval is the time duration and duration of the fourth time interval is the time duration
No TPTP formula. May not be expressible in strict first order.	Merge.kif 9445-9455	If decomposition of a time interval into the time intervalTYPEs is equal to another kind of time interval, then for all a third time interval if the third time interval is an instance of another kind of time interval and the third time interval doesn't finish the time interval, then there exists a fourth time interval such that the fourth time interval is an instance of the other kind of time interval and the third time interval meets the fourth time interval
No TPTP formula. May not be expressible in strict first order.	Merge.kif 9457-9467	If decomposition of a time interval into the time intervalTYPEs is equal to another kind of time interval, then for all a third time interval if the third time interval is an instance of another kind of time interval and the third time interval doesn't start the time interval, then there exists a fourth time interval such that the fourth time interval is an instance of the other kind of time interval and the fourth time interval meets the third time interval
No TPTP formula. May not be expressible in strict first order.	Merge.kif 267-272	If an attribute is equal to another attribute, then for all an entity the entity the attribute the attribute if and only if the entity the attribute the other attribute
No TPTP formula. May not be expressible in strict first order.	Merge.kif 281-286	If a class is equal to another class, then for all an entity the entity is an instance of the class if and only if the entity is an instance of the other class
No TPTP formula. May not be expressible in strict first order.	Merge.kif 9859-9868	If an object is equal to the difference between the parts of another object and a third object, then for all a fourth object the fourth object is a proper part of the object if and only if the fourth object is a proper part of the other object and the fourth object is not a proper part of the third object
No TPTP formula. May not be expressible in strict first order.	Merge.kif 9839-9846	If an object is equal to the intersection of the parts of another object and a third object, then for all a fourth object the fourth object is a part of the object if and only if the fourth object is a part of the other object and the fourth object is a part of the third object
No TPTP formula. May not be expressible in strict first order.	Merge.kif 9818-9825	If an object is equal to the union of the parts of another object and a third object, then for all a fourth object the fourth object is a part of the object if and only if the fourth object is a part of the other object or the fourth object is a part of the third object
No TPTP formula. May not be expressible in strict first order.	Merge.kif 260-265	If an entity is equal to another entity, then for all an attribute the entity the attribute the attribute if and only if the other entity the attribute the attribute
No TPTP formula. May not be expressible in strict first order.	Merge.kif 274-279	If an entity is equal to another entity, then for all a class the entity is an instance of the class if and only if the other entity is an instance of the class
No TPTP formula. May not be expressible in strict first order.	Merge.kif 4127-4132	If a process is located at an object, then for all another process if the other process is a subprocess of the process, then the other process is located at the object
No TPTP formula. May not be expressible in strict first order.	Merge.kif 509-517	If @ROW are all the attributes of another kind of attribute, then for all an entity if the entity is an instance of another kind of attribute, then there exists another entity such that the other entity is a member of (@ROW) and the entity is equal to the other entity
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