No TPTP formula. May not be expressible in strict first order.	Economy.kif 490-497	If a time interval is an instance of time interval and upper middle income country is an economy type of a geopolitical area holds during the time interval, then there exists a real number such that the geopolitical area is per capitaGDP in period the real number united states dollar(s) for the time interval and the real number is less than 9267.0
No TPTP formula. May not be expressible in strict first order.	Catalog.kif 139-150	If an agent offers items for sale in a catalog during a time interval and a kind of entity is in the catalog and a kind of entity is a subclass of object and a process is an instance of another kind of process and another kind of process is a subclass of process and another entity is an instance of the kind of entity and the other entity is a patient of the process and the time interval is an instance of another kind of time interval and another kind of time interval is a subclass of time interval, then the agent is capable of being a agent in the other kind of process during the other kind of time interval
No TPTP formula. May not be expressible in strict first order.	Catalog.kif 130-137	If an agent offers items for sale in a catalog during a time interval and a kind of entity is in the catalog and a kind of entity is a subclass of process and the time interval is an instance of another kind of time interval and another kind of time interval is a subclass of time interval, then the agent is capable of being a agent in the kind of entity during the other kind of time interval
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 8132-8134	If a time interval is an instance of time interval, then the beginning of the time interval happens before the end of the time interval
No TPTP formula. May not be expressible in strict first order.	Merge.kif 8521-8523	If a time interval is an instance of time interval, then after the time interval is equal to interval between the end of the time interval and positive infinity
No TPTP formula. May not be expressible in strict first order.	Merge.kif 8490-8492	If a time interval is an instance of time interval, then before the time interval is equal to interval between negative infinity and the beginning of the time interval
No TPTP formula. May not be expressible in strict first order.	Merge.kif 7947-7952	If a time position is an instance of time interval, then there exists another time position such that the other time position is an instance of time point and the other time position is a part of the time position
No TPTP formula. May not be expressible in strict first order.	Merge.kif 8504-8506	If a time position is an instance of time interval, then immediately before the time position finishes before the time position
No TPTP formula. May not be expressible in strict first order.	Merge.kif 8486-8488	If a time interval is an instance of time interval, then before the time interval meets the time interval
No TPTP formula. May not be expressible in strict first order.	Merge.kif 8517-8519	If a time interval is an instance of time interval, then the time interval meets after the time interval
No TPTP formula. May not be expressible in strict first order.	Merge.kif 8535-8537	If a time position is an instance of time interval, then immediately after the time position starts after the time position

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