No TPTP formula. May not be expressible in strict first order.	UXExperimentalTerms.kif 1496-1518	If a time interval is an instance of the time interval_CLASS and the time interval_CLASS is a subclass of process and an accessing web page is an instance of accessing web page and an agent is an instance of agent and the agent is an agent of the time interval and the agent is an agent of the accessing web page and the time interval takes place during the accessing web page and a physical is an instance of time interval and there doesn't exist the time interval2 such that the time interval2 is an instance of the time interval_CLASS and the agent is an agent of the time interval2 and the time interval2 takes place during the accessing web page and the beginning of the time of existence of the time interval2 happens before the beginning of the time of existence of the time interval and the beginning of the time of existence of the accessing web page is equal to the beginning of the time of existence of the physical and the beginning of the time of existence of the time interval is equal to the end of the time of existence of the physical, then the time of the accessing web page in the class the time interval_CLASS is equal to the physical
No TPTP formula. May not be expressible in strict first order.	Mid-level-ontology.kif 19565-19577	If a process is an instance of chemical reduction and an entity is a patient of the process and a real number is an electron number of the entity holds during the beginning of the time of existence of the process, then there exists another real number such that the other real number is greater than the real number and the other real number is an electron number of the entity holds during the end of the time of existence of the process
No TPTP formula. May not be expressible in strict first order.	Mid-level-ontology.kif 17517-17522	If a process is an instance of reversing and an entity is a patient of the process and the top of the entity is another entity and the bottom of the entity is a third entity holds during the beginning of the time of existence of the process, then the top of the entity is the third entity and the bottom of the entity is the other entity holds during the end of the time of existence of the process
No TPTP formula. May not be expressible in strict first order.	Merge.kif 8262-8267	If a time interval is an instance of time interval and a time point is equal to the beginning of the time interval and another time point is equal to the end of the time interval, then the time point happens before the other time point
No TPTP formula. May not be expressible in strict first order.	Merge.kif 8269-8279	If a time interval is an instance of time interval and another time interval is an instance of time interval and the beginning of the other time interval happens before or at the beginning of the time interval and the beginning of the time interval happens before the end of the other time interval, then the time interval overlaps the other time interval
No TPTP formula. May not be expressible in strict first order.	Merge.kif 8690-8697	If a time interval is an instance of the year an integer and another time interval is an instance of the year another integer and a time point is equal to the beginning of the time interval and another time point is equal to the beginning of the other time interval and the other integer is greater than the integer, then the time point happens before the other time point
No TPTP formula. May not be expressible in strict first order.	Anatomy.kif 1758-1780	If the insertion point of a kind of muscle is a kind of body part and an object is an instance of human and standard anatomical position is an attribute of the object holds during a time interval and healthy is an attribute of the object and another time interval is an instance of muscular contraction and the time of existence of the other time interval takes place during the time interval and another object is an instance of a kind of muscle and the other object is a part of the object and the other object is an instrument for the other time interval and one end of the other object is a third object and the third object meets a fourth object and the third object is located at an entity holds during the beginning of the other time interval, then the third object is not located at the entity holds during the end of the other time interval
No TPTP formula. May not be expressible in strict first order.	Anatomy.kif 1708-1729	If the origin of a kind of muscle is a kind of body part and an object is an instance of human and standard anatomical position is an attribute of the object holds during a time interval and healthy is an attribute of the object and another time interval is an instance of muscular contraction and the time of existence of the other time interval takes place during the time interval and another object is an instance of a kind of muscle and the other object is a part of the object and the other object is an instrument for the other time interval and one end of the other object is a third object and the third object meets a fourth object and the third object is located at an entity holds during the beginning of the other time interval, then the third object is located at the entity holds during the end of the other time interval
No TPTP formula. May not be expressible in strict first order.	Merge.kif 12804-12810	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.	FinancialOntology.kif 2669-2685	If an agreement the attribute option and a cognitive agent holds the agreement and a currency measure is a strike price of the agreement and the agreement has expiration a time interval and a financial instrument is price the currency measure for an agent and the agent is an instance of time interval and the end of the agent happens before the beginning of the time interval and the financial instrument is an underlier of the agreement, then the cognitive agent has the right to perform the class described by a symbolic string
No TPTP formula. May not be expressible in strict first order.	FinancialOntology.kif 2623-2639	If an agreement the attribute option and a cognitive agent holds the agreement and a currency measure is a strike price of the agreement and the agreement has expiration a time interval and a financial instrument is an underlier of the agreement and the financial instrument is price the currency measure for an agent and the agent is an instance of time interval and the end of the agent happens before the beginning of the time interval, then the cognitive agent has the right to perform the class described by a symbolic string
No TPTP formula. May not be expressible in strict first order.	FinancialOntology.kif 2687-2703	If an agreement the attribute option and a cognitive agent sells the agreement and a currency measure is a strike price of the agreement and the agreement has expiration a time interval and a financial instrument is price the currency measure for an agent and the agent is an instance of time interval and the end of the agent happens before the beginning of the time interval and the financial instrument is an underlier of the agreement, then the cognitive agent is obliged to perform tasks of type the class described by a symbolic string
No TPTP formula. May not be expressible in strict first order.	FinancialOntology.kif 2641-2659	If an agreement the attribute option and a cognitive agent sells the agreement and a currency measure is a strike price of the agreement and the agreement has expiration a time interval and a financial instrument is an underlier of the agreement and the financial instrument is price the currency measure for an agent and the agent is an instance of time interval and the end of the agent happens before the beginning of the time interval, then the cognitive agent is obliged to perform tasks of type the class described by a symbolic string
No TPTP formula. May not be expressible in strict first order.	Merge.kif 8025-8030	If an object is a resource for a process and the measure of the object is a real number holds during the beginning of the time of existence of the process and the measure of the object is another real number holds during the end of the time of existence of the process, then the real number is greater than the other real number
No TPTP formula. May not be expressible in strict first order.	FinancialOntology.kif 834-842	If a currency measure is a transaction amount of a financial transaction and date of the financial transaction is a day and a financial account is an instance of financial account and the financial transaction ends up at the currency of the financial account and the financial account amount due the currency measure for a time interval and the end of the day happens before the beginning of the time interval, then the financial transaction is an instance of prepayment
No TPTP formula. May not be expressible in strict first order.	Merge.kif 8382-8384	If the end of a time interval happens before the beginning of another time interval, then the time interval happens earlier than the other time interval
No TPTP formula. May not be expressible in strict first order.	Merge.kif 7998-8005	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 8339-8343	If the end of a time interval is equal to the beginning of another time interval, then the time interval meets the other time interval
No TPTP formula. May not be expressible in strict first order.	QoSontology.kif 1270-1284	If there exist a time interval and another time interval such that a time duration is a dependency delay of a computer program and shutdown block is a dependency type of the computer program and another computer program has a dependency on the computer program and a computer process is an instance of computer process and the computer program is a program running of the computer process and another computer process is an instance of computer process and the other computer program is a program running of the other computer process and the time of existence of the other computer process is equal to the other time interval and a third time interval finishes the time interval and the time of existence of the other computer process is equal to the other time interval and the beginning of the third time interval is equal to the end of the other time interval, then duration of the third time interval is the time duration
No TPTP formula. May not be expressible in strict first order.	QoSontology.kif 1254-1268	If there exist a time interval and another time interval such that a time duration is a dependency delay of a computer program and startup block is a dependency type of the computer program and another computer program has a dependency on the computer program and a computer process is an instance of computer process and the computer program is a program running of the computer process and another computer process is an instance of computer process and the other computer program is a program running of the other computer process and the time of existence of the other computer process is equal to the other time interval and the other time interval starts a third time interval and the time of existence of the computer process is equal to the time interval and the end of the third time interval is equal to the beginning of the time interval, then duration of the third time interval is the time duration
No TPTP formula. May not be expressible in strict first order.	Merge.kif 8212-8221	If a time point is between or at the beginning of the time of existence of a physical and the end of the time of existence of the physical, then the physical exists during the time point and the time point is an instance of time point

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