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 3392-3396	If a function is an instance of sequence function and the range of the function is an instance of a class, then the class is a subclass of integer
No TPTP formula. May not be expressible in strict first order.	Merge.kif 1954-1954	Integer is a subclass of rational number
No TPTP formula. May not be expressible in strict first order.	Merge.kif 1960-1960	Even integer is a subclass of integer
No TPTP formula. May not be expressible in strict first order.	Merge.kif 1965-1965	Odd integer is a subclass of integer
No TPTP formula. May not be expressible in strict first order.	Merge.kif 1970-1970	Prime number is a subclass of integer
No TPTP formula. May not be expressible in strict first order.	Merge.kif 1975-1975	Nonnegative integer is a subclass of integer
No TPTP formula. May not be expressible in strict first order.	Merge.kif 1985-1985	Negative integer is a subclass of integer

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