| appearance as argument number 1 |
|
| No TPTP formula. May not be expressible in strict first order. | chinese_format.kif 1504-1506 | |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 459-462 | |
| No TPTP formula. May not be expressible in strict first order. | japanese_format.kif 68-70 | |
| No TPTP formula. May not be expressible in strict first order. | spanish_format.kif 78-81 | |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 457-457 | O argumento numero 1 de contraryAttribute e' uma instancia de Atributo |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 455-455 | contraryAttribute e' uma instancia de Predicado |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 456-456 | contraryAttribute e' uma instancia de Relacao de aridade variavel |
| appearance as argument number 2 |
|
|
| No TPTP formula. May not be expressible in strict first order. | chinese_format.kif 283-283 | |
| No TPTP formula. May not be expressible in strict first order. | english_format.kif 288-288 | |
| No TPTP formula. May not be expressible in strict first order. | french_format.kif 164-164 | |
| No TPTP formula. May not be expressible in strict first order. | relations-it.txt 58-58 | |
| No TPTP formula. May not be expressible in strict first order. | japanese_format.kif 1984-1984 | |
| No TPTP formula. May not be expressible in strict first order. | portuguese_format.kif 116-116 | |
| No TPTP formula. May not be expressible in strict first order. | relations-de.txt 367-367 | |
| No TPTP formula. May not be expressible in strict first order. | relations-hindi.txt 99-99 | |
| No TPTP formula. May not be expressible in strict first order. | relations-ro.kif 184-184 | |
| No TPTP formula. May not be expressible in strict first order. | relations-sv.txt 171-171 | |
| No TPTP formula. May not be expressible in strict first order. | relations-cb.txt 92-92 | |
| No TPTP formula. May not be expressible in strict first order. | chinese_format.kif 284-284 | |
| No TPTP formula. May not be expressible in strict first order. | domainEnglishFormat.kif 17010-17010 | |
| No TPTP formula. May not be expressible in strict first order. | domainEnglishFormat.kif 17009-17009 | |
| No TPTP formula. May not be expressible in strict first order. | domainEnglishFormat.kif 17008-17008 | |
| No TPTP formula. May not be expressible in strict first order. | terms-de.txt 114-114 | |
| No TPTP formula. May not be expressible in strict first order. | relations-tg.txt 133-133 |
| antecedent |
|
|
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 476-484 | |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 470-474 |
|
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 15025-15036 |
|
| No TPTP formula. May not be expressible in strict first order. | ComputerInput.kif 2332-2343 |
|
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 16992-17000 |
|
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 464-468 |
| consequent |
|
|
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 470-474 |
|
| No TPTP formula. May not be expressible in strict first order. | Mid-level-ontology.kif 18170-18172 |
|
| appearance as argument number 0 |
|
|
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 17144-17144 | Above e' &o oposto de Below |
| No TPTP formula. May not be expressible in strict first order. | ComputingBrands.kif 4475-4475 | AccountDeactivated e' &o oposto de AccountActive |
| No TPTP formula. May not be expressible in strict first order. | Food.kif 2803-2803 | AcidicPH e' &o oposto de BasicPH |
| No TPTP formula. May not be expressible in strict first order. | emotion.kif 522-522 | AppraisalAsBeingDisliked e' &o oposto de AppraisalAsBeingLiked |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 13653-13653 | Audible e' &o oposto de Inaudible |
| No TPTP formula. May not be expressible in strict first order. | Government.kif 336-336 | AuthoritarianRegime e' &o oposto de MultipartyDemocracy |
| No TPTP formula. May not be expressible in strict first order. | Transportation.kif 391-391 | BroadGauge e' &o oposto de StandardGauge |
| No TPTP formula. May not be expressible in strict first order. | Mid-level-ontology.kif 22284-22284 | Civilian e' &o oposto de MilitaryPerson |
| No TPTP formula. May not be expressible in strict first order. | Cars.kif 4945-4945 | Clockwise e' &o oposto de CounterClockwise |
| No TPTP formula. May not be expressible in strict first order. | engineering.kif 675-675 | Conductivity e' &o oposto de Resistivity |
| No TPTP formula. May not be expressible in strict first order. | Medicine.kif 435-435 | Conscious e' &o oposto de Inconsciente |
| No TPTP formula. May not be expressible in strict first order. | Mid-level-ontology.kif 1631-1631 | ContainerFull e' &o oposto de ContainerEmpty |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 18172-18172 | Dead e' &o oposto de Living |
| No TPTP formula. May not be expressible in strict first order. | Mid-level-ontology.kif 29489-29489 | DeviceDamaged e' &o oposto de DeviceNormal |
| No TPTP formula. May not be expressible in strict first order. | ComputingBrands.kif 3644-3644 | DeviceOn e' &o oposto de DeviceOff |
| No TPTP formula. May not be expressible in strict first order. | ComputingBrands.kif 3645-3645 | DeviceOpen e' &o oposto de DeviceClosed |
| No TPTP formula. May not be expressible in strict first order. | Mid-level-ontology.kif 25629-25629 | Dirty e' &o oposto de Clean |
| No TPTP formula. May not be expressible in strict first order. | Mid-level-ontology.kif 8683-8683 | Drugged e' &o oposto de Sober |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 18070-18070 | Dry e' &o oposto de Damp |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 18269-18269 | Embryonic e' &o oposto de Larval |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 17056-17056 | False e' &o oposto de True |
| No TPTP formula. May not be expressible in strict first order. | Government.kif 285-285 | FederalGovernment e' &o oposto de AuthoritarianRegime |
| No TPTP formula. May not be expressible in strict first order. | Government.kif 284-284 | FederalGovernment e' &o oposto de UnitaryRule |
| No TPTP formula. May not be expressible in strict first order. | emotion.kif 1849-1849 | FeelingAlert e' &o oposto de FeelingTired |
| No TPTP formula. May not be expressible in strict first order. | emotion.kif 1782-1782 | FeelingAtEase e' &o oposto de FeelingRestless |
| Display limited to 25 items. Show next 25 | ||
| Display limited to 25 items. Show next 25 |
|
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