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



KB Term:  Term intersection
English Word: 

Sigma KEE - WhenFn
WhenFn

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


(instance WhenFn TemporalRelation) Merge.kif 8667-8667 When is an instance of temporal relation
(instance WhenFn UnaryFunction) Merge.kif 8668-8668 When is an instance of unary function
(instance WhenFn TotalValuedRelation) Merge.kif 8669-8669 When is an instance of total valued relation
(domain WhenFn 1 Physical) Merge.kif 8670-8670 The number 1 argument of when is an instance of physical
(range WhenFn TimeInterval) Merge.kif 8671-8671 The range of when is an instance of timeframe
(documentation WhenFn EnglishLanguage "A UnaryFunction that maps an Object or Process to the exact TimeInterval during which it exists. Note that, for every TimePoint ?TIME outside of the TimeInterval (WhenFn ?THING), (time ?THING ?TIME) does not hold.") Merge.kif 8673-8676 The range of when is an instance of timeframe

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


(relatedInternalConcept WhereFn WhenFn) Merge.kif 4340-4340 Where is internally related to when
(termFormat EnglishLanguage WhenFn "when") domainEnglishFormat.kif 62986-62986 Where is internally related to when
(termFormat ChineseTraditionalLanguage WhenFn "何時") domainEnglishFormat.kif 62987-62987 Where is internally related to when
(termFormat ChineseLanguage WhenFn "何时") domainEnglishFormat.kif 62988-62988 Where is internally related to when
(format EnglishLanguage WhenFn "the time of existence of %1") english_format.kif 461-461 Where is internally related to when

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


(=>
    (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 4489-4499 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
(=>
    (temporalPart ?POS
        (WhenFn ?THING))
    (time ?THING ?POS))
Merge.kif 8143-8146 If X is a part of the time of existence of Y, then Y exists during X
(=>
    (and
        (resource ?PROC ?OBJ)
        (holdsDuring
            (BeginFn
                (WhenFn ?PROC))
            (measure ?OBJ ?QUANT1))
        (holdsDuring
            (EndFn
                (WhenFn ?PROC))
            (measure ?OBJ ?QUANT2)))
    (greaterThan ?QUANT1 ?QUANT2))
Merge.kif 8199-8204 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
(=>
    (temporallyBetweenOrEqual
        (BeginFn
            (WhenFn ?PHYS)) ?TIME
        (EndFn
            (WhenFn ?PHYS)))
    (and
        (time ?PHYS ?TIME)
        (instance ?TIME TimePoint)))
Merge.kif 8414-8423 If X is between or at the beginning of the time of existence of Y and the end of the time of existence of Y, then Y exists during X and X is an instance of time point
(=>
    (equal
        (WhenFn ?PHYS1)
        (WhenFn ?PHYS2))
    (cooccur ?PHYS1 ?PHYS2))
Merge.kif 8604-8606 If equal the time of existence of X and the time of existence of Y, then X occurs at the same time as Y
(=>
    (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 11410-11418 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 11545-11553 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 11923-11930 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
            (WhenFn ?DISCOVERING))
        (knows ?A
            (located ?OBJ ?PLACE))))
Merge.kif 12256-12268 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 the time of existence of 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 12671-12685 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 12721-12730 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
        (patient ?PROCESS ?PATIENT)
        (time ?PATIENT
            (EndFn
                (WhenFn ?PROCESS)))
        (not
            (time ?PATIENT
                (BeginFn
                    (WhenFn ?PROCESS)))))
    (instance ?PROCESS Creation))
Merge.kif 13094-13100 If X is a patient of Y, X exists during the end of the time of existence of Y, and X doesn't exist during the beginning of the time of existence of Y, then Y is an instance of creation
(=>
    (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 14140-14148 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
        (holdsDuring ?TIME
            (attribute ?ORG Larval))
        (instance ?BIRTH Birth)
        (equal ?BW
            (WhenFn ?BIRTH))
        (experiencer ?BIRTH ?ORG))
    (meetsTemporally ?BW ?TIME))
Merge.kif 18522-18528 If larval is an attribute of X holds during Y, Z is an instance of birth, equal W and the time of existence of Z, and X experiences Z, then W meets Y
(=>
    (and
        (holdsDuring ?TIME
            (attribute ?ORG Embryonic))
        (instance ?BIRTH Birth)
        (equal ?BW
            (WhenFn ?BIRTH))
        (experiencer ?BIRTH ?ORG))
    (not
        (overlapsTemporally ?TIME ?BW)))
Merge.kif 18544-18550 If embryonic is an attribute of X holds during Y, Z is an instance of birth, equal W and the time of existence of Z, and X experiences Z, then W doesn't overlap Y
(=>
    (and
        (instance ?REM OrganismRemains)
        (holdsDuring
            (WhenFn ?REM)
            (part ?OBJ ?REM)))
    (exists (?ORG)
        (and
            (instance ?ORG Organism)
            (earlier
                (WhenFn ?ORG)
                (WhenFn ?REM))
            (finishes
                (WhenFn ?REM)
                (WhenFn ?ORG))
            (holdsDuring
                (WhenFn ?ORG)
                (part ?OBJ ?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
(=>
    (and
        (instance ?D Dodging)
        (agent ?D ?A)
        (equal ?DT
            (WhenFn ?D)))
    (hasPurpose ?D
        (not
            (exists (?I)
                (and
                    (or
                        (meetsTemporally ?DT
                            (WhenFn ?I))
                        (overlapsTemporally ?DT
                            (WhenFn ?I)))
                    (instance ?I Impacting)
                    (patient ?I ?A))))))
Mid-level-ontology.kif 433-446 If X is an instance of dodging, Y is an agent of X, and equal Z and the time of existence of X, then X has the purpose there doesn't exist W such that Z meets the time of existence of W or the time of existence of W overlaps Z, W is an instance of impacting, and Y is a patient of W
(=>
    (and
        (instance ?AMBULATE Ambulating)
        (equal ?DURATION
            (WhenFn ?AMBULATE)))
    (exists (?STEP1 ?STEPN)
        (and
            (instance ?STEP1 Stepping)
            (instance ?STEPN Stepping)
            (subProcess ?STEP1 ?AMBULATE)
            (subProcess ?STEPN ?AMBULATE)
            (starts
                (WhenFn ?STEP1) ?DURATION)
            (finishes
                (WhenFn ?STEPN) ?DURATION)
            (not
                (equal ?STEP1 ?STEPN)))))
Mid-level-ontology.kif 470-482 If X is an instance of ambulating and equal Y and the time of existence of X, then All of the following hold: (1) there exist Z (2) W such that Z is an instance of stepping (3) W is an instance of stepping (4) Z is a subprocess of X (5) W is a subprocess of X (6) the time of existence of Z starts Y (7) the time of existence of W finishes Y (8) equal Z (9) W
(=>
    (and
        (instance ?A Ambulating)
        (subProcess ?S1 ?A)
        (instance ?S1 Stepping)
        (subProcess ?S2 ?A)
        (instance ?S2 Stepping)
        (equal ?S1START
            (BeginFn
                (WhenFn ?S1)))
        (equal ?S2START
            (BeginFn
                (WhenFn ?S2)))
        (not
            (or
                (before ?S1START ?S2START)
                (before ?S2START ?S1START))))
    (equal ?S1 ?S2))
Mid-level-ontology.kif 484-497 If All of the following hold: (1) X is an instance of ambulating (2) Y is a subprocess of X (3) Y is an instance of stepping (4) Z is a subprocess of X (5) Z is an instance of stepping (6) equal W and the beginning of the time of existence of Y (7) equal V and the beginning of the time of existence of Z (8) ~{ W happens before V } and ~{ V happens before W }, then equal Y and Z
(=>
    (and
        (instance ?SCO SelfConnectedObject)
        (instance ?C Compressing)
        (patient ?C ?SCO)
        (holdsDuring
            (ImmediatePastFn
                (WhenFn ?C))
            (measure ?SCO
                (MeasureFn ?N1 ?V)))
        (instance ?V UnitOfVolume)
        (holdsDuring
            (ImmediateFutureFn
                (WhenFn ?C))
            (measure ?SCO
                (MeasureFn ?N2 ?V))))
    (greaterThan ?N1 ?N2))
Mid-level-ontology.kif 4181-4193 If All of the following hold: (1) X is an instance of self connected object (2) Y is an instance of compressing (3) X is a patient of Y (4) the measure of X is Z W(s) holds during immediately before the time of existence of Y (5) W is an instance of unit of volume (6) the measure of X is V W(s) holds during immediately after the time of existence of Y, then Z is greater than V
(=>
    (and
        (instance ?I Ingesting)
        (experiencer ?I ?H)
        (objectTransferred ?I ?MS)
        (instance ?MS MoodStabilizer)
        (instance ?E ?EC)
        (involvedInEvent ?E ?H)
        (holdsDuring
            (WhenFn ?E)
            (attribute ?H ?ES))
        (instance ?ES EmotionalState)
        (instance ?E2 ?EC)
        (involvedInEvent ?E2 ?H)
        (earlier
            (WhenFn ?E2)
            (WhenFn ?I)))
    (modalAttribute
        (not
            (holdsDuring ?E2
                (attribute ?H ?ES))) Unlikely))
Mid-level-ontology.kif 11219-11240 If All of the following hold: (1) X is an instance of ingesting (2) Y experiences X (3) the object transferred in X is Z (4) Z is an instance of mood stabilizer (5) W is an instance of V (6) Y is an involved in event of W (7) U is an attribute of Y holds during the time of existence of W (8) U is an instance of emotional state (9) T is an instance of V (10) Y is an involved in event of T (11) the time of existence of T happens earlier than the time of existence of X, then the statement U is not an attribute of Y doesn't hold during T has the modal force of unlikely
(=>
    (and
        (instance ?A Antacid)
        (instance ?I Ingesting)
        (agent ?I ?H)
        (moves ?I ?A)
        (instance ?S Stomach)
        (part ?S ?H)
        (holdsDuring
            (ImmediatePastFn
                (WhenFn ?I))
            (and
                (contains ?S ?F1)
                (instance ?F1 Fluid)))
        (holdsDuring
            (ImmediateFutureFn
                (WhenFn ?I))
            (and
                (contains ?S ?F2)
                (instance ?F2 Fluid)))
        (phMeasure ?F1 ?N1)
        (phMeasure ?F2 ?N2))
    (greaterThan ?N2 ?N1))
Mid-level-ontology.kif 11284-11306 If All of the following hold: (1) X is an instance of antacid (2) Y is an instance of ingesting (3) Z is an agent of Y (4) X moves during Y (5) W is an instance of stomach (6) W is a part of Z (7) W contains V and V is an instance of fluid holds during immediately before the time of existence of Y (8) W contains U and U is an instance of fluid holds during immediately after the time of existence of Y (9) pH measure V and T (10) pH measure U and S, then S is greater than T
(=>
    (and
        (instance ?A ProtonPumpInhibitor)
        (instance ?I Ingesting)
        (agent ?I ?H)
        (moves ?I ?A)
        (instance ?S Stomach)
        (part ?S ?H)
        (holdsDuring
            (ImmediatePastFn
                (WhenFn ?I))
            (and
                (contains ?S ?F1)
                (instance ?F1 Fluid)))
        (holdsDuring
            (ImmediateFutureFn
                (WhenFn ?I))
            (and
                (contains ?S ?F2)
                (instance ?F2 Fluid)))
        (phMeasure ?F1 ?N1)
        (phMeasure ?F2 ?N2))
    (greaterThan ?N2 ?N1))
Mid-level-ontology.kif 11345-11367 If All of the following hold: (1) X is an instance of PPI (2) Y is an instance of ingesting (3) Z is an agent of Y (4) X moves during Y (5) W is an instance of stomach (6) W is a part of Z (7) W contains V and V is an instance of fluid holds during immediately before the time of existence of Y (8) W contains U and U is an instance of fluid holds during immediately after the time of existence of Y (9) pH measure V and T (10) pH measure U and S, then S is greater than T
(=>
    (and
        (instance ?MC MuscularContraction)
        (patient ?MC ?M)
        (instance ?M Muscle)
        (holdsDuring
            (ImmediatePastFn
                (WhenFn ?MC))
            (length ?M
                (MeasureFn ?N1 ?U)))
        (holdsDuring
            (ImmediateFutureFn
                (WhenFn ?MC))
            (length ?M
                (MeasureFn ?N2 ?U))))
    (greaterThan ?N1 ?N2))
Mid-level-ontology.kif 11986-12001 If X is an instance of muscular contraction, Y is a patient of X, Y is an instance of muscle, the length of Y is Z W(s) holds during immediately before the time of existence of X, and the length of Y is V W(s) holds during immediately after the time of existence of X, then Z is greater than V
(=>
    (and
        (instance ?MC MuscleRelaxing)
        (patient ?MC ?M)
        (instance ?M Muscle)
        (holdsDuring
            (ImmediatePastFn
                (WhenFn ?MC))
            (length ?M
                (MeasureFn ?N1 ?U)))
        (holdsDuring
            (ImmediateFutureFn
                (WhenFn ?MC))
            (length ?M
                (MeasureFn ?N2 ?U))))
    (greaterThan ?N2 ?N1))
Mid-level-ontology.kif 12008-12023 If X is an instance of muscle relaxing, Y is a patient of X, Y is an instance of muscle, the length of Y is Z W(s) holds during immediately before the time of existence of X, and the length of Y is V W(s) holds during immediately after the time of existence of X, then V is greater than Z

Display limited to 25 items. Show next 25

Display limited to 25 items. Show next 25

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


(=>
    (and
        (resourceExhausted ?P ?R)
        (instance ?R ?C))
    (holdsDuring
        (ImmediateFutureFn
            (WhenFn ?P))
        (not
            (exists (?OBJ1)
                (and
                    (part ?OBJ1 ?R)
                    (instance ?OBJ1 ?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
(=>
    (causes ?P1 ?P2)
    (earlier
        (WhenFn ?P1)
        (WhenFn ?P2)))
Merge.kif 3901-3903 If X causes Y, then the time of existence of X happens earlier than the time of existence of Y
(=>
    (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 4511-4522 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
(=>
    (and
        (instance ?TIME TimePoint)
        (holdsDuring ?TIME
            (age ?OBJ ?DURATION)))
    (duration
        (TimeIntervalFn
            (BeginFn
                (WhenFn ?OBJ)) ?TIME) ?DURATION))
Merge.kif 7662-7666 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
(=>
    (time ?THING ?POS)
    (temporalPart ?POS
        (WhenFn ?THING)))
Merge.kif 8148-8151 If X exists during Y, then Y is a part of the time of existence of X
(=>
    (origin ?PROCESS ?OBJ)
    (eventLocated
        (WhereFn ?PROCESS
            (BeginFn
                (WhenFn ?PROCESS)))
        (WhereFn ?OBJ
            (BeginFn
                (WhenFn ?OBJ)))))
Merge.kif 8162-8170 If X originates at Y, then the place where X was at the beginning of the time of existence of X is located at the place where Y was at the beginning of the time of existence of Y
(=>
    (result ?PROC ?OBJ)
    (forall (?TIME)
        (=>
            (before ?TIME
                (BeginFn
                    (WhenFn ?PROC)))
            (not
                (time ?OBJ ?TIME)))))
Merge.kif 8326-8332 If X is a result of Y, then For all TimePoint Z: if Z happens before the beginning of the time of existence of Y, then X doesn't exist during Z
(=>
    (and
        (time ?PHYS ?TIME)
        (instance ?TIME TimePoint))
    (temporallyBetweenOrEqual
        (BeginFn
            (WhenFn ?PHYS)) ?TIME
        (EndFn
            (WhenFn ?PHYS))))
Merge.kif 8408-8412 If X exists during Y and Y is an instance of time point, then Y is between or at the beginning of the time of existence of X and the end of the time of existence of X
(=>
    (and
        (instance ?REL BinaryPredicate)
        (instance ?REL SpatialRelation)
        (instance ?OBJ1 Physical)
        (instance ?OBJ2 Physical)
        (?REL ?OBJ1 ?OBJ2))
    (overlapsTemporally
        (WhenFn ?OBJ1)
        (WhenFn ?OBJ2)))
Merge.kif 8451-8458 If X is an instance of binary predicate, X is an instance of spatial relation, Y is an instance of physical, Z is an instance of physical, and X Y and Z, then the time of existence of Z overlaps the time of existence of Y
(=>
    (cooccur ?PHYS1 ?PHYS2)
    (equal
        (WhenFn ?PHYS1)
        (WhenFn ?PHYS2)))
Merge.kif 8600-8602 If X occurs at the same time as Y, then equal the time of existence of X and the time of existence of Y
(=>
    (subProcess ?SUBPROC ?PROC)
    (temporalPart
        (WhenFn ?SUBPROC)
        (WhenFn ?PROC)))
Merge.kif 10333-10335 If X is a subprocess of Y, then the time of existence of X is a part of the time of existence of Y
(=>
    (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 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
(=>
    (and
        (instance ?DIGEST Digesting)
        (agent ?DIGEST ?ORGANISM))
    (exists (?INGEST)
        (and
            (instance ?INGEST Ingesting)
            (agent ?INGEST ?ORGANISM)
            (overlapsTemporally
                (WhenFn ?INGEST)
                (WhenFn ?DIGEST)))))
Merge.kif 10536-10544 If X is an instance of digesting and Y is an agent of X, then there exists Z such that Z is an instance of ingesting, Y is an agent of Z, and the time of existence of X overlaps the time of existence of Z
(=>
    (and
        (instance ?PROC IntentionalProcess)
        (agent ?PROC ?HUMAN)
        (instance ?HUMAN Animal))
    (holdsDuring
        (WhenFn ?PROC)
        (attribute ?HUMAN Awake)))
Merge.kif 10750-10755 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 10824-10832 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
(=>
    (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 10857-10865 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 10867-10876 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 ?JOIN Hiring)
        (instance ?ORG Organization)
        (agent ?JOIN ?ORG)
        (patient ?JOIN ?PERSON))
    (expects ?ORG
        (exists (?FT)
            (and
                (instance ?FT FinancialTransaction)
                (agent ?FT ?ORG)
                (destination ?FT ?PERSON)
                (earlier
                    (WhenFn ?JOIN)
                    (WhenFn ?FT))))))
Merge.kif 10878-10890 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 expects there exists W such that W is an instance of financial transaction, Y is an agent of W, W ends up at Z, and the time of existence of X happens earlier than the time of existence of W will be true
(=>
    (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 10898-10906 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 10912-10922 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 10930-10938 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
(=>
    (and
        (instance ?HIRE Hiring)
        (instance ?ORG Organization)
        (agent ?HIRE ?ORG)
        (patient ?HIRE ?PERSON))
    (and
        (holdsDuring
            (BeginFn
                (WhenFn ?HIRE))
            (not
                (employs ?ORG ?PERSON)))
        (holdsDuring
            (EndFn
                (WhenFn ?HIRE))
            (employs ?ORG ?PERSON))))
Merge.kif 10971-10979 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 doesn't employ Z holds during the beginning of the time of existence of X and Y employs Z holds during the end of the time of existence of X
(=>
    (and
        (instance ?FIRE TerminatingEmployment)
        (instance ?ORG Organization)
        (agent ?FIRE ?ORG)
        (patient ?FIRE ?PERSON))
    (and
        (holdsDuring
            (BeginFn
                (WhenFn ?FIRE))
            (employs ?ORG ?PERSON))
        (holdsDuring
            (EndFn
                (WhenFn ?FIRE))
            (not
                (employs ?ORG ?PERSON)))))
Merge.kif 10987-10995 If X is an instance of terminating employment, 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 the beginning of the time of existence of X and Y doesn't employ Z holds during the end of the time of existence of X
(=>
    (instance ?DECISION LegalDecision)
    (exists (?DECIDE ?LD)
        (and
            (instance ?DECIDE Deciding)
            (result ?DECIDE ?LD)
            (instance ?DECISION ?LD)
            (earlier
                (WhenFn ?DECIDE)
                (WhenFn ?DECISION)))))
Merge.kif 11048-11055 If X is an instance of legal decision, then there exist Y, Z such that Y is an instance of deciding, Z is a result of Y, X is an instance of Z, and the time of existence of Y happens earlier than the time of existence of X
(=>
    (and
        (instance ?INTERPRET Interpreting)
        (agent ?INTERPRET ?AGENT)
        (patient ?INTERPRET ?CONTENT)
        (instance ?CONTENT ContentBearingObject))
    (exists (?PROP)
        (holdsDuring
            (EndFn
                (WhenFn ?INTERPRET))
            (believes ?AGENT
                (containsInformation ?CONTENT ?PROP)))))
Merge.kif 11110-11122 If X is an instance of interpreting, Y is an agent of X, Z is a patient of X, and Z is an instance of content bearing object, then there exists W such that Y believes Z contains information W 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
-------------------------


(holdsDuring
    (WhenFn JesusOfNazareth)
    (located JesusOfNazareth Palestine))
Media.kif 1867-1867 Jesus of Nazareth is located at palestine holds during the time of existence of Jesus of Nazareth
(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 1917-1925 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


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.0-0a80e6c8 (2026-05-12) is open source software produced by Articulate Software and its partners