Sigma KB Term Intersection

No TPTP formula. May not be expressible in strict first order.	Mid-level-ontology.kif 24235-24245	If a day is a birthdate of a human and the day is an instance of the day a positive integer, then there exist another kind of day and an integer such that the human's birthday is another kind of day and the other kind of day is a subclass of day and the integer is an instance of integer and the other kind of day is equal to the day the positive integer and the integer is greater than another integer
No TPTP formula. May not be expressible in strict first order.	Mid-level-ontology.kif 24194-24205	If a physical is an instance of wedding and date of the physical is a day and the day is an instance of the day a positive integer, then there exist another kind of day and an integer such that weddingAnniversary the physical and another kind of day and the other kind of day is a subclass of day and the integer is an instance of integer and the other kind of day is equal to the day the positive integer and the integer is greater than another integer
No TPTP formula. May not be expressible in strict first order.	Merge.kif 9252-9252	Day is a subclass of time interval
No TPTP formula. May not be expressible in strict first order.	Merge.kif 9262-9262	Monday is a subclass of day
No TPTP formula. May not be expressible in strict first order.	Merge.kif 9265-9265	Tuesday is a subclass of day
No TPTP formula. May not be expressible in strict first order.	Merge.kif 9278-9278	Wednesday is a subclass of day
No TPTP formula. May not be expressible in strict first order.	Merge.kif 9291-9291	Thursday is a subclass of day
No TPTP formula. May not be expressible in strict first order.	Merge.kif 9304-9304	Friday is a subclass of day
No TPTP formula. May not be expressible in strict first order.	Merge.kif 9317-9317	Saturday is a subclass of day
No TPTP formula. May not be expressible in strict first order.	Merge.kif 9330-9330	Sunday is a subclass of day
No TPTP formula. May not be expressible in strict first order.	Media.kif 335-335	Christmas day is a subclass of day

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