Sigma KB Term Intersection

No TPTP formula. May not be expressible in strict first order.	Mid-level-ontology.kif 24236-24246	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 24195-24206	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 9230-9230	Day is a subclass of time interval
No TPTP formula. May not be expressible in strict first order.	Merge.kif 9240-9240	Monday is a subclass of day
No TPTP formula. May not be expressible in strict first order.	Merge.kif 9243-9243	Tuesday is a subclass of day
No TPTP formula. May not be expressible in strict first order.	Merge.kif 9256-9256	Wednesday is a subclass of day
No TPTP formula. May not be expressible in strict first order.	Merge.kif 9269-9269	Thursday is a subclass of day
No TPTP formula. May not be expressible in strict first order.	Merge.kif 9282-9282	Friday is a subclass of day
No TPTP formula. May not be expressible in strict first order.	Merge.kif 9295-9295	Saturday is a subclass of day
No TPTP formula. May not be expressible in strict first order.	Merge.kif 9308-9308	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