  disjointDecomposition
|
|
Sigma KEE - disjointDecomposition
|
appearance as argument number 1
|
|
|
|
appearance as argument number 2
|
|
|
|
antecedent
|
|
|
(=>
(disjointDecomposition @ROW)
(=>
(inList ?ELEMENT
(ListFn @ROW))
(instance ?ELEMENT Class))) |
Merge.kif 566-570 |
Assuming @ROW is disjointly decomposed into @ROW, it follows that: if Y is a member of (@ROW), then Y is an instance of class |
(=>
(and
(exhaustiveDecomposition @ROW)
(disjointDecomposition @ROW))
(partition @ROW)) |
Merge.kif 588-592 |
If @ROW is covered by @ROW and @ROW is disjointly decomposed into @ROW, then @ROW is exhaustively partitioned into @ROW |
(=>
(disjointDecomposition ?CLASS @ROW)
(forall (?ITEM)
(=>
(inList ?ITEM
(ListFn @ROW))
(subclass ?ITEM ?CLASS)))) |
Merge.kif 3061-3066 |
If X is disjointly decomposed into @ROW, then For all Class Z: if Z is a member of (@ROW), then Z is a subclass of X |
(=>
(disjointDecomposition ?CLASS @ROW)
(forall (?ITEM1 ?ITEM2)
(=>
(and
(inList ?ITEM1
(ListFn @ROW))
(inList ?ITEM2
(ListFn @ROW))
(not
(equal ?ITEM1 ?ITEM2)))
(disjoint ?ITEM1 ?ITEM2)))) |
Merge.kif 3068-3077 |
If X is disjointly decomposed into @ROW, then For all Classes Z and W: if Z is a member of (@ROW), W is a member of (@ROW), and equal Z and W, then Z is disjoint from W |
(=>
(disjointDecomposition ?CLASS ?ROW1 ?ROW2 ?ROW3)
(and
(disjoint ?ROW1 ?ROW2)
(disjoint ?ROW2 ?ROW3)
(disjoint ?ROW3 ?ROW1))) |
Merge.kif 3079-3084 |
If X is disjointly decomposed into Y, Z, and W, then Y is disjoint from Z, Z is disjoint from W, and W is disjoint from Y |
|
consequent
|
|
|
|
appearance as argument number 0
|
|
|
| (disjointDecomposition Language AnimalLanguage HumanLanguage ComputerLanguage) |
Merge.kif 1495-1495 |
Language is disjointly decomposed into animal language, human language, and computer language |
| (disjointDecomposition Abstract Quantity Attribute Relation Proposition List) |
Merge.kif 1763-1763 |
Abstract is disjointly decomposed into quantity, attribute, relation, proposition, and list |
| (disjointDecomposition Relation BinaryRelation TernaryRelation QuaternaryRelation QuintaryRelation VariableArityRelation) |
Merge.kif 2270-2271 |
Relation is disjointly decomposed into binary relation, ternary relation, quaternary relation, quintary relation, and variable arity relation |
| (disjointDecomposition NonFloweringPlant Alga Fern Moss) |
Merge.kif 14722-14722 |
Non flowering plant is disjointly decomposed into alga, fern, and moss |
| (disjointDecomposition Invertebrate Worm Mollusk Arthropod) |
Merge.kif 14816-14816 |
Invertebrate is disjointly decomposed into worm, mollusk, and arthropod |
| (disjointDecomposition Arthropod Arachnid Myriapod Insect Crustacean) |
Merge.kif 14837-14837 |
Arthropod is disjointly decomposed into arachnid, myriapod, insect, and crustacean |
| (disjointDecomposition ColdBloodedVertebrate Amphibian Fish Reptile) |
Merge.kif 14859-14859 |
Cold blooded vertebrate is disjointly decomposed into amphibian, fish, and reptile |
| (disjointDecomposition Mammal AquaticMammal HoofedMammal Marsupial Rodent Primate) |
Merge.kif 14893-14893 |
Mammal is disjointly decomposed into aquatic mammal, hoofed mammal, marsupial, rodent, and primate |
| (disjointDecomposition Primate Ape Monkey Hominid) |
Merge.kif 14939-14939 |
Primate is disjointly decomposed into ape, monkey, and hominid |
| (disjointDecomposition Nutrient Protein Carbohydrate Vitamin) |
Merge.kif 14994-14994 |
Nutrient is disjointly decomposed into protein, carbohydrate, and vitamin |
| (disjointDecomposition Tissue ConnectiveTissue MuscleTissue NervousTissue EpithelialTissue) |
Merge.kif 15421-15421 |
Tissue is disjointly decomposed into connective tissue, muscle tissue, nervous tissue, and epithelial tissue |
| (disjointDecomposition Phrase VerbPhrase NounPhrase PrepositionalPhrase) |
Merge.kif 15594-15594 |
Phrase is disjointly decomposed into verb phrase, noun phrase, and prepositional phrase |
| (disjointDecomposition Residence PermanentResidence TemporaryResidence) |
Merge.kif 16079-16079 |
Residence is disjointly decomposed into permanent residence and temporary residence |
| (disjointDecomposition Expressing ExpressingApproval ExpressingDisapproval) |
Mid-level-ontology.kif 14558-14558 |
Expressing is disjointly decomposed into expressing approval and expressing disapproval |
| (disjointDecomposition Sentence Statement Supposition Question Request Order) |
Mid-level-ontology.kif 15835-15835 |
Sentence is disjointly decomposed into statement, supposition, question, request, and order |
| (disjointDecomposition GameArtifact GameBoard GamePiece) |
Mid-level-ontology.kif 18595-18595 |
Game artifact is disjointly decomposed into game board and game piece |
| (disjointDecomposition PowerGeneration FossilFuelPowerGeneration HydroElectricPowerGeneration NuclearPowerGeneration OtherSourcePowerGeneration) |
Economy.kif 2322-2322 |
Power generation is disjointly decomposed into fossil fuel power generation, hydro electric power generation, nuclear power generation, and other source power generation |
| (disjointDecomposition NSAID Aspirin Ibuprofen Acetaminophen) |
Medicine.kif 3535-3535 |
Non-steriodal anti-inflammatory is disjointly decomposed into aspirin, ibuprofen, and paracetamol |
| (disjointDecomposition EnlistedSoldierRank PrivateRank NonCommissionedOfficerRank) |
Military.kif 544-544 |
Enlisted soldier rank is disjointly decomposed into private rank and non commissioned officer rank |
| (disjointDecomposition CommissionedOfficerRank FlagOfficerRank FieldGradeOfficerRank CompanyGradeRank) |
Military.kif 558-559 |
Commissioned officer rank is disjointly decomposed into flag officer rank, field grade officer rank, and company grade rank |
| (disjointDecomposition NonCommissionedOfficerRank JuniorNCORank SeniorNCORank) |
Military.kif 581-581 |
Non commissioned officer rank is disjointly decomposed into juniorNCO rank and seniorNCO rank |
| (disjointDecomposition LAN BusNetwork StarNetwork RingNetwork) |
QoSontology.kif 32-32 |
LAN is disjointly decomposed into bus network, star network, and ring network |
| (disjointDecomposition DifferentialEquation FirstOrderDifferentialEquation HigherOrderDifferentialEquation) |
engineering.kif 187-187 |
Differential equation is disjointly decomposed into first order differential equation and higher order differential equation |
| (disjointDecomposition DifferentialEquation OrdinaryDifferentialEquation PartialDifferentialEquation) |
engineering.kif 197-197 |
Differential equation is disjointly decomposed into ordinary differential equation and partial differential equation |
|
Show simplified definition (without tree view)
Show simplified definition (with tree view)
|
