Browsing Interface : Welcome guest : log in
|
Browsing Interface : Welcome guest : log in |
[
Home |
Graph |
LogLearn |
Editor |
]
KB:
Language:
Formal Language:
|
| part |
| appearance as argument number 1 |
|
| s__instance(s__part,s__SpatialRelation)
|
Merge.kif 921-921 | part is an instance of spatial relation |
| s__instance(s__part,s__PartialOrderingRelation)
|
Merge.kif 922-922 | part is an instance of partial ordering relation |
| s__instance(s__part,s__BinaryPredicate)
|
Merge.kif 923-923 | part is an instance of binary predicate |
| s__domain(s__part,n__1,s__Object)
|
Merge.kif 924-924 | The number 1 argument of part is an instance of object |
| s__domain(s__part,n__2,s__Object)
|
Merge.kif 925-925 | The number 2 argument of part is an instance of object |
| s__documentation(s__part, s__EnglishLanguage, "The basic mereological relation_ All other mereological relations are defined in terms of this one_ (part ?PART ?WHOLE) simply means that the Object ?PART is part of the Object ?WHOLE_ Note that, since part is a ReflexiveRelation, every Object is a part of itself_") | Merge.kif 927-931 | The number 2 argument of part is an instance of object |
| appearance as argument number 2 |
|
|
| antecedent |
|
|
| ! [V__OBJ1,V__OBJ2] : (((s__instance(V__OBJ1,s__Object) & s__instance(V__OBJ2,s__Object)) => ((s__part(V__OBJ1,V__OBJ2) & ~(s__part(V__OBJ2,V__OBJ1))) => s__properPart(V__OBJ1,V__OBJ2))) )
|
Merge.kif 951-956 | If X is a part of Y and Y is not a part of X, then X is a proper part of Y |
| ! [V__OBJ : $i,V__P : $i,V__PERSON : $i,V__T : $i] : (((s__holdsDuring(V__T, s__possesses(V__PERSON, V__OBJ)) & s__part(V__P, V__OBJ)) => s__holdsDuring(V__T, s__possesses(V__PERSON, V__P)))) | Merge.kif 4371-4377 | If X possesses Y holds during Z and W is a part of Y, then X possesses W holds during Z |
| ! [V__S,V__CO,V__N,V__U,V__SI,V__N2] : (((s__instance(V__S,s__Class) & s__subclass(V__S,s__Substance) & s__instance(V__CO,s__CorpuscularObject) & s__instance(V__N,s__RealNumber) & s__instance(V__U,s__UnitOfMass) & s__instance(V__SI,s__Object) & s__instance(V__N2,s__RealNumber)) => ((s__amount(V__S,V__CO,s__MeasureFn(V__N,V__U)) & s__instance(V__SI,V__S) & s__measure(V__SI,s__MeasureFn(V__N2,V__U)) & s__part(V__SI,V__CO)) => (? [V__L] : ((s__instance(V__L,s__List) & (s__inList(s__MeasureFn(V__N2,V__U) ,V__L) & (V__L = s__AmountsFn(V__S,V__CO,V__U)) & (V__N = s__ListSumFn(V__L)))))))) )
|
Merge.kif 7740-7755 | If amount X, Y and Z W(s), V is an instance of X, the measure of V is U W(s), and V is a part of Y, then there exists T such that U W(s) is a member of T and equal T and Amounts fn X, Y and W and equal Z and the sum of T |
| ! [V__OBJ3,V__OBJ1,V__OBJ2] : (((s__instance(V__OBJ3,s__Object) & s__instance(V__OBJ1,s__Object) & s__instance(V__OBJ2,s__Object)) => ((s__part(V__OBJ3,V__OBJ1) & s__part(V__OBJ3,V__OBJ2)) => s__overlapsSpatially(V__OBJ1,V__OBJ2))) )
|
Merge.kif 9812-9816 | If X is a part of Y and X is a part of Z, then Y and Z overlapsSpatially |
| ! [V__OBJ1,V__OBJ2,V__OBJ3] : (((s__instance(V__OBJ1,s__Object) & s__instance(V__OBJ2,s__Object) & s__instance(V__OBJ3,s__Object)) => ((~(s__part(V__OBJ1,V__OBJ2)) & ~(s__part(V__OBJ2,V__OBJ1)) & (s__part(V__OBJ3,V__OBJ1) & s__part(V__OBJ3,V__OBJ2))) => s__overlapsPartially(V__OBJ1,V__OBJ2))) )
|
Merge.kif 9859-9866 | If X is not a part of Y, Y is not a part of X, and Z is a part of X and Z is a part of Y, then X partially overlaps with Y |
| ! [V__BOTTOM,V__OBJECT,V__PART] : (((s__instance(V__BOTTOM,s__SelfConnectedObject) & s__instance(V__OBJECT,s__SelfConnectedObject) & s__instance(V__PART,s__Object)) => ((s__bottom(V__BOTTOM,V__OBJECT) & s__part(V__PART,V__OBJECT) & ~(s__connected(V__PART,V__BOTTOM))) => s__orientation(V__PART,V__BOTTOM,s__Above))) )
|
Merge.kif 9942-9947 | If the bottom of X is Y, Z is a part of X, and Z is not connected to Y, then Z is above to Y |
| ! [V__TOP,V__OBJECT,V__PART] : (((s__instance(V__TOP,s__SelfConnectedObject) & s__instance(V__OBJECT,s__SelfConnectedObject) & s__instance(V__PART,s__Object)) => ((s__top(V__TOP,V__OBJECT) & s__part(V__PART,V__OBJECT) & ~(s__connected(V__PART,V__TOP))) => s__orientation(V__PART,V__TOP,s__Below))) )
|
Merge.kif 9957-9962 | If the top of X is Y, Z is a part of X, and Z is not connected to Y, then Z is below to Y |
| ! [V__SIDE,V__OBJECT,V__PART] : (((s__instance(V__SIDE,s__SelfConnectedObject) & s__instance(V__OBJECT,s__SelfConnectedObject) & s__instance(V__PART,s__Object)) => ((s__side(V__SIDE,V__OBJECT) & s__part(V__PART,V__OBJECT) & ~(s__connected(V__PART,V__SIDE))) => (? [V__DIRECT] : ((s__instance(V__DIRECT,s__PositionalAttribute) & s__orientation(V__SIDE,V__PART,V__DIRECT)))))) )
|
Merge.kif 9972-9979 | If a side of X is Y, Z is a part of X, and Z is not connected to Y, then there exists W such that Y is W to Z |
| ! [V__HOLE,V__OBJ1,V__OBJ2] : (((s__instance(V__HOLE,s__HoleRegion) & s__instance(V__OBJ1,s__SelfConnectedObject) & s__instance(V__OBJ2,s__SelfConnectedObject)) => ((s__hole(V__HOLE,V__OBJ1) & s__part(V__OBJ1,V__OBJ2)) => (s__overlapsSpatially(V__HOLE,V__OBJ2) | s__hole(V__HOLE,V__OBJ2)))) )
|
Merge.kif 10130-10136 | If X is a hole in Y and Y is a part of Z, then X and Z overlapsSpatially or X is a hole in Z |
| ! [V__HOLE1,V__HOLE2] : ((s__instance(V__HOLE1,s__Object) => ((s__instance(V__HOLE2,s__HoleRegion) & s__part(V__HOLE1,V__HOLE2)) => s__attribute(V__HOLE1,s__Fillable))) )
|
Merge.kif 10194-10198 | If X is an instance of hole and Y is a part of X, then fillable is an attribute of Y |
| ! [V__PROCESS,V__PATH1,V__SOURCE,V__DEST,V__MEASURE1,V__U,V__DISTANCE,V__OBJ] : (((s__instance(V__PROCESS,s__Motion) & s__instance(V__PATH1,s__Object) & s__instance(V__SOURCE,s__Object) & s__instance(V__DEST,s__Object) & s__instance(V__MEASURE1,s__RealNumber) & s__instance(V__U,s__UnitOfMeasure) & s__instance(V__DISTANCE,s__RealNumber) & s__instance(V__OBJ,s__Object)) => ((s__path(V__PROCESS,V__PATH1) & s__origin(V__PROCESS,V__SOURCE) & s__destination(V__PROCESS,V__DEST) & s__length(V__PATH1,s__MeasureFn(V__MEASURE1,V__U)) & s__distance(V__SOURCE,V__DEST,s__MeasureFn(V__DISTANCE,V__U)) & ~(s__greaterThan(V__MEASURE1,V__DISTANCE)) & s__part(V__OBJ,V__PATH1)) => s__between(V__SOURCE,V__OBJ,V__DEST))) )
|
Merge.kif 11334-11344 | If All of the following hold: (1) X is path along which Y occurs (2) Y originates at Z (3) Y ends up at W (4) the length of X is V U(s) (5) the distance between Z and W is T U(s) (6) V is not greater than T (7) S is a part of X, then S is between Z and W |
| ! [V__SUBSTANCE,V__ANIMAL] : (((s__instance(V__SUBSTANCE,s__AnimalSubstance) & s__instance(V__ANIMAL,s__Organism) & s__part(V__SUBSTANCE,V__ANIMAL)) => s__instance(V__ANIMAL,s__Animal)) )
|
Merge.kif 15128-15133 | If X is an instance of animal substance, Y is an instance of organism, and X is a part of Y, then Y is an instance of animal |
| ! [V__SUBSTANCE,V__PLANT] : (((s__instance(V__SUBSTANCE,s__PlantSubstance) & s__instance(V__PLANT,s__Organism) & s__part(V__SUBSTANCE,V__PLANT)) => s__instance(V__PLANT,s__Plant)) )
|
Merge.kif 15139-15144 | If X is an instance of plant substance, Y is an instance of organism, and X is a part of Y, then Y is an instance of plant |
| ! [V__STRUCTURE,V__ANIMAL] : (((s__instance(V__STRUCTURE,s__AnimalAnatomicalStructure) & s__instance(V__ANIMAL,s__Organism) & s__part(V__STRUCTURE,V__ANIMAL)) => s__instance(V__ANIMAL,s__Animal)) )
|
Merge.kif 15296-15301 | If X is an instance of animal anatomical structure, Y is an instance of organism, and X is a part of Y, then Y is an instance of animal |
| ! [V__STRUCTURE,V__PLANT] : (((s__instance(V__STRUCTURE,s__PlantAnatomicalStructure) & s__instance(V__PLANT,s__Organism) & s__part(V__STRUCTURE,V__PLANT)) => s__instance(V__PLANT,s__Plant)) )
|
Merge.kif 15307-15312 | If X is an instance of plant anatomical structure, Y is an instance of organism, and X is a part of Y, then Y is an instance of plant |
| ! [V__H : $i,V__T1 : $i,V__T1C : $i,V__T2 : $i,V__T2C : $i] : (((s__subclass(V__T1C, s__Tissue) & s__subclass(V__T2C, s__Tissue) & s__instance(V__T1, V__T1C) & s__instance(V__T2, V__T2C) & s__instance(V__H, s__Human) & s__part(V__T1, V__H) & s__part(V__T2, V__H) & ~(V__T1C = V__T2C) & ~(s__subclass(V__T1C, V__T2C)) & ~(s__subclass(V__T2C, V__T1C)) & s__orientation(V__T1, V__T2, s__Adjacent)) => s__modalAttribute(( ? [V__CT:$i] : ((s__instance(V__CT, s__ConnectiveTissue) & s__between(V__T1, V__CT, V__T2)))), s__Likely))) | Merge.kif 15462-15483 | If All of the following hold: (1) X is a subclass of tissue (2) Y is a subclass of tissue (3) Z is an instance of X (4) W is an instance of Y (5) V is an instance of human (6) Z is a part of V (7) W is a part of V (8) equal X and Y (9) X is not a subclass of Y (10) Y is not a subclass of X (11) Z is adjacent to W, then the statement there exists U such that U is an instance of connective tissue, U is between Z, and W has the modal force of likely |
| ! [V__A,V__C,V__P] : (((s__instance(V__A,s__Animal) & s__instance(V__C,s__WearableItem) & s__instance(V__P,s__WearableItem)) => ((s__wears(V__A,V__C) & s__part(V__P,V__C)) => s__wears(V__A,V__P))) )
|
Merge.kif 16277-16281 | If X wears Y and Z is a part of Y, then X wears Z |
| ! [V__BODY,V__ORG] : (((s__instance(V__BODY,s__ReproductiveBody) & s__part(V__BODY,V__ORG) & s__instance(V__ORG,s__Organism)) => s__attribute(V__ORG,s__Female)) )
|
Merge.kif 18458-18463 | If X is an instance of reproductive body, X is a part of Y, and Y is an instance of organism, then female is an attribute of Y |
| ! [V__F : $i,V__H : $i,V__P : $i,V__PI : $i,V__T : $i] : (((s__holdsDuring(V__T, s__attribute(V__H, s__ImpairedBodyPartFn(V__P))) & s__instance(V__PI, V__P) & s__part(V__PI, V__H) & s__hasPurpose(V__PI, V__F)) => s__modalAttribute(~(V__F), s__Likely))) | Merge.kif 18566-18576 | If impaired body part fn X is an attribute of Y holds during Z, W is an instance of X, W is a part of Y, and W has the purpose V, then the statement V has the modal force of likely |
| ! [V__F : $i,V__H : $i,V__P : $i,V__PI : $i,V__T : $i] : (((s__holdsDuring(V__T, s__attribute(V__H, s__DeadOrMissingBodyPartFn(V__P))) & s__instance(V__PI, V__P) & s__part(V__PI, V__H) & s__hasPurpose(V__PI, V__F)) => ~(V__F))) | Merge.kif 18587-18595 | If dead or missing body part fn X is an attribute of Y holds during Z, W is an instance of X, W is a part of Y, and W has the purpose V, then V |
| ! [V__OBJ : $i,V__REM : $i] : (((s__instance(V__REM, s__OrganismRemains) & s__holdsDuring(s__WhenFn(V__REM), s__part(V__OBJ, V__REM))) => ( ? [V__ORG:$i] : ((s__instance(V__ORG, s__Organism) & s__earlier(s__WhenFn(V__ORG), s__WhenFn(V__REM)) & s__finishes(s__WhenFn(V__REM), s__WhenFn(V__ORG)) & s__holdsDuring(s__WhenFn(V__ORG), s__part(V__OBJ, V__ORG))))))) | Mid-level-ontology.kif 32-43 | If X is an instance of organism remains and Y is a part of X holds during the time of existence of X, then there exists Z such that Z is an instance of organism, the time of existence of Z happens earlier than the time of existence of X, the time of existence of X finishes the time of existence of Z, and Y is a part of Z holds during the time of existence of Z |
| ! [V__DEATH : $i,V__OBJ : $i,V__ORG : $i,V__REM : $i,V__T1 : $i,V__T2 : $i] : (((s__instance(V__DEATH, s__Death) & s__instance(V__REM, s__OrganismRemains) & s__instance(V__ORG, s__Organism) & s__holdsDuring(V__T2, s__part(V__OBJ, V__REM)) & s__holdsDuring(V__T1, s__part(V__OBJ, V__ORG)) & s__earlier(V__T1, V__T2) & s__result(V__DEATH, V__REM)) => s__experiencer(V__DEATH, V__ORG))) | Mid-level-ontology.kif 61-70 | If All of the following hold: (1) X is an instance of death (2) Y is an instance of organism remains (3) Z is an instance of organism (4) W is a part of Y holds during V (5) W is a part of Z holds during U (6) U happens earlier than V (7) Y is a result of X, then Z experiences X |
| ! [V__DEATH : $i,V__OBJ : $i,V__ORG : $i,V__REM : $i,V__T1 : $i,V__T2 : $i] : (((s__instance(V__DEATH, s__Death) & s__instance(V__REM, s__OrganismRemains) & s__instance(V__ORG, s__Organism) & s__holdsDuring(V__T2, s__part(V__OBJ, V__REM)) & s__holdsDuring(V__T1, s__part(V__OBJ, V__ORG)) & s__earlier(V__T1, V__T2) & s__experiencer(V__DEATH, V__ORG)) => s__result(V__DEATH, V__REM))) | Mid-level-ontology.kif 72-81 | If All of the following hold: (1) X is an instance of death (2) Y is an instance of organism remains (3) Z is an instance of organism (4) W is a part of Y holds during V (5) W is a part of Z holds during U (6) U happens earlier than V (7) Z experiences X, then Y is a result of X |
| ! [V__G,V__B,V__S,V__P] : (((s__instance(V__G,s__Gun) & s__instance(V__B,s__GunBarrel) & s__part(V__B,V__G) & s__instance(V__S,s__Shooting) & s__instrument(V__S,V__G) & s__patient(V__S,V__P) & s__instance(V__P,s__Projectile)) => (? [V__SUB] : ((s__instance(V__SUB,s__Motion) & (s__subProcess(V__SUB,V__S) & s__path(V__SUB,V__B)))))) )
|
Mid-level-ontology.kif 1336-1348 | If All of the following hold: (1) X is an instance of gun (2) Y is an instance of gun barrel (3) Y is a part of X (4) Z is an instance of shooting (5) X is an instrument for Z (6) W is a patient of Z (7) W is an instance of projectile, then there exists V such that V is a subprocess of Z and Y is path along which V occurs |
| ! [V__E1,V__O,V__E2,V__P1,V__P2,V__D1,V__U] : (((s__instance(V__E1,s__Object) & s__instance(V__O,s__Object) & s__instance(V__E2,s__Object) & s__instance(V__P1,s__Object) & s__instance(V__P2,s__Object) & s__instance(V__D1,s__RealNumber)) => ((s__physicalEnd(V__E1,V__O) & s__physicalEnd(V__E2,V__O) & s__part(V__P1,V__E1) & s__part(V__P2,V__E2) & s__instance(V__U,s__UnitOfLength) & s__distance(V__P1,V__P2,s__MeasureFn(V__D1,V__U)) & ~((V__E1 = V__E2))) => ~((? [V__OP1,V__OP2,V__D2] : ((s__instance(V__OP1,s__Object) & s__instance(V__OP2,s__Object) & s__instance(V__D2,s__RealNumber) & (~(s__part(V__OP1,V__E1)) & ~(s__part(V__OP2,V__E2)) & s__distance(V__OP1,V__OP2,s__MeasureFn(V__D2,V__U)) & s__greaterThan(V__D2,V__D1)))))))) )
|
Mid-level-ontology.kif 1550-1570 | If All of the following hold: (1) one end of X is Y (2) one end of X is Z (3) W is a part of Y (4) V is a part of Z (5) U is an instance of unit of length (6) the distance between W and V is T U(s) (7) equal Y and Z, then there don't exist S, R and Q such that S is not a part of Y and R is not a part of Z and the distance between S and R is Q U(s) and Q is greater than T |
| Display limited to 25 items. Show next 25 | ||
| Display limited to 25 items. Show next 25 |
| consequent |
|
|
| ! [V__OBJ1,V__OBJ2] : (((s__instance(V__OBJ1,s__Object) & s__instance(V__OBJ2,s__Object)) => (s__properPart(V__OBJ1,V__OBJ2) => (s__part(V__OBJ1,V__OBJ2) & ~(s__part(V__OBJ2,V__OBJ1))))) )
|
Merge.kif 944-949 | If X is a proper part of Y, then X is a part of Y and Y is not a part of X |
| ! [V__ATOM] : ((s__instance(V__ATOM,s__Atom) => (? [V__PROTON,V__ELECTRON] : ((s__part(V__PROTON,V__ATOM) & s__part(V__ELECTRON,V__ATOM) & s__instance(V__PROTON,s__Proton) & s__instance(V__ELECTRON,s__Electron))))) )
|
Merge.kif 1186-1193 | If X is an instance of atom, then there exist Y, Z such that Y is a part of X, Z is a part of X, Y is an instance of proton, and Z is an instance of electron |
| ! [V__ATOM] : ((s__instance(V__ATOM,s__Atom) => (! [V__NUCLEUS1,V__NUCLEUS2] : (((s__part(V__NUCLEUS1,V__ATOM) & s__part(V__NUCLEUS2,V__ATOM) & s__instance(V__NUCLEUS1,s__AtomicNucleus) & s__instance(V__NUCLEUS2,s__AtomicNucleus)) => (V__NUCLEUS1 = V__NUCLEUS2))))) )
|
Merge.kif 1195-1204 | If X is an instance of atom, then For all Objects Y and Z: if Y is a part of X, Z is a part of X, Y is an instance of atomic nucleus, and Z is an instance of atomic nucleus, then equal Y and Z |
| ! [V__STRING] : ((s__instance(V__STRING,s__SymbolicString) => (? [V__PART] : ((s__part(V__PART,V__STRING) & s__instance(V__PART,s__Character))))) )
|
Merge.kif 1437-1442 | If X is an instance of symbolic string, then there exists Y such that Y is a part of X and Y is an instance of character |
| ! [V__C : $i,V__P : $i,V__R : $i] : (((s__resourceExhausted(V__P, V__R) & s__instance(V__R, V__C)) => s__holdsDuring(s__ImmediateFutureFn(s__WhenFn(V__P)), ~(( ? [V__OBJ1:$i] : ((s__part(V__OBJ1, V__R) & s__instance(V__OBJ1, V__C)))))))) | Merge.kif 2644-2655 | If X exhausts Y and Y is an instance of Z, then there doesn't exist W such that W is a part of Y and W is an instance of Z holds during immediately after the time of existence of X |
| ! [V__OBJ2,V__OBJ1] : ((s__instance(V__OBJ2,s__Object) => ((s__instance(V__OBJ1,s__Object) & s__partlyLocated(V__OBJ1,V__OBJ2)) => (? [V__SUB] : ((s__instance(V__SUB,s__Object) & (s__part(V__SUB,V__OBJ1) & s__located(V__SUB,V__OBJ2))))))) )
|
Merge.kif 4167-4174 | If X is an instance of object and X is partly located in Y, then there exists Z such that Z is a part of X and Z is located at Y |
| ! [V__OBJ1,V__OBJ2] : (((s__instance(V__OBJ1,s__Object) & s__instance(V__OBJ2,s__Object)) => (s__located(V__OBJ1,V__OBJ2) => (! [V__SUB] : ((s__instance(V__SUB,s__Object) => (s__part(V__SUB,V__OBJ1) => s__located(V__SUB,V__OBJ2))))))) )
|
Merge.kif 4188-4193 | If X is located at Y, then For all Object Z: if Z is a part of X, then Z is located at Y |
| ! [V__OBJ1,V__OBJ2] : (((s__instance(V__OBJ1,s__Object) & s__instance(V__OBJ2,s__Object)) => (s__overlapsSpatially(V__OBJ1,V__OBJ2) => (? [V__OBJ3] : ((s__instance(V__OBJ3,s__Object) & (s__part(V__OBJ3,V__OBJ1) & s__part(V__OBJ3,V__OBJ2))))))) )
|
Merge.kif 9805-9810 | If X and Y overlapsSpatially, then there exists Z such that Z is a part of X and Z is a part of Y |
| ! [V__OBJ1,V__OBJ2] : (((s__instance(V__OBJ1,s__Object) & s__instance(V__OBJ2,s__Object)) => (s__overlapsPartially(V__OBJ1,V__OBJ2) => (~(s__part(V__OBJ1,V__OBJ2)) & ~(s__part(V__OBJ2,V__OBJ1)) & (? [V__OBJ3] : ((s__instance(V__OBJ3,s__Object) & (s__part(V__OBJ3,V__OBJ1) & s__part(V__OBJ3,V__OBJ2)))))))) )
|
Merge.kif 9849-9857 | If X partially overlaps with Y, then X is not a part of Y, Y is not a part of X, and there exists Z such that Z is a part of X and Z is a part of Y |
| ! [V__PART,V__WHOLE] : (((s__instance(V__PART,s__Object) & s__instance(V__WHOLE,s__Object)) => (s__superficialPart(V__PART,V__WHOLE) => s__part(V__PART,V__WHOLE))) )
|
Merge.kif 9872-9874 | If X is a superficial part of Y, then X is a part of Y |
| ! [V__OBJ1,V__OBJ2] : (((s__instance(V__OBJ1,s__SelfConnectedObject) & s__instance(V__OBJ2,s__SelfConnectedObject)) => (s__surface(V__OBJ1,V__OBJ2) => (! [V__OBJ3] : ((s__instance(V__OBJ3,s__Object) => (s__superficialPart(V__OBJ3,V__OBJ2) => s__part(V__OBJ3,V__OBJ1))))))) )
|
Merge.kif 9910-9915 | If X is a surface of Y, then For all Object Z: if Z is a superficial part of Y, then Z is a part of X |
| ! [V__OBJ3,V__OBJ1,V__OBJ2] : (((s__instance(V__OBJ3,s__Object) & s__instance(V__OBJ1,s__Object) & s__instance(V__OBJ2,s__Object)) => ((V__OBJ3 = s__MereologicalSumFn(V__OBJ1,V__OBJ2)) => (! [V__PART] : ((s__instance(V__PART,s__Object) => ((s__part(V__PART,V__OBJ3) => (s__part(V__PART,V__OBJ1) | s__part(V__PART,V__OBJ2))) & ((s__part(V__PART,V__OBJ1) | s__part(V__PART,V__OBJ2)) => s__part(V__PART,V__OBJ3)))))))) )
|
Merge.kif 10023-10030 | If equal X, the union of the parts of Y, and Z, then For all Object W: W is a part of X if and only if W is a part of Y or W is a part of Z |
| ! [V__OBJ3,V__OBJ1,V__OBJ2] : (((s__instance(V__OBJ3,s__Object) & s__instance(V__OBJ1,s__Object) & s__instance(V__OBJ2,s__Object)) => ((V__OBJ3 = s__MereologicalProductFn(V__OBJ1,V__OBJ2)) => (! [V__PART] : ((s__instance(V__PART,s__Object) => ((s__part(V__PART,V__OBJ3) => (s__part(V__PART,V__OBJ1) & s__part(V__PART,V__OBJ2))) & ((s__part(V__PART,V__OBJ1) & s__part(V__PART,V__OBJ2)) => s__part(V__PART,V__OBJ3)))))))) )
|
Merge.kif 10044-10051 | If equal X, the intersection of the parts of Y, and Z, then For all Object W: W is a part of X if, only if W is a part of Y, and W is a part of Z |
| ! [V__HOLE1,V__OBJ,V__HOLE2] : (((s__instance(V__HOLE1,s__HoleRegion) & s__instance(V__OBJ,s__SelfConnectedObject) & s__instance(V__HOLE2,s__HoleRegion)) => ((s__hole(V__HOLE1,V__OBJ) & s__hole(V__HOLE2,V__OBJ)) => (! [V__HOLE3] : ((s__instance(V__HOLE3,s__HoleRegion) => (s__part(V__HOLE3,s__MereologicalSumFn(V__HOLE1,V__HOLE2)) => s__hole(V__HOLE3,V__OBJ))))))) )
|
Merge.kif 10121-10128 | If X is a hole in Y and Z is a hole in Y, then For all HoleRegion W: if W is a part of the union of the parts of X and Z, then W is a hole in Y |
| ! [V__HOLE1] : ((s__instance(V__HOLE1,s__Object) => (s__attribute(V__HOLE1,s__Fillable) => (? [V__HOLE2] : ((s__instance(V__HOLE2,s__HoleRegion) & s__part(V__HOLE1,V__HOLE2)))))) )
|
Merge.kif 10187-10192 | If fillable is an attribute of X, then there exists Y such that Y is an instance of hole and X is a part of Y |
| ! [V__OBJ,V__HOLE1] : (((s__instance(V__OBJ,s__Object) & s__instance(V__HOLE1,s__HoleRegion)) => (s__partiallyFills(V__OBJ,V__HOLE1) => (? [V__HOLE2] : ((s__instance(V__HOLE2,s__HoleRegion) & (s__part(V__HOLE2,V__HOLE1) & s__completelyFills(V__OBJ,V__HOLE2))))))) )
|
Merge.kif 10212-10217 | If X partially fills Y, then there exists Z such that Z is a part of Y and X completely fills Z |
| ! [V__OBJ,V__HOLE1] : (((s__instance(V__OBJ,s__Object) & s__instance(V__HOLE1,s__HoleRegion)) => (s__properlyFills(V__OBJ,V__HOLE1) => (? [V__HOLE2] : ((s__instance(V__HOLE2,s__HoleRegion) & (s__part(V__HOLE2,V__HOLE1) & s__fills(V__OBJ,V__HOLE2))))))) )
|
Merge.kif 10219-10224 | If X properly fills Y, then there exists Z such that Z is a part of Y and X fills Z |
| ! [V__OBJ1,V__HOLE] : (((s__instance(V__OBJ1,s__Object) & s__instance(V__HOLE,s__HoleRegion)) => (s__completelyFills(V__OBJ1,V__HOLE) => (? [V__OBJ2] : ((s__instance(V__OBJ2,s__Object) & (s__part(V__OBJ2,V__OBJ1) & s__fills(V__OBJ2,V__HOLE))))))) )
|
Merge.kif 10240-10245 | If X completely fills Y, then there exists Z such that Z is a part of X and Z fills Y |
| ! [V__DEATH : $i,V__ORG : $i] : (((s__instance(V__DEATH, s__Death) & s__instance(V__ORG, s__Organism) & s__experiencer(V__DEATH, V__ORG)) => ( ? [V__REM:$i, V__OBJ:$i] : ((s__result(V__DEATH, V__REM) & s__instance(V__REM, s__OrganicObject) & s__holdsDuring(s__FutureFn(s__WhenFn(V__DEATH)), s__attribute(V__REM, s__Dead)) & (s__holdsDuring(s__ImmediateFutureFn(s__WhenFn(V__DEATH)), s__part(V__OBJ, V__REM)) => s__holdsDuring(s__ImmediatePastFn(s__WhenFn(V__DEATH)), s__part(V__OBJ, V__ORG)))))))) | Merge.kif 10450-10469 | If X is an instance of death, Y is an instance of organism, and Y experiences X, then there exist Z and W such that Z is a result of X and Z is an instance of organic object and dead is an attribute of Z holds during after the time of existence of X and W is a part of Z holds during immediately after the time of existence of XW is a part of Y holds during immediately before the time of existence of X |
| ! [V__ORG,V__PATH] : ((s__instance(V__ORG,s__AutonomousAgent) => ((s__instance(V__PATH,s__PathologicProcess) & s__experiencer(V__PATH,V__ORG)) => (? [V__PART,V__DISEASE] : ((s__instance(V__PART,s__Object) & (s__part(V__PART,V__ORG) & s__instance(V__DISEASE,s__DiseaseOrSyndrome) & s__attribute(V__PART,V__DISEASE))))))) )
|
Merge.kif 10641-10649 | If X is an instance of pathologic process and Y experiences X, then there exist Z, W such that Z is a part of Y, W is an instance of disease or syndrome, and W is an attribute of Z |
| ! [V__BIO,V__PROC] : ((s__instance(V__BIO,s__Object) => ((s__instance(V__PROC,s__TherapeuticProcess) & s__patient(V__PROC,V__BIO)) => (s__instance(V__BIO,s__Organism) | (? [V__ORG] : ((s__instance(V__ORG,s__Organism) & s__part(V__BIO,V__ORG))))))) )
|
Merge.kif 12530-12539 | If X is an instance of therapeutic process and Y is a patient of X, then Y is an instance of organism or there exists Z such that Z is an instance of organism and Y is a part of Z |
| ! [V__COMBINE : $i,V__OBJ1 : $i,V__OBJ2 : $i] : ((((s__instance(V__COMBINE, s__Combining) & s__resource(V__COMBINE, V__OBJ1) & s__result(V__COMBINE, V__OBJ2)) => (s__holdsDuring(s__BeginFn(s__WhenFn(V__COMBINE)), ~(s__part(V__OBJ1, V__OBJ2))) & s__holdsDuring(s__EndFn(s__WhenFn(V__COMBINE)), s__part(V__OBJ1, V__OBJ2)))) & ((s__holdsDuring(s__BeginFn(s__WhenFn(V__COMBINE)), ~(s__part(V__OBJ1, V__OBJ2))) & s__holdsDuring(s__EndFn(s__WhenFn(V__COMBINE)), s__part(V__OBJ1, V__OBJ2))) => (s__instance(V__COMBINE, s__Combining) & s__resource(V__COMBINE, V__OBJ1) & s__result(V__COMBINE, V__OBJ2))))) | Merge.kif 12756-12763 | X is an instance of combining, Y is a resource for X, Z is a result of X if, only if Y is not a part of Z holds during the beginning of the time of existence of X, and Y is a part of Z holds during the end of the time of existence of X |
| ! [V__COLORING : $i,V__OBJ : $i] : (((s__instance(V__COLORING, s__Coloring) & s__patient(V__COLORING, V__OBJ)) => ( ? [V__PROPERTY:$i, V__PART:$i] : ((s__part(V__PART, V__OBJ) & s__instance(V__PROPERTY, s__ColorAttribute) & ((s__holdsDuring(s__BeginFn(s__WhenFn(V__COLORING)), s__attribute(V__PART, V__PROPERTY)) & s__holdsDuring(s__EndFn(s__WhenFn(V__COLORING)), ~(s__attribute(V__PART, V__PROPERTY)))) | (s__holdsDuring(s__BeginFn(s__WhenFn(V__COLORING)), ~(s__attribute(V__PART, V__PROPERTY))) & s__holdsDuring(s__EndFn(s__WhenFn(V__COLORING)), s__attribute(V__PART, V__PROPERTY))))))))) | Merge.kif 12926-12940 | If X is an instance of coloring and Y is a patient of X, then there exist Z and W such that W is a part of Y and Z is an instance of color attribute and Z is an attribute of W holds during the beginning of the time of existence of X and Z is not an attribute of W holds during the end of the time of existence of X or Z is not an attribute of W holds during the beginning of the time of existence of X and Z is an attribute of W holds during the end of the time of existence of X |
| ! [V__OBJ : $i,V__PROCESS : $i] : (((s__instance(V__PROCESS, s__StateChange) & s__patient(V__PROCESS, V__OBJ)) => ( ? [V__PART:$i, V__STATE1:$i, V__STATE2:$i] : ((s__part(V__PART, V__OBJ) & s__instance(V__STATE1, s__PhysicalState) & s__instance(V__STATE2, s__PhysicalState) & ~(V__STATE1 = V__STATE2) & s__holdsDuring(s__BeginFn(s__WhenFn(V__PROCESS)), s__attribute(V__PART, V__STATE1)) & s__holdsDuring(s__EndFn(s__WhenFn(V__PROCESS)), s__attribute(V__PART, V__STATE2))))))) | Merge.kif 14066-14077 | If X is an instance of state change and Y is a patient of X, then All of the following hold: (1) there exist Z, W (2) V such that Z is a part of Y (3) W is an instance of physical state (4) V is an instance of physical state (5) equal W (6) V (7) W is an attribute of Z holds during the beginning of the time of existence of X (8) V is an attribute of Z holds during the end of the time of existence of X |
| ! [V__ATOM : $i,V__NUMBER : $int,V__PROTON : $i,V__SUBSTANCE : $i,V__TYPE : $i] : ((s__atomicNumber(V__TYPE,V__NUMBER) => ((s__instance(V__SUBSTANCE, V__TYPE) & s__part(V__ATOM, V__SUBSTANCE) & s__instance(V__ATOM, s__Atom)) => V__NUMBER = s__CardinalityFn(s__KappaFn(V__PROTON, (s__part(V__PROTON, V__ATOM) & s__instance(V__PROTON, s__Proton))))))) | Merge.kif 14087-14099 | Assuming X is an atomic number of Y, it follows that: if Z is an instance of Y, W is a part of Z, and W is an instance of atom, then equal X and the number of instances in the class described by V |
| Display limited to 25 items. Show next 25 | ||
| Display limited to 25 items. Show next 25 |
| appearance as argument number 0 |
|
|
|