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


KB Term:  Term intersection
English Word: 

Sigma KEE - finishes
finishes

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


(subrelation finishes temporalPart) Merge.kif 8238-8238 finishes is a subrelation of temporal part
(instance finishes TemporalRelation) Merge.kif 8239-8239 finishes is an instance of temporal relation
(instance finishes TransitiveRelation) Merge.kif 8240-8240 finishes is an instance of transitive relation
(instance finishes IrreflexiveRelation) Merge.kif 8241-8241 finishes is an instance of irreflexive relation
(instance finishes TotalValuedRelation) Merge.kif 8242-8242 finishes is an instance of total valued relation
(domain finishes 1 TimeInterval) Merge.kif 8243-8243 The number 1 argument of finishes is an instance of timeframe
(domain finishes 2 TimeInterval) Merge.kif 8244-8244 The number 2 argument of finishes is an instance of timeframe
(documentation finishes EnglishLanguage "(finishes ?INTERVAL1 ?INTERVAL2) means that ?INTERVAL1 and ?INTERVAL2 are both TimeIntervals that have the same ending TimePoint and that ?INTERVAL2 begins before ?INTERVAL1.") Merge.kif 8246-8248 The number 2 argument of finishes is an instance of timeframe

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


(termFormat EnglishLanguage finishes "finishes") domainEnglishFormat.kif 23872-23872
(termFormat ChineseTraditionalLanguage finishes "飾面") domainEnglishFormat.kif 23873-23873
(termFormat ChineseLanguage finishes "饰面") domainEnglishFormat.kif 23874-23874
(format EnglishLanguage finishes "%1 %n{doesn't} finish%p{es} %2") english_format.kif 427-427

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


(=>
    (finishes ?INTERVAL1 ?INTERVAL2)
    (and
        (before
            (BeginFn ?INTERVAL2)
            (BeginFn ?INTERVAL1))
        (equal
            (EndFn ?INTERVAL2)
            (EndFn ?INTERVAL1))))		 Merge.kif 8250-8258 If X finishes Y, then the beginning of Y happens before the beginning of X and equal the end of Y and the end of X
(<=>
    (and
        (agreementPeriod ?Account ?Period)
        (finishes ?End ?Period))
    (maturityDate ?Account ?End))		 FinancialOntology.kif 663-667 X is an agreement period of Y, Z finishes X if, and only if Z is a maturity date of Y
(=>
    (and
        (instance ?Y Year)
        (instance ?E EasterSunday)
        (instance ?P PalmSunday)
        (during ?E ?Y)
        (during ?P ?Y)
        (starts ?P ?I)
        (finishes ?E ?I))
    (duration ?I
        (MeasureFn 8 DayDuration)))		 Media.kif 467-476 If All of the following hold: (1) X is an instance of year (2) Y is an instance of Easter sunday (3) Z is an instance of palm sunday (4) Y takes place during X (5) Z takes place during X (6) Z starts W (7) Y finishes W, then duration of W is 8 day duration(s)
(=>
    (and
        (instance ?Y Year)
        (instance ?E EasterSunday)
        (instance ?A AscensionThursday)
        (during ?E ?Y)
        (during ?A ?Y)
        (starts ?E ?I)
        (finishes ?A ?I))
    (duration ?I
        (MeasureFn 40 DayDuration)))		 Media.kif 532-541 If All of the following hold: (1) X is an instance of year (2) Y is an instance of Easter sunday (3) Z is an instance of ascension thursday (4) Y takes place during X (5) Z takes place during X (6) Y starts W (7) Z finishes W, then duration of W is 40 day duration(s)
(=>
    (and
        (instance ?Y Year)
        (instance ?E EasterSunday)
        (instance ?P Pentecost)
        (during ?E ?Y)
        (during ?P ?Y)
        (starts ?E ?I)
        (finishes ?P ?I))
    (duration ?I
        (MeasureFn 50 DayDuration)))		 Media.kif 553-562 If All of the following hold: (1) X is an instance of year (2) Y is an instance of Easter sunday (3) Z is an instance of Pentecost (4) Y takes place during X (5) Z takes place during X (6) Y starts W (7) Z finishes W, then duration of W is 50 day duration(s)
(=>
    (and
        (dependencyDelay ?Program1 ?Delay)
        (dependencyType ?Program1 ShutdownBlock)
        (hasDependency ?Program1 ?Program2)
        (instance ?Process1 ComputerProcess)
        (programRunning ?Process1 ?Program1)
        (instance ?Process2 ComputerProcess)
        (programRunning ?Process2 ?Program2)
        (equal
            (WhenFn ?Process2) ?Time2)
        (finishes ?Time ?Time1)
        (equal
            (WhenFn ?Process2) ?Time2)
        (equal
            (BeginFn ?Time)
            (EndFn ?Time2)))
    (duration ?Time ?Delay))		 QoSontology.kif 1369-1386 If All of the following hold: (1) X is a dependency delay of Y (2) shutdown block is a dependency type of Y (3) Z has a dependency on Y (4) W is an instance of computer process (5) Y is a program running of W (6) V is an instance of computer process (7) Z is a program running of V (8) equal the time of existence of V and U (9) T finishes S (10) equal the time of existence of V and U (11) equal the beginning of T and the end of U, then duration of T is X

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


(=>
    (and
        (before
            (BeginFn ?INTERVAL2)
            (BeginFn ?INTERVAL1))
        (equal
            (EndFn ?INTERVAL2)
            (EndFn ?INTERVAL1)))
    (finishes ?INTERVAL1 ?INTERVAL2))		 Merge.kif 8260-8268 If the beginning of X happens before the beginning of Y and equal the end of X and the end of Y, then Y finishes X
(=>
    (instance ?INTERVAL
        (RecurrentTimeIntervalFn ?TIMECLASS1 ?TIMECLASS2))
    (exists (?TIME1 ?TIME2)
        (and
            (instance ?TIME1 ?TIMECLASS1)
            (instance ?TIME2 ?TIMECLASS2)
            (starts ?TIME1 ?INTERVAL)
            (finishes ?TIME2 ?INTERVAL))))		 Merge.kif 8658-8665 If X is an instance of the recurring period from Y to Z, then there exist W, V such that W is an instance of Y, V is an instance of Z, W starts X, and V finishes X
(=>
    (instance ?INTERVAL TimeInterval)
    (finishes
        (ImmediatePastFn ?INTERVAL)
        (PastFn ?INTERVAL)))		 Merge.kif 8706-8708 If X is an instance of timeframe, then immediately before X finishes before X
(=>
    (instance ?MORNING Morning)
    (exists (?HOUR ?DAY)
        (and
            (instance ?HOUR
                (HourFn 12 ?DAY))
            (finishes ?HOUR ?MORNING))))		 Merge.kif 9009-9015 If X is an instance of morning, then there exist Y, Z such that Y is an instance of the hour 12, and Y finishes X
(=>
    (instance ?DAY DayTime)
    (exists (?RISE ?SET)
        (and
            (instance ?RISE Sunrise)
            (instance ?SET Sunset)
            (starts ?RISE ?DAY)
            (finishes ?SET ?DAY))))		 Merge.kif 9081-9088 If X is an instance of day time, then there exist Y, Z such that Y is an instance of sunrise, Z is an instance of sunset, Y starts X, and Z finishes X
(=>
    (instance ?NIGHT NightTime)
    (exists (?RISE ?SET)
        (and
            (instance ?RISE Sunrise)
            (instance ?SET Sunset)
            (starts ?SET ?NIGHT)
            (finishes ?RISE ?NIGHT))))		 Merge.kif 9103-9110 If X is an instance of night time, then there exist Y, Z such that Y is an instance of sunrise, Z is an instance of sunset, Z starts X, and Y finishes X
(=>
    (and
        (instance ?S Saturday)
        (instance ?W Week)
        (during ?S ?W))
    (finishes ?S ?W))		 Merge.kif 9558-9563 If X is an instance of Saturday, Y is an instance of week, and X takes place during Y, then X finishes Y
(=>
    (equal
        (TemporalCompositionFn ?INTERVAL ?INTERVALTYPE) ?CLASS)
    (exists (?TIME)
        (and
            (instance ?TIME ?CLASS)
            (finishes ?TIME ?INTERVAL))))		 Merge.kif 9641-9646 If equal decomposition of X into Y and Z, then there exists W such that W is an instance of Z and W finishes X
(=>
    (equal
        (TemporalCompositionFn ?INTERVAL ?INTERVALTYPE) ?CLASS)
    (forall (?TIME1)
        (=>
            (and
                (instance ?TIME1 ?CLASS)
                (not
                    (finishes ?TIME1 ?INTERVAL)))
            (exists (?TIME2)
                (and
                    (instance ?TIME2 ?CLASS)
                    (meetsTemporally ?TIME1 ?TIME2))))))		 Merge.kif 9648-9658 If equal decomposition of X into Y and Z, then For all TimeInterval W: if W doesn't finish X, then there exists V such that V is an instance of Z and W meets V
(=>
    (and
        (instance ?T1 Translocation)
        (instance ?T2 Translocation)
        (origin ?T1 ?O1)
        (origin ?T2 ?D1)
        (destination ?T1 ?D1)
        (destination ?T2 ?D2)
        (experiencer ?T1 ?P)
        (experiencer ?T2 ?P))
    (exists (?T)
        (and
            (instance ?T Translocation)
            (origin ?T ?O1)
            (destination ?T ?D2)
            (subProcess ?T1 ?T)
            (subProcess ?T2 ?T)
            (experiencer ?T ?P)
            (starts
                (WhenFn ?T1)
                (WhenFn ?T))
            (finishes
                (WhenFn ?T2)
                (WhenFn ?T)))))		 Merge.kif 11586-11609 If All of the following hold: (1) X is an instance of translocation (2) Y is an instance of translocation (3) X originates at Z (4) Y originates at W (5) X ends up at W (6) Y ends up at V (7) U experiences X (8) U experiences Y, then All of the following hold: (1) there exists T such that T is an instance of translocation (2) T originates at Z (3) T ends up at V (4) X is a subprocess of T (5) Y is a subprocess of T (6) U experiences T (7) the time of existence of X starts the time of existence of T (8) the time of existence of Y finishes the time of existence of T
(=>
    (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
(=>
    (instance ?S
        (StopFn ?P))
    (exists (?I)
        (and
            (instance ?I ?P)
            (finishes
                (WhenFn ?S)
                (WhenFn ?I)))))		 Mid-level-ontology.kif 421-426 If X is an instance of the stop of Y, then there exists Z such that Z is an instance of Y and the time of existence of X finishes the time of existence of Z
(=>
    (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
(=>
    (instance ?D Divorcing)
    (exists (?P1 ?P2 ?T1 ?T2)
        (and
            (holdsDuring ?T1
                (spouse ?P1 ?P2))
            (holdsDuring ?T2
                (not
                    (spouse ?P1 ?P2)))
            (finishes ?T1 ?D)
            (starts ?T2 ?D))))		 Mid-level-ontology.kif 1015-1024 If X is an instance of divorcing, then there exist Y, Z,, , W, V such that Y is the spouse of Z holds during W, Y is the spouse of Z holds during V, W finishes X, and V starts X
(=>
    (and
        (instance ?OP CeasingOperations)
        (instance ?ORG Organization)
        (agent ?OP ?ORG))
    (finishes ?OP
        (WhenFn ?ORG)))		 Mid-level-ontology.kif 17964-17969 If X is an instance of ceasing operations, Y is an instance of organization, and Y is an agent of X, then X finishes the time of existence of Y
(=>
    (and
        (instance ?FALL FallingAsleep)
        (experiencer ?FALL ?AGENT))
    (exists (?START ?FINISH)
        (and
            (starts ?START
                (WhenFn ?FALL))
            (finishes ?FINISH
                (WhenFn ?FALL))
            (holdsDuring ?START
                (attribute ?AGENT Awake))
            (holdsDuring ?FINISH
                (attribute ?AGENT Asleep)))))		 Mid-level-ontology.kif 18013-18022 If X is an instance of falling asleep and Y experiences X, then there exist Z, W such that Z starts the time of existence of X, W finishes the time of existence of X, awake is an attribute of Y holds during Z, and asleep is an attribute of Y holds during W
(=>
    (and
        (instance ?WAKE WakingUp)
        (experiencer ?WAKE ?AGENT))
    (exists (?START ?FINISH)
        (and
            (starts ?START
                (WhenFn ?WAKE))
            (finishes ?FINISH
                (WhenFn ?WAKE))
            (holdsDuring ?START
                (attribute ?AGENT Asleep))
            (holdsDuring ?FINISH
                (attribute ?AGENT Awake)))))		 Mid-level-ontology.kif 18028-18037 If X is an instance of waking up and Y experiences X, then there exist Z, W such that Z starts the time of existence of X, W finishes the time of existence of X, asleep is an attribute of Y holds during Z, and awake is an attribute of Y holds during W
(=>
    (instance ?ARRIVE Arriving)
    (exists (?GO)
        (and
            (instance ?GO Translocation)
            (subProcess ?ARRIVE ?GO)
            (finishes
                (WhenFn ?ARRIVE)
                (WhenFn ?GO)))))		 Mid-level-ontology.kif 19150-19156 If X is an instance of arriving, then there exists Y such that Y is an instance of translocation, X is a subprocess of Y, and the time of existence of X finishes the time of existence of Y
(=>
    (instance ?AM AnteMeridiem)
    (exists (?D ?HOUR1 ?HOUR2)
        (and
            (instance ?HOUR1
                (HourFn 0 ?D))
            (starts ?HOUR1 ?AM)
            (instance ?HOUR2
                (HourFn 12 ?D))
            (finishes ?HOUR2 ?AM))))		 Mid-level-ontology.kif 21032-21039 If X is an instance of ante meridiem, then there exist Y, Z, W such that Z is an instance of the hour 0, Z starts X, W is an instance of the hour 12, and W finishes X
(=>
    (instance ?PM PostMeridiem)
    (exists (?D ?HOUR1 ?HOUR2)
        (and
            (instance ?HOUR1
                (HourFn 12 ?D))
            (starts ?HOUR1 ?PM)
            (instance ?HOUR2
                (HourFn 23 ?D))
            (finishes ?HOUR2 ?PM))))		 Mid-level-ontology.kif 21046-21053 If X is an instance of post meridiem, then there exist Y, Z, W such that Z is an instance of the hour 12, Z starts X, W is an instance of the hour 23, and W finishes X
(=>
    (instance ?WEEKEND Weekend)
    (exists (?SATURDAY ?SUNDAY)
        (and
            (instance ?SATURDAY Saturday)
            (instance ?SUNDAY Sunday)
            (starts ?SATURDAY ?WEEKEND)
            (finishes ?SUNDAY ?WEEKEND)
            (meetsTemporally ?SATURDAY ?SUNDAY))))		 Mid-level-ontology.kif 21058-21066 If X is an instance of weekend, then there exist Y, Z such that Y is an instance of Saturday, Z is an instance of Sunday, Y starts X, Z finishes X, and Y meets Z
(=>
    (instance ?NEGOTIATE Negotiating)
    (hasPurpose ?NEGOTIATE
        (exists (?COMMIT)
            (and
                (instance ?COMMIT Committing)
                (subProcess ?COMMIT ?NEGOTIATE)
                (finishes
                    (WhenFn ?COMMIT)
                    (WhenFn ?NEGOTIATE))))))		 Mid-level-ontology.kif 21613-21622 If X is an instance of negotiating, then X has the purpose there exists Y such that Y is an instance of committing, Y is a subprocess of X, and the time of existence of Y finishes the time of existence of X
(=>
    (and
        (meatOfAnimal ?MEAT ?ANIMAL)
        (instance ?M ?MEAT))
    (exists (?TIME ?A)
        (and
            (instance ?A ?ANIMAL)
            (finishes ?TIME
                (WhenFn ?A))
            (holdsDuring ?TIME
                (part ?M ?A)))))		 Mid-level-ontology.kif 22595-22604 If X is the meat of Y and Z is an instance of X, then there exist W, V such that V is an instance of Y, W finishes the time of existence of V, and Z is a part of V holds during W
(=>
    (holdsDuring ?T
        (and
            (instance ?ICU IntensiveCareUnit)
            (stays ?H ?ICU)))
    (modalAttribute
        (exists (?D)
            (and
                (instance ?D Death)
                (finishes
                    (WhenFn ?D) ?T))) Possibility))		 Mid-level-ontology.kif 22810-22820 If X is an instance of ICU and Y stays at X holds during Z, then the statement there exists W such that W is an instance of death and the time of existence of W finishes Z has the modal force of possibility
(=>
    (instance ?MS MuakharSadaq)
    (exists (?H ?W ?T1 ?T2)
        (and
            (agent ?MS ?H)
            (origin ?MS ?H)
            (destination ?MS ?W)
            (holdsDuring ?T1
                (wife ?W ?H))
            (not
                (holdsDuring ?T2
                    (wife ?W ?H)))
            (finishes ?T1 ?MS)
            (before ?T1 ?T2)
            (starts ?T2 ?MS))))		 ArabicCulture.kif 285-299 If X is an instance of muakhar sadaq, then All of the following hold: (1) there exist Y, Z,, , W (2) V such that Y is an agent of X (3) X originates at Y (4) X ends up at Z (5) Z is the wife of Y holds during W (6) Z is the wife of Y doesn't hold during V (7) W finishes X (8) W happens before V (9) V starts X

Display limited to 25 items. Show next 25

Display limited to 25 items. Show next 25

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


(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