| appearance as argument number 1 |
|
| No TPTP formula. May not be expressible in strict first order. | chinese_format.kif 1719-1720 | |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 1759-1760 | |
| No TPTP formula. May not be expressible in strict first order. | japanese_format.kif 324-325 | |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 1756-1756 | The number 1 argument of extension is an instance of attribute |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 1755-1755 | Extension is an instance of partial valued relation |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 1754-1754 | Extension is an instance of unary function |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 1757-1757 | The range of extension is an instance of class |
| appearance as argument number 2 |
|
|
| No TPTP formula. May not be expressible in strict first order. | chinese_format.kif 257-257 | |
| No TPTP formula. May not be expressible in strict first order. | english_format.kif 262-262 | |
| No TPTP formula. May not be expressible in strict first order. | french_format.kif 147-147 | |
| No TPTP formula. May not be expressible in strict first order. | relations-it.txt 106-106 | |
| No TPTP formula. May not be expressible in strict first order. | japanese_format.kif 1975-1975 | |
| No TPTP formula. May not be expressible in strict first order. | portuguese_format.kif 99-99 | |
| No TPTP formula. May not be expressible in strict first order. | relations-de.txt 331-331 | |
| No TPTP formula. May not be expressible in strict first order. | relations-ro.kif 166-166 | |
| No TPTP formula. May not be expressible in strict first order. | relations-sv.txt 153-153 | |
| No TPTP formula. May not be expressible in strict first order. | relations-tg.txt 222-222 | |
| No TPTP formula. May not be expressible in strict first order. | chinese_format.kif 258-258 | |
| No TPTP formula. May not be expressible in strict first order. | domainEnglishFormat.kif 23004-23004 | |
| No TPTP formula. May not be expressible in strict first order. | domainEnglishFormat.kif 23003-23003 | |
| No TPTP formula. May not be expressible in strict first order. | domainEnglishFormat.kif 23002-23002 | |
| No TPTP formula. May not be expressible in strict first order. | terms-de.txt 105-105 | |
| No TPTP formula. May not be expressible in strict first order. | relations-tg.txt 223-223 |
| antecedent |
|
|
| No TPTP formula. May not be expressible in strict first order. | Transportation.kif 1349-1359 | A geographic area is total facility type in area the class corresponding to airport with paved runway for a nonnegative integer if and only if there exist a symbolic string and an entity such that the nonnegative integer is a cardinality of the class described by the symbolic string |
| No TPTP formula. May not be expressible in strict first order. | Transportation.kif 1611-1620 |
|
| No TPTP formula. May not be expressible in strict first order. | Transportation.kif 1361-1368 |
|
| consequent |
|
|
| No TPTP formula. May not be expressible in strict first order. | Transportation.kif 777-783 |
|
| No TPTP formula. May not be expressible in strict first order. | Transportation.kif 2565-2567 |
|
| No TPTP formula. May not be expressible in strict first order. | Transportation.kif 2606-2608 |
|
| statement |
|
|
| No TPTP formula. May not be expressible in strict first order. | Economy.kif 144-144 | 35 is a cardinality of the class corresponding to developed country |
| No TPTP formula. May not be expressible in strict first order. | Economy.kif 613-613 | 126 is a cardinality of the class corresponding to developing country |
| No TPTP formula. May not be expressible in strict first order. | Economy.kif 405-405 | 42 is a cardinality of the class corresponding to least developed country |
| No TPTP formula. May not be expressible in strict first order. | Economy.kif 229-229 | 172 is a cardinality of the class corresponding to less developed country |
| No TPTP formula. May not be expressible in strict first order. | Weather.kif 11-11 | Atmosphere is a subclass of the class corresponding to fluid |
|
Show full definition with tree view
Show simplified definition (without tree view)
Show simplified definition (with tree view)
|
|
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