Browsing Interface : Welcome guest : log in
Home |  Graph |  LogLearn |  ]  KB:  Language:    Formal Language: 


KB Term:  Term intersection
English Word: 

Sigma KEE - holdsDuring
holdsDuring

appearance as argument number 1
-------------------------


(instance holdsDuring BinaryPredicate) Merge.kif 3916-3916 holds during is an instance of binary predicate
(instance holdsDuring AsymmetricRelation) Merge.kif 3917-3917 holds during is an instance of asymmetric relation
(domain holdsDuring 1 TimePosition) Merge.kif 3918-3918 The number 1 argument of holds during is an instance of time position
(domain holdsDuring 2 Formula) Merge.kif 3919-3919 The number 2 argument of holds during is an instance of formula
(documentation holdsDuring EnglishLanguage "(holdsDuring ?TIME ?FORMULA) means that the proposition denoted by ?FORMULA is true in the time frame ?TIME. Note that this implies that ?FORMULA is true at every TimePoint which is a temporalPart of ?TIME.") Merge.kif 3921-3924 The number 2 argument of holds during is an instance of formula

appearance as argument number 2
-------------------------


(relatedInternalConcept time holdsDuring) Merge.kif 3906-3906 time is internally related to holds during
(termFormat EnglishLanguage holdsDuring "holds during") domainEnglishFormat.kif 28355-28355 time is internally related to holds during
(termFormat ChineseTraditionalLanguage holdsDuring "持有期間") domainEnglishFormat.kif 28356-28356 time is internally related to holds during
(termFormat ChineseLanguage holdsDuring "持有期间") domainEnglishFormat.kif 28357-28357 time is internally related to holds during
(format EnglishLanguage holdsDuring "%2 %n{doesn't} hold%p{s} during %1") english_format.kif 122-122 time is internally related to holds during

antecedent
-------------------------


(<=>
    (holdsDuring ?TIME
        (attribute ?AGENT LegalPersonhood))
    (holdsDuring ?TIME
        (or
            (capability LegalAction agent ?AGENT)
            (capability LegalAction patient ?AGENT))))
Merge.kif 1635-1641 Legal personhood is an attribute of X holds during Y if and only if X is capable of doing legal action as a agent or X is capable of doing legal action as a patient holds during Y
(=>
    (holdsDuring ?TIME
        (leader ?X ?Y))
    (holdsDuring ?TIME
        (attribute ?Y Living)))
Merge.kif 1652-1654 If X is a leader of Y holds during Z, then living is an attribute of X holds during Z
(=>
    (and
        (holdsDuring ?T2 ?SIT2)
        (holdsDuring ?T1 ?SIT1)
        (instance ?T1 TimeInterval)
        (instance ?T2 TimeInterval)
        (causesProposition ?SIT1 ?SIT2))
    (beforeOrEqual
        (BeginFn ?T1)
        (BeginFn ?T2)))
Merge.kif 3873-3880 If X holds during Y, Z holds during W, W is an instance of timeframe, Y is an instance of timeframe, and X is a causes proposition of Z, then the beginning of W happens before or at the beginning of Y
(=>
    (and
        (holdsDuring ?TIME ?SITUATION1)
        (entails ?SITUATION1 ?SITUATION2))
    (holdsDuring ?TIME ?SITUATION2))
Merge.kif 3926-3930 If X holds during Y and X entails Z, then Z holds during Y
(=>
    (holdsDuring ?TIME
        (not ?SITUATION))
    (not
        (holdsDuring ?TIME ?SITUATION)))
Merge.kif 3932-3936 If X holds during Y, then X doesn't hold during Y
(=>
    (holdsDuring ?TIME
        (confersNorm ?ENTITY ?NORM ?FORMULA))
    (and
        (holdsDuring
            (ImmediatePastFn ?TIME)
            (not
                (modalAttribute ?FORMULA ?NORM)))
        (holdsDuring
            (ImmediateFutureFn ?TIME)
            (modalAttribute ?FORMULA ?NORM))))
Merge.kif 4040-4050 If X confers norm Y for Z holds during W, then the statement Z doesn't have the modal force of Y holds during immediately before W and the statement Z has the modal force of Y holds during immediately after W
(=>
    (holdsDuring ?TIME
        (deprivesNorm ?ENTITY ?NORM ?FORMULA))
    (and
        (holdsDuring
            (ImmediatePastFn ?TIME)
            (modalAttribute ?FORMULA ?NORM))
        (holdsDuring
            (ImmediateFutureFn ?TIME)
            (not
                (modalAttribute ?FORMULA ?NORM)))))
Merge.kif 4062-4071 If X deprives norm Y for Z holds during W, then the statement Z has the modal force of Y holds during immediately before W and the statement Z doesn't have the modal force of Y holds during immediately after W
(=>
    (holdsDuring ?TIME
        (exactlyLocated ?THING ?REGION))
    (equal
        (WhereFn ?THING ?TIME) ?REGION))
Merge.kif 4289-4293 If X is exactly located in Y holds during Z, then equal the place where X was at Z and Y
(=>
    (and
        (holdsDuring ?T
            (possesses ?PERSON ?OBJ))
        (part ?P ?OBJ))
    (holdsDuring ?T
        (possesses ?PERSON ?P)))
Merge.kif 4309-4315 If X possesses Y holds during Z and W is a part of Y, then X possesses W holds during Z
(=>
    (and
        (instance ?TIME TimePosition)
        (holdsDuring ?TIME
            (possesses ?AGENT1 ?OBJ))
        (holdsDuring ?TIME
            (possesses ?AGENT2 ?OBJ)))
    (equal ?AGENT1 ?AGENT2))
Merge.kif 4317-4322 If X is an instance of time position, Y possesses Z holds during X, and W possesses Z holds during X, then equal Y and W
(=>
    (and
        (instance ?TIME TimePoint)
        (holdsDuring ?TIME
            (age ?OBJ ?DURATION)))
    (duration
        (TimeIntervalFn
            (BeginFn
                (WhenFn ?OBJ)) ?TIME) ?DURATION))
Merge.kif 7593-7597 If X is an instance of time point and the age of Y is Z holds during X, then duration of interval between the beginning of the time of existence of Y and X is Z
(=>
    (and
        (holdsDuring ?TIME1 ?SITUATION)
        (temporalPart ?TIME2 ?TIME1))
    (holdsDuring ?TIME2 ?SITUATION))
Merge.kif 8059-8063 If X holds during Y and Z is a part of Y, then X holds during Z
(=>
    (and
        (holdsDuring ?INTERVAL
            (?REL ?INST1 ?INST2))
        (instance ?INST1 Physical)
        (instance ?INST2 Physical))
    (and
        (time ?INST1 ?INTERVAL)
        (time ?INST2 ?INTERVAL)))
Merge.kif 8065-8072 If X Y and Z holds during W, Y is an instance of physical, and Z is an instance of physical, then Y exists during W and Z exists during W
(=>
    (and
        (resource ?PROC ?OBJ)
        (holdsDuring
            (BeginFn
                (WhenFn ?PROC))
            (measure ?OBJ ?QUANT1))
        (holdsDuring
            (EndFn
                (WhenFn ?PROC))
            (measure ?OBJ ?QUANT2)))
    (greaterThan ?QUANT1 ?QUANT2))
Merge.kif 8130-8135 If X is a resource for Y, the measure of X is Z holds during the beginning of the time of existence of Y, and the measure of X is W holds during the end of the time of existence of Y, then Z is greater than W
(=>
    (holdsDuring ?TIME
        (fills ?OBJ ?HOLE))
    (attribute ?HOLE Fillable))
Merge.kif 10114-10117 If X fills Y holds during Z, then fillable is an attribute of Y
(=>
    (holdsDuring ?T1
        (expects ?AGENT ?FORMULA))
    (exists (?T2)
        (and
            (holdsDuring ?T1
                (believes ?AGENT
                    (holdsDuring ?T2 ?FORMULA)))
            (earlier ?T1 ?T2))))
Merge.kif 10753-10761 If X expects Y will be true holds during Z, then there exists W such that X believes Y holds during W holds during Z and Z happens earlier than W
(=>
    (and
        (instance ?WALK Walking)
        (instance ?RUN Running)
        (agent ?WALK ?AGENT)
        (agent ?RUN ?AGENT)
        (holdsDuring
            (WhenFn ?WALK)
            (measure ?AGENT
                (SpeedFn ?LENGTH1 ?TIME)))
        (holdsDuring
            (WhenFn ?RUN)
            (measure ?AGENT
                (SpeedFn ?LENGTH2 ?TIME))))
    (greaterThan ?LENGTH2 ?LENGTH1))
Merge.kif 11316-11324 If All of the following hold: (1) X is an instance of walking (2) Y is an instance of running (3) Z is an agent of X (4) Z is an agent of Y (5) the measure of Z is W per V holds during the time of existence of X (6) the measure of Z is U per V holds during the time of existence of Y, then U is greater than W
(=>
    (and
        (attribute ?W Windy)
        (located ?W ?L)
        (equal ?T
            (WhenFn ?W))
        (holdsDuring ?T
            (surfaceWindSpeed ?L
                (MeasureFn ?N MilesPerHour))))
    (greaterThan ?N 20.0))
Merge.kif 11434-11442 If windy is an attribute of X, X is located at Y, equal Z and the time of existence of X, and W miles per hour(s) is a surface wind speed of Y holds during Z, then W is greater than 20.0
(=>
    (and
        (instance ?CHANGE ChangeOfPossession)
        (patient ?CHANGE ?OBJ)
        (holdsDuring
            (BeginFn
                (WhenFn ?CHANGE))
            (possesses ?AGENT1 ?OBJ))
        (holdsDuring
            (EndFn
                (WhenFn ?CHANGE))
            (possesses ?AGENT2 ?OBJ)))
    (not
        (equal ?AGENT1 ?AGENT2)))
Merge.kif 11817-11824 If X is an instance of change of possession, Y is a patient of X, Z possesses Y holds during the beginning of the time of existence of X, and W possesses Y holds during the end of the time of existence of X, then equal Z and W
(=>
    (and
        (instance ?DISCOVER Discovering)
        (agent ?DISCOVER ?A)
        (patient ?DISCOVER ?OBJ)
        (holdsDuring
            (WhenFn ?DISCOVER)
            (located ?OBJ ?PLACE)))
    (holdsDuring
        (ImmediateFutureFn ?DISCOVERING)
        (knows ?A
            (located ?OBJ ?PLACE))))
Merge.kif 12143-12154 If X is an instance of discovering, Y is an agent of X, Z is a patient of X, and Z is located at W holds during the time of existence of X, then Y knows Z is located at W holds during immediately after V
(=>
    (and
        (instance ?A Attaching)
        (patient ?A ?O1)
        (patient ?A ?O2)
        (holdsDuring
            (BeginFn
                (WhenFn ?A))
            (not
                (connected ?O1 ?O2)))
        (holdsDuring
            (EndFn
                (WhenFn ?A))
            (connected ?O1 ?O2)))
    (and
        (objectAttached ?A ?O1)
        (objectAttached ?A ?O2)))
Merge.kif 12557-12571 If X is an instance of attaching, Y is a patient of X, Z is a patient of X, Y is not connected to Z holds during the beginning of the time of existence of X, and Y is connected to Z holds during the end of the time of existence of X, then X attaches Y to another object and X attaches Z to another object
(=>
    (and
        (instance ?D Detaching)
        (patient ?D ?O1)
        (patient ?D ?O2)
        (holdsDuring
            (BeginFn
                (WhenFn ?D))
            (connected ?O1 ?O2))
        (holdsDuring
            (EndFn
                (WhenFn ?A))
            (not
                (connected ?O1 ?O2))))
    (and
        (objectDetached ?A ?O1)
        (objectDetached ?A ?O2)))
Merge.kif 12607-12616 If X is an instance of detaching, Y is a patient of X, Z is a patient of X, Y is connected to Z holds during the beginning of the time of existence of X, and Y is not connected to Z holds during the end of the time of existence of W, then W detaches Y from another object and W detaches Z from another object
(=>
    (and
        (instance ?BOILING Boiling)
        (boilingPoint ?TYPE
            (MeasureFn ?TEMP1 ?MEASURE))
        (instance ?SUBSTANCE ?TYPE)
        (patient ?BOILING ?SUBSTANCE)
        (holdsDuring
            (WhenFn ?BOILING)
            (measure ?SUBSTANCE
                (MeasureFn ?TEMP2 ?MEASURE)))
        (instance ?MEASURE UnitOfTemperature))
    (greaterThanOrEqualTo ?TEMP2 ?TEMP1))
Merge.kif 14006-14014 If All of the following hold: (1) X is an instance of boiling (2) Y Z(s) is a boiling point of W (3) V is an instance of W (4) V is a patient of X (5) the measure of V is U Z(s) holds during the time of existence of X (6) Z is an instance of unit of temperature, then U is greater than or equal to Y
(=>
    (and
        (boilingPoint ?TYPE
            (MeasureFn ?TEMP1 ?MEASURE))
        (instance ?SUBSTANCE ?TYPE)
        (holdsDuring ?TIME
            (measure ?SUBSTANCE
                (MeasureFn ?TEMP2 ?MEASURE)))
        (instance ?MEASURE UnitOfTemperature)
        (greaterThanOrEqualTo ?TEMP2 ?TEMP1))
    (or
        (holdsDuring ?TIME
            (attribute ?SUBSTANCE Gas))
        (exists (?BOIL)
            (and
                (overlapsTemporally
                    (WhenFn ?BOIL) ?TIME)
                (instance ?BOIL Boiling)
                (patient ?BOIL ?SUBSTANCE)))))
Merge.kif 14016-14029 If X Y(s) is a boiling point of Z, W is an instance of Z, the measure of W is V Y(s) holds during U, Y is an instance of unit of temperature, and V is greater than or equal to X, then gas is an attribute of W holds during U or there exists T such that U overlaps the time of existence of T, T is an instance of boiling, and W is a patient of T
(=>
    (and
        (instance ?SUBSTANCE ?TYPE)
        (boilingPoint ?TYPE
            (MeasureFn ?TEMP1 ?MEASURE))
        (meltingPoint ?TYPE
            (MeasureFn ?TEMP2 ?MEASURE))
        (instance ?MEASURE UnitOfTemperature)
        (holdsDuring ?TIME
            (measure ?SUBSTANCE
                (MeasureFn ?TEMP3 ?MEASURE)))
        (greaterThan ?TEMP3 ?TEMP2)
        (lessThan ?TEMP3 ?TEMP1))
    (or
        (holdsDuring ?TIME
            (attribute ?SUBSTANCE Liquid))
        (exists (?MELT)
            (and
                (overlapsTemporally
                    (WhenFn ?MELT) ?TIME)
                (instance ?MELT Melting)
                (patient ?MELT ?SUBSTANCE)))))
Merge.kif 14038-14053 If All of the following hold: (1) X is an instance of Y (2) Z W(s) is a boiling point of Y (3) V W(s) is a melting point of Y (4) W is an instance of unit of temperature (5) the measure of X is U W(s) holds during T (6) U is greater than V (7) U is less than Z, then liquid is an attribute of X holds during T or there exists S such that T overlaps the time of existence of S, S is an instance of melting, and X is a patient of S

Display limited to 25 items. Show next 25

Display limited to 25 items. Show next 25

consequent
-------------------------


(<=>
    (holdsDuring ?TIME
        (attribute ?AGENT LegalPersonhood))
    (holdsDuring ?TIME
        (or
            (capability LegalAction agent ?AGENT)
            (capability LegalAction patient ?AGENT))))
Merge.kif 1635-1641 Legal personhood is an attribute of X holds during Y if and only if X is capable of doing legal action as a agent or X is capable of doing legal action as a patient holds during Y
(=>
    (holdsDuring ?TIME
        (leader ?X ?Y))
    (holdsDuring ?TIME
        (attribute ?Y Living)))
Merge.kif 1652-1654 If X is a leader of Y holds during Z, then living is an attribute of X holds during Z
(=>
    (and
        (resourceExhausted ?P ?R)
        (instance ?R ?C))
    (holdsDuring
        (ImmediateFutureFn
            (WhenFn ?P))
        (not
            (exists (?OBJ1)
                (and
                    (part ?OBJ1 ?R)
                    (instance ?OBJ1 ?C))))))
Merge.kif 2572-2581 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
(=>
    (believes ?AGENT ?FORMULA)
    (exists (?TIME)
        (holdsDuring ?TIME
            (considers ?AGENT ?FORMULA))))
Merge.kif 2852-2856 If X believes Y, then there exists Z such that X considers Y holds during Z
(=>
    (and
        (holdsDuring ?TIME ?SITUATION1)
        (entails ?SITUATION1 ?SITUATION2))
    (holdsDuring ?TIME ?SITUATION2))
Merge.kif 3926-3930 If X holds during Y and X entails Z, then Z holds during Y
(=>
    (holdsDuring ?TIME
        (not ?SITUATION))
    (not
        (holdsDuring ?TIME ?SITUATION)))
Merge.kif 3932-3936 If X holds during Y, then X doesn't hold during Y
(=>
    (holdsDuring ?TIME
        (confersNorm ?ENTITY ?NORM ?FORMULA))
    (and
        (holdsDuring
            (ImmediatePastFn ?TIME)
            (not
                (modalAttribute ?FORMULA ?NORM)))
        (holdsDuring
            (ImmediateFutureFn ?TIME)
            (modalAttribute ?FORMULA ?NORM))))
Merge.kif 4040-4050 If X confers norm Y for Z holds during W, then the statement Z doesn't have the modal force of Y holds during immediately before W and the statement Z has the modal force of Y holds during immediately after W
(=>
    (holdsDuring ?TIME
        (deprivesNorm ?ENTITY ?NORM ?FORMULA))
    (and
        (holdsDuring
            (ImmediatePastFn ?TIME)
            (modalAttribute ?FORMULA ?NORM))
        (holdsDuring
            (ImmediateFutureFn ?TIME)
            (not
                (modalAttribute ?FORMULA ?NORM)))))
Merge.kif 4062-4071 If X deprives norm Y for Z holds during W, then the statement Z has the modal force of Y holds during immediately before W and the statement Z doesn't have the modal force of Y holds during immediately after W
(=>
    (equal
        (WhereFn ?THING ?TIME) ?REGION)
    (holdsDuring ?TIME
        (exactlyLocated ?THING ?REGION)))
Merge.kif 4283-4287 If equal the place where X was at Y and Z, then X is exactly located in Z holds during Y
(=>
    (and
        (holdsDuring ?T
            (possesses ?PERSON ?OBJ))
        (part ?P ?OBJ))
    (holdsDuring ?T
        (possesses ?PERSON ?P)))
Merge.kif 4309-4315 If X possesses Y holds during Z and W is a part of Y, then X possesses W holds during Z
(=>
    (hindersSubclass ?PROC1 ?PROC2)
    (forall (?TIME ?PLACE)
        (decreasesLikelihood
            (holdsDuring ?TIME
                (exists (?INST1)
                    (and
                        (instance ?INST1 ?PROC1)
                        (eventLocated ?INST1 ?PLACE))))
            (holdsDuring ?TIME
                (exists (?INST2)
                    (and
                        (instance ?INST2 ?PROC2)
                        (eventLocated ?INST2 ?PLACE)))))))
Merge.kif 4371-4384 If instances of X hinder instances of Y, then For all Entities Z and W: there exists V such that V is an instance of X, V is located at W holds during Z decreases likelihood of there exists U such that U is an instance of Y, and U is located at W holds during Z
(=>
    (preventsSubclass ?PROC1 ?PROC2)
    (forall (?TIME ?PLACE)
        (=>
            (holdsDuring ?TIME
                (exists (?INST1)
                    (and
                        (instance ?INST1 ?PROC1)
                        (eventLocated ?INST1 ?PLACE))))
            (not
                (holdsDuring ?TIME
                    (exists (?INST2)
                        (and
                            (instance ?INST2 ?PROC2)
                            (eventLocated ?INST2 ?PLACE))))))))
Merge.kif 4400-4414 If instances of X prevent instances of Y, then For all TimePosition Z and Entity W: if there exists V such that V is an instance of X and V is located at W holds during Z, then there doesn't exist U such that U is an instance of Y and U is located at W doesn't hold during Z
(=>
    (and
        (prevents ?X ?P)
        (equal
            (WhenFn ?X) ?T)
        (eventLocated ?X ?L))
    (not
        (holdsDuring ?T
            (exists (?Y)
                (and
                    (instance ?Y ?P)
                    (eventLocated ?Y ?L))))))
Merge.kif 4427-4437 If X prevents the occurrence of Y, equal the time of existence of X and Z, and X is located at W, then there doesn't exist V such that V is an instance of Y and V is located at W doesn't hold during Z
(=>
    (hinders ?X ?PROC)
    (exists (?L ?T)
        (decreasesLikelihood
            (and
                (equal
                    (WhenFn ?X) ?T)
                (eventLocated ?X ?L))
            (holdsDuring ?T
                (exists (?Y)
                    (and
                        (instance ?Y ?PROC)
                        (eventLocated ?Y ?L)))))))
Merge.kif 4449-4460 If X hinders Y, then there exist Z, W such that equal the time of existence of X, W, X is located at Z decreases likelihood of there exists V such that V is an instance of Y, and V is located at Z holds during W
(=>
    (frequency ?PROC ?TIME1)
    (forall (?TIME2)
        (=>
            (duration ?TIME2 ?TIME1)
            (exists (?POSITION)
                (and
                    (temporalPart ?POSITION ?TIME2)
                    (holdsDuring ?POSITION
                        (exists (?INST)
                            (instance ?INST ?PROC))))))))
Merge.kif 8022-8032 If X occurs every Y, then For all TimeInterval Z: if duration of Z is Y, then there exists W such that W is a part of Z and there exists V such that V is an instance of X holds during W
(=>
    (and
        (holdsDuring ?TIME1 ?SITUATION)
        (temporalPart ?TIME2 ?TIME1))
    (holdsDuring ?TIME2 ?SITUATION))
Merge.kif 8059-8063 If X holds during Y and Z is a part of Y, then X holds during Z
(=>
    (and
        (instance ?DEATH Death)
        (instance ?ORG Organism)
        (experiencer ?DEATH ?ORG))
    (exists (?REM ?OBJ)
        (and
            (result ?DEATH ?REM)
            (instance ?REM OrganicObject)
            (holdsDuring
                (FutureFn
                    (WhenFn ?DEATH))
                (attribute ?REM Dead))
            (=>
                (holdsDuring
                    (ImmediateFutureFn
                        (WhenFn ?DEATH))
                    (part ?OBJ ?REM))
                (holdsDuring
                    (ImmediatePastFn
                        (WhenFn ?DEATH))
                    (part ?OBJ ?ORG))))))
Merge.kif 10382-10397 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
(=>
    (and
        (instance ?PROC IntentionalProcess)
        (agent ?PROC ?HUMAN)
        (instance ?HUMAN Animal))
    (holdsDuring
        (WhenFn ?PROC)
        (attribute ?HUMAN Awake)))
Merge.kif 10663-10668 If X is an instance of intentional process, Y is an agent of X, and Y is an instance of animal, then awake is an attribute of Y holds during the time of existence of X
(=>
    (and
        (instance ?JOIN JoiningAnOrganization)
        (instance ?ORG Organization)
        (agent ?JOIN ?PERSON)
        (patient ?JOIN ?ORG))
    (and
        (holdsDuring
            (BeginFn
                (WhenFn ?JOIN))
            (not
                (member ?PERSON ?ORG)))
        (holdsDuring
            (EndFn
                (WhenFn ?JOIN))
            (member ?PERSON ?ORG))))
Merge.kif 10736-10744 If X is an instance of joining an organization, Y is an instance of organization, Z is an agent of X, and Y is a patient of X, then Z is not a member of Y holds during the beginning of the time of existence of X and Z is a member of Y holds during the end of the time of existence of X
(=>
    (holdsDuring ?T1
        (expects ?AGENT ?FORMULA))
    (exists (?T2)
        (and
            (holdsDuring ?T1
                (believes ?AGENT
                    (holdsDuring ?T2 ?FORMULA)))
            (earlier ?T1 ?T2))))
Merge.kif 10753-10761 If X expects Y will be true holds during Z, then there exists W such that X believes Y holds during W holds during Z and Z happens earlier than W
(=>
    (and
        (instance ?JOIN Hiring)
        (instance ?ORG Organization)
        (agent ?JOIN ?ORG)
        (patient ?JOIN ?PERSON))
    (and
        (holdsDuring
            (BeginFn
                (WhenFn ?JOIN))
            (not
                (member ?PERSON ?ORG)))
        (holdsDuring
            (EndFn
                (WhenFn ?JOIN))
            (member ?PERSON ?ORG))))
Merge.kif 10768-10776 If X is an instance of hiring, Y is an instance of organization, Y is an agent of X, and Z is a patient of X, then Z is not a member of Y holds during the beginning of the time of existence of X and Z is a member of Y holds during the end of the time of existence of X
(=>
    (and
        (instance ?JOIN Hiring)
        (instance ?ORG Organization)
        (agent ?JOIN ?ORG)
        (patient ?JOIN ?PERSON))
    (holdsDuring
        (ImmediateFutureFn
            (WhenFn ?JOIN))
        (employs ?ORG ?PERSON)))
Merge.kif 10778-10787 If X is an instance of hiring, Y is an instance of organization, Y is an agent of X, and Z is a patient of X, then Y employs Z holds during immediately after the time of existence of X
(=>
    (and
        (instance ?LEAVE LeavingAnOrganization)
        (instance ?ORG Organization)
        (agent ?LEAVE ?PERSON)
        (patient ?LEAVE ?ORG))
    (and
        (holdsDuring
            (BeginFn
                (WhenFn ?LEAVE))
            (member ?PERSON ?ORG))
        (holdsDuring
            (EndFn
                (WhenFn ?LEAVE))
            (not
                (member ?PERSON ?ORG)))))
Merge.kif 10809-10817 If X is an instance of leaving an organization, Y is an instance of organization, Z is an agent of X, and Y is a patient of X, then Z is a member of Y holds during the beginning of the time of existence of X and Z is not a member of Y holds during the end of the time of existence of X
(=>
    (and
        (instance ?LEAVE Quitting)
        (instance ?ORG Organization)
        (agent ?LEAVE ?PERSON)
        (patient ?LEAVE ?ORG))
    (desires ?PERSON
        (holdsDuring
            (EndFn
                (WhenFn ?LEAVE))
            (not
                (member ?PERSON ?ORG)))))
Merge.kif 10823-10833 If X is an instance of quitting, Y is an instance of organization, Z is an agent of X, and Y is a patient of X, then Z desires Z is not a member of Y holds during the end of the time of existence of X
(=>
    (and
        (instance ?LEAVE Firing)
        (instance ?ORG Organization)
        (agent ?LEAVE ?ORG)
        (patient ?LEAVE ?P))
    (and
        (holdsDuring
            (BeginFn
                (WhenFn ?LEAVE))
            (member ?P ?ORG))
        (holdsDuring
            (EndFn
                (WhenFn ?LEAVE))
            (not
                (member ?P ?ORG)))))
Merge.kif 10841-10849 If X is an instance of firing, Y is an instance of organization, Y is an agent of X, and Z is a patient of X, then Z is a member of Y holds during the beginning of the time of existence of X and Z is not a member of Y holds during the end of the time of existence of X

Display limited to 25 items. Show next 25

Display limited to 25 items. Show next 25

statement
-------------------------


(exists (?T)
    (and
        (instance ?T
            (YearFn 2002))
        (holdsDuring ?T
            (coworker SteveJobsOfApple TimCookOfApple))))
ComputingBrands.kif 2441-2445 There exists X such that X is an instance of the year 2002 and Tim Cook is a coworker of Steve Jobs holds during X
(exists (?T)
    (and
        (instance ?T
            (YearFn 1976))
        (holdsDuring ?T
            (coworker SteveJobsOfApple SteveWozniakOfApple))))
ComputingBrands.kif 2453-2457 There exists X such that X is an instance of the year 1976 and Steve Wozniak is a coworker of Steve Jobs holds during X
(exists (?TIME)
    (and
        (instance ?TIME TimeInterval)
        (finishes ?TIME
            (WhenFn JesusOfNazareth))
        (starts ?TIME
            (WhenFn TwelveApostles))
        (forall (?MEM)
            (=>
                (holdsDuring ?TIME
                    (member ?MEM TwelveApostles))
                (holdsDuring ?TIME
                    (friend ?MEM JesusOfNazareth))))))
Media.kif 1972-1980 There exists X such that X is an instance of timeframe, X finishes the time of existence of Jesus of Nazareth, X starts the time of existence of Twelve apostles, and Y Y is a member of Twelve apostles holds during XJesus of Nazareth is a friend of Y holds during X
(equal
    (ReachingMilitaryAgeAnnuallyMaleFn ?AREA ?YEAR)
    (CardinalityFn
        (KappaFn ?PERSON
            (and
                (instance ?PERSON Human)
                (attribute ?PERSON Male)
                (militaryAge ?AREA ?MILITARYAGE)
                (equal ?AGEMINUSONE
                    (SubtractionFn ?AGE 1))
                (holdsDuring ?YEAR
                    (or
                        (age ?PERSON ?AGEMINUSONE)
                        (age ?PERSON ?AGE)))
                (equal ?AGE ?MILITARYAGE)
                (inhabits ?PERSON ?AREA)))))
Military.kif 1195-1208 equal the reaching military age annually male of X, Y, and the number of instances in the class described by Z
(and
    (instance ?YEAR
        (YearFn ?Y))
    (equal
        (ChildrenBornPerWomanFn ?AREA ?YEAR)
        (CardinalityFn
            (KappaFn ?INFANT
                (and
                    (instance ?BIRTH Birth)
                    (experiencer ?BIRTH ?INFANT)
                    (agent ?BIRTH ?WOMAN)
                    (instance ?WOMAN Human)
                    (attribute ?WOMAN Female)
                    (holdsDuring ?YEAR
                        (inhabits ?WOMAN ?AREA)))))))
People.kif 456-469 X is an instance of the year Y and equal the children born per woman of Z, X, and the number of instances in the class described by W

appearance as argument number 0
-------------------------


(holdsDuring
    (ImmediateFutureFn ?TIME)
    (and
        (instance ?TIME
            (YearFn 1996))
        (conventionalLongName "Agency for the French_Speaking Community" AgencyForTheFrenchSpeakingCommunity)))
Government.kif 2746-2750 X is an instance of the year 1996 and agency for the french speaking community is a conventional long name of "Agency for the French_Speaking Community" holds during immediately after X
(holdsDuring
    (ImmediateFutureFn ?T)
    (and
        (instance ?T
            (DayFn 1
                (MonthFn October
                    (YearFn 1992))))
        (conventionalLongName "Andean Community of Nations" AndeanCommunityOfNations)))
Government.kif 2772-2775 X is an instance of the day 1 of month the month October and andean community of nations is a conventional long name of "Andean Community of Nations" holds during immediately after X
(holdsDuring
    (WhenFn JesusOfNazareth)
    (located JesusOfNazareth Palestine))
Media.kif 1922-1922 Jesus of Nazareth is located at palestine holds during the time of existence of Jesus of Nazareth
(holdsDuring
    (FutureFn ?T)
    (and
        (instance Serbia IndependentState)
        (instance ?T
            (DayFn 5
                (MonthFn June
                    (YearFn 2006))))))
Media.kif 2498-2501 Serbia is an instance of independent state and X is an instance of the day 5 of month the month June holds during after X
(holdsDuring
    (FutureFn ?T)
    (and
        (instance Serbia EuropeanNation)
        (instance ?T
            (DayFn 5
                (MonthFn June
                    (YearFn 2006))))))
Media.kif 2503-2506 Serbia is an instance of european nation and X is an instance of the day 5 of month the month June holds during after X
(holdsDuring
    (FutureFn ?T)
    (and
        (names "Republic of Serbia" Serbia)
        (instance ?T
            (DayFn 5
                (MonthFn June
                    (YearFn 2006))))))
Media.kif 2508-2511 Serbia has name "Republic of Serbia" and X is an instance of the day 5 of month the month June holds during after X
(holdsDuring
    (FutureFn ?TIME)
    (and
        (instance ?TIME
            (DayFn 3
                (MonthFn June
                    (YearFn 2006))))
        (instance Montenegro IndependentState)))
Media.kif 2525-2528 X is an instance of the day 3 of month the month June and Montenegro is an instance of independent state holds during after X
(holdsDuring
    (FutureFn ?TIME)
    (and
        (instance ?TIME
            (DayFn 3
                (MonthFn June
                    (YearFn 2006))))
        (instance Montenegro EuropeanNation)))
Media.kif 2530-2533 X is an instance of the day 3 of month the month June and Montenegro is an instance of european nation holds during after X
(holdsDuring
    (FutureFn ?TIME)
    (and
        (instance ?TIME
            (DayFn 3
                (MonthFn June
                    (YearFn 2006))))
        (names "Montenegro" Montenegro)))
Media.kif 2535-2538 X is an instance of the day 3 of month the month June and Montenegro has name "Montenegro" holds during after X
(holdsDuring
    (FutureFn ?TIME)
    (and
        (instance ?TIME
            (DayFn 3
                (MonthFn June
                    (YearFn 2006))))
        (not
            (instance SerbiaAndMontenegro IndependentState))))
Media.kif 2548-2552 X is an instance of the day 3 of month the month June and serbia and montenegro is not an instance of independent state holds during after X


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