TreeView Knowledge Base Browser

appearance as argument number 1

s__documentation(s__before__m,s__ChineseLanguage,'"(before ?POINT1 ?POINT2)的意思是 ?POINT1 在通用时间轴上比 ?POINT2 先开始。"')	chinese_format.kif 2707-2708
s__documentation(s__before__m,s__EnglishLanguage,'"(before ?POINT1 ?POINT2) means that ?POINT1 precedes ?POINT2 on the universal timeline."')	Merge.kif 7850-7851
s__domain(s__before__m,n__1,s__TimePoint)	Merge.kif 7847-7847	The number 1 argument of before is an instance of time point
s__domain(s__before__m,n__2,s__TimePoint)	Merge.kif 7848-7848	The number 2 argument of before is an instance of time point
s__instance(s__IrreflexiveRelation,s__Class) s__instance(s__before__m,s__IrreflexiveRelation)	Merge.kif 7843-7843	before is an instance of irreflexive relation
s__instance(s__TemporalRelation,s__Class) s__instance(s__before__m,s__TemporalRelation)	Merge.kif 7842-7842	before is an instance of temporal relation
s__instance(s__TransitiveRelation,s__Class) s__instance(s__before__m,s__TransitiveRelation)	Merge.kif 7844-7844	before is an instance of transitive relation
s__relatedInternalConcept(s__before__m,s__earlier__m)	Merge.kif 7846-7846	before is internally related to earlier
s__subrelation(s__before__m,s__beforeOrEqual__m)	Merge.kif 7845-7845	before is a subrelation of before or equal

appearance as argument number 2

s__format(s__ChineseLanguage,s__before__m,'"%1%n在%2before发生"')	chinese_format.kif 423-423
s__format(s__EnglishLanguage,s__before__m,'"%1 %n{doesnt} happen%p{s} before %2"')	english_format.kif 432-432
s__termFormat(s__ChineseLanguage,s__before__m,'"之前"')	chinese_format.kif 424-424
s__termFormat(s__ChineseTraditionalLanguage,s__before__m,'"之前"')	domainEnglishFormat.kif 10543-10543
s__termFormat(s__EnglishLanguage,s__before__m,'"before"')	domainEnglishFormat.kif 10542-10542

antecedent

No TPTP formula. May not be expressible in strict first order.	ArabicCulture.kif 57-75	If mausaharati is an attribute of an agent and a time interval is an instance of drumming and the agent is an agent of the time interval and the time intervalAY is an instance of day and another time interval is an instance of sunrise and the other time interval takes place during the time interval and the time interval happens before the other time interval, then the time interval has the purpose there exist another entity, the other time intervalUHUR and a fourth entity such that the fourth entity is an instance of waking up and the other entity experiences the fourth entity and the other time intervalUHUR is an instance of suhur and the other entity is an agent of the other time intervalUHUR and the fourth entity happens before the other time intervalUHUR and the fourth entity takes place during the time intervalAY and the other time intervalUHUR takes place during the time intervalAY
( ! [V__S1START,V__A,V__S1,V__S2START,V__S2] : (((s__instance(V__S1START,s__TimePoint) & s__instance(V__S2START,s__TimePoint)) => (((s__instance(V__A,s__Ambulating) & s__subProcess(V__S1,V__A) & s__instance(V__S1,s__Stepping) & s__subProcess(V__S2,V__A) & s__instance(V__S2,s__Stepping) & (V__S1START = s__BeginFn(s__WhenFn(V__S1))) & (V__S2START = s__BeginFn(s__WhenFn(V__S2))) & ~((s__before(V__S1START,V__S2START) \| s__before(V__S2START,V__S1START)))) => ((V__S1 = V__S2))))) ) )	Mid-level-ontology.kif 472-485	If a process is an instance of ambulating and another process is a subprocess of the process and the other process is an instance of stepping and a third process is a subprocess of the process and the third process is an instance of stepping and the other processSTART is equal to the beginning of the time of existence of the other process and the third processSTART is equal to the beginning of the time of existence of the third process and the other processSTART happens before the third processSTART and the third processSTART happens before the other processSTART, then the other process is equal to the third process
( ! [V__CD,V__DateOfWithdrawal,V__Withdrawal,V__MaturityDate] : (((s__instance(V__DateOfWithdrawal,s__Day) & s__instance(V__MaturityDate,s__Day)) => (((s__instance(V__CD,s__CertificateOfDeposit) & s__maturityDate(V__CD,V__MaturityDate) & s__instance(V__Withdrawal,s__Withdrawal) & s__origin(V__Withdrawal,s__CurrencyFn(V__CD)) & s__date(V__Withdrawal,V__DateOfWithdrawal) & s__before(s__EndFn(V__DateOfWithdrawal) ,s__BeginFn(V__MaturityDate))) => (( ? [V__Penalty] : ((s__instance(V__Penalty,s__Penalty) & s__destination(V__Penalty,s__CurrencyFn(V__CD)) & s__causes(V__Withdrawal,V__Penalty)))))))) ) )	FinancialOntology.kif 1041-1053	If a financial account is an instance of certificate of deposit and a day is a maturity date of the financial account and a process is an instance of withdrawal and the process originates at the currency of the financial account and date of the process is another day and the end of the other day happens before the beginning of the day, then there exists another process such that the other process is an instance of penalty and the other process ends up at the currency of the financial account and the process causes the other process
No TPTP formula. May not be expressible in strict first order.	Weather.kif 1597-1607	If a process is an instance of flooding and an entity is an instance of land area and the process is located at 2 and a time point is an instance of time point and the time point happens before the time of existence of the process, then the statement the entity is an instance of submerged land area holds during the time point has the modal force of unlikely
( ! [V__AGENT,V__PROCESS,V__ACCESSING,V__TIMETOFIRST,V__PROCESS_CLASS] : (((s__instance(V__PROCESS,s__TimeInterval) & s__instance(V__PROCESS,s__Process) & s__instance(V__PROCESS_CLASS,s__Class)) => (((s__instance(V__PROCESS,V__PROCESS_CLASS) & s__subclass(V__PROCESS_CLASS,s__Process) & s__instance(V__ACCESSING,s__AccessingWebPage) & s__instance(V__AGENT,s__Agent) & s__agent(V__PROCESS,V__AGENT) & s__agent(V__ACCESSING,V__AGENT) & s__during(V__PROCESS,V__ACCESSING) & s__instance(V__TIMETOFIRST,s__TimeInterval) & ~(( ? [V__PROCESS2] : ((s__instance(V__PROCESS2,s__TimeInterval) & s__instance(V__PROCESS2,s__Process) & (s__instance(V__PROCESS2,V__PROCESS_CLASS) & s__agent(V__PROCESS2,V__AGENT) & s__during(V__PROCESS2,V__ACCESSING) & s__before(s__BeginFn(s__WhenFn(V__PROCESS2)) ,s__BeginFn(s__WhenFn(V__PROCESS)))))))) & (s__BeginFn(s__WhenFn(V__ACCESSING)) = s__BeginFn(s__WhenFn(V__TIMETOFIRST))) & (s__BeginFn(s__WhenFn(V__PROCESS)) = s__EndFn(s__WhenFn(V__TIMETOFIRST)))) => ((s__TTFxFn(V__PROCESS_CLASS,V__ACCESSING) = V__TIMETOFIRST))))) ) )	UXExperimentalTerms.kif 1703-1725	If a time interval is an instance of the time interval_CLASS and the time interval_CLASS is a subclass of process and an AccessingWebPage is an instance of AccessingWebPage and an agent is an instance of agent and the agent is an agent of the time interval and the agent is an agent of the AccessingWebPage and the time interval takes place during the AccessingWebPage and a physical is an instance of time interval and there doesn't exist the time interval2 such that the time interval2 is an instance of the time interval_CLASS and the agent is an agent of the time interval2 and the time interval2 takes place during the AccessingWebPage and the beginning of the time of existence of the time interval2 happens before the beginning of the time of existence of the time interval and the beginning of the time of existence of the AccessingWebPage is equal to the beginning of the time of existence of the physical and the beginning of the time of existence of the time interval is equal to the end of the time of existence of the physical, then the time of the AccessingWebPage in the class the time interval_CLASS is equal to the physical
No TPTP formula. May not be expressible in strict first order.	FinancialOntology.kif 2631-2647	If an agreement the attribute option and a cognitive agent holds the agreement and a currency measure is a strike price of the agreement and the agreement has expiration a time interval and a financial instrument is price the currency measure for an agent and the agent is an instance of time interval and the end of the agent happens before the beginning of the time interval and the financial instrument is an underlier of the agreement, then the cognitive agent has the right to perform the class described by a symbolic string
No TPTP formula. May not be expressible in strict first order.	FinancialOntology.kif 2585-2601	If an agreement the attribute option and a cognitive agent holds the agreement and a currency measure is a strike price of the agreement and the agreement has expiration a time interval and a financial instrument is an underlier of the agreement and the financial instrument is price the currency measure for an agent and the agent is an instance of time interval and the end of the agent happens before the beginning of the time interval, then the cognitive agent has the right to perform the class described by a symbolic string
No TPTP formula. May not be expressible in strict first order.	FinancialOntology.kif 2649-2665	If an agreement the attribute option and a cognitive agent sells the agreement and a currency measure is a strike price of the agreement and the agreement has expiration a time interval and a financial instrument is price the currency measure for an agent and the agent is an instance of time interval and the end of the agent happens before the beginning of the time interval and the financial instrument is an underlier of the agreement, then the cognitive agent is obliged to perform tasks of type the class described by a symbolic string
No TPTP formula. May not be expressible in strict first order.	FinancialOntology.kif 2603-2621	If an agreement the attribute option and a cognitive agent sells the agreement and a currency measure is a strike price of the agreement and the agreement has expiration a time interval and a financial instrument is an underlier of the agreement and the financial instrument is price the currency measure for an agent and the agent is an instance of time interval and the end of the agent happens before the beginning of the time interval, then the cognitive agent is obliged to perform tasks of type the class described by a symbolic string
( ! [V__Amount,V__Date,V__Account,V__Payment,V__DueDate] : (((s__instance(V__Amount,s__CurrencyMeasure) & s__instance(V__Date,s__Day) & s__instance(V__Payment,s__FinancialTransaction) & s__instance(V__DueDate,s__TimeInterval)) => (((s__transactionAmount(V__Payment,V__Amount) & s__date(V__Payment,V__Date) & s__instance(V__Account,s__FinancialAccount) & s__destination(V__Payment,s__CurrencyFn(V__Account)) & s__amountDue(V__Account,V__Amount,V__DueDate) & s__before(s__EndFn(V__Date) ,s__BeginFn(V__DueDate))) => (s__instance(V__Payment,s__Prepayment))))) ) )	FinancialOntology.kif 788-796	If a currency measure is a transaction amount of a financial transaction and date of the financial transaction is a day and a financial account is an instance of financial account and the financial transaction ends up at the currency of the financial account and the financial account amount due the currency measure for a time interval and the end of the day happens before the beginning of the time interval, then the financial transaction is an instance of prepayment

consequent

( ! [V__INTERVAL2,V__INTERVAL1] : (((s__instance(V__INTERVAL2,s__TimeInterval) & s__instance(V__INTERVAL1,s__TimeInterval)) => (((s__earlier(V__INTERVAL1,V__INTERVAL2) => s__before(s__EndFn(V__INTERVAL1) ,s__BeginFn(V__INTERVAL2))) & (s__before(s__EndFn(V__INTERVAL1) ,s__BeginFn(V__INTERVAL2)) => s__earlier(V__INTERVAL1,V__INTERVAL2))))) ) )	Merge.kif 8028-8030	A time interval happens earlier than another time interval if and only if the end of the time interval happens before the beginning of the other time interval
( ! [V__INTERVAL2,V__INTERVAL1] : (((s__instance(V__INTERVAL2,s__TimeInterval) & s__instance(V__INTERVAL1,s__TimeInterval)) => (((s__finishes(V__INTERVAL1,V__INTERVAL2) => (s__before(s__BeginFn(V__INTERVAL2) ,s__BeginFn(V__INTERVAL1)) & (s__EndFn(V__INTERVAL2) = s__EndFn(V__INTERVAL1)))) & ((s__before(s__BeginFn(V__INTERVAL2) ,s__BeginFn(V__INTERVAL1)) & (s__EndFn(V__INTERVAL2) = s__EndFn(V__INTERVAL1))) => s__finishes(V__INTERVAL1,V__INTERVAL2))))) ) )	Merge.kif 7832-7840	A time interval finishes another time interval if and only if the beginning of the other time interval happens before the beginning of the time interval and the end of the other time interval is equal to the end of the time interval
( ! [V__INTERVAL2,V__INTERVAL1] : (((s__instance(V__INTERVAL2,s__TimeInterval) & s__instance(V__INTERVAL1,s__TimeInterval)) => (((s__starts(V__INTERVAL1,V__INTERVAL2) => ((s__BeginFn(V__INTERVAL1) = s__BeginFn(V__INTERVAL2)) & s__before(s__EndFn(V__INTERVAL1) ,s__EndFn(V__INTERVAL2)))) & (((s__BeginFn(V__INTERVAL1) = s__BeginFn(V__INTERVAL2)) & s__before(s__EndFn(V__INTERVAL1) ,s__EndFn(V__INTERVAL2))) => s__starts(V__INTERVAL1,V__INTERVAL2))))) ) )	Merge.kif 7810-7818	A time interval starts another time interval if and only if the beginning of the time interval is equal to the beginning of the other time interval and the end of the time interval happens before the end of the other time interval
( ! [V__POINT3,V__POINT2,V__POINT1] : (((s__instance(V__POINT3,s__TimePoint) & s__instance(V__POINT2,s__TimePoint) & s__instance(V__POINT1,s__TimePoint)) => (((s__temporallyBetween(V__POINT1,V__POINT2,V__POINT3) => (s__before(V__POINT1,V__POINT2) & s__before(V__POINT2,V__POINT3))) & ((s__before(V__POINT1,V__POINT2) & s__before(V__POINT2,V__POINT3)) => s__temporallyBetween(V__POINT1,V__POINT2,V__POINT3))))) ) )	Merge.kif 7910-7914	A time point is between another time point and a third time point if and only if the other time point happens before the time point and the time point happens before the third time point
( ! [V__A,V__T] : (((s__instance(V__A,s__Album) & s__instance(V__T,s__TimePoint)) => ((s__albumRelease(V__A,V__T) => ((( ? [V__R1, V__DS1] : ((s__instance(V__R1,s__GeographicArea) & s__subclass(V__DS1,s__DataStorageDevice) & s__releaseForSale(s__AlbumCopiesFn(V__A,V__DS1) ,V__R1,V__T)))) & ~(( ? [V__B, V__R2, V__DS2] : ((s__instance(V__B,s__TimePoint) & s__instance(V__R2,s__GeographicArea) & s__subclass(V__DS2,s__DataStorageDevice) & (s__before(V__B,V__T) & s__releaseForSale(s__AlbumCopiesFn(V__A,V__DS2) ,V__R2,V__B))))))))))) ) )	Music.kif 258-267	If an album was released on a time point, then there exist a geographic area and a kind of DataStorageDevice such that the set of copies on a kind of DataStorageDevice of the album was released for sale in the geographic area at the time point and there don't exist another time point, another geographic area and another kind of DataStorageDevice such that the other time point happens before the time point and the set of copies on another kind of DataStorageDevice of the album was released for sale in the other geographic area at the other time point
No TPTP formula. May not be expressible in strict first order.	Mid-level-ontology.kif 5884-5897	If allergic a human and a kind of substance and a kind of substanceUB is an instance of the kind of substance and the kind of substance meets the human holds during a time position, then the statement there exists another entity such that the other entity is an instance of AllergicReaction and the human experiences the other entity and the time of existence of the other entity overlaps the time position and the beginning of the time position happens before the beginning of the time of existence of the other entity has the modal force of likely
No TPTP formula. May not be expressible in strict first order.	ArabicCulture.kif 57-75	If mausaharati is an attribute of an agent and a time interval is an instance of drumming and the agent is an agent of the time interval and the time intervalAY is an instance of day and another time interval is an instance of sunrise and the other time interval takes place during the time interval and the time interval happens before the other time interval, then the time interval has the purpose there exist another entity, the other time intervalUHUR and a fourth entity such that the fourth entity is an instance of waking up and the other entity experiences the fourth entity and the other time intervalUHUR is an instance of suhur and the other entity is an agent of the other time intervalUHUR and the fourth entity happens before the other time intervalUHUR and the fourth entity takes place during the time intervalAY and the other time intervalUHUR takes place during the time intervalAY
( ! [V__A,V__MR,V__M,V__MM] : (((s__instance(V__A,s__CognitiveAgent) & s__instance(V__M,s__Music) & s__instance(V__MM,s__Physical)) => (((s__attribute(V__MR,s__CoverRecording) & s__instance(V__MR,s__MusicRecording) & s__songArtist(V__MR,V__A) & s__musicInterpretation(V__MR,V__M) & s__record(V__MR,V__MM)) => (( ? [V__ORIG, V__ARTIST, V__MUSIC] : ((s__instance(V__ORIG,s__MusicRecording) & s__instance(V__ARTIST,s__CognitiveAgent) & s__instance(V__MUSIC,s__Physical) & (s__musicInterpretation(V__ORIG,V__M) & s__songArtist(V__ORIG,V__ARTIST) & ~((V__A = V__ARTIST)) & s__record(V__ORIG,V__MUSIC) & s__before(s__WhenFn(V__MUSIC) ,s__WhenFn(V__MM)))))))))) ) )	Music.kif 454-467	If cover recording is an attribute of a music recording and the music recording is an instance of music recording and a cognitive agent is the performer in the music recording and the music recording is a recording of a music and the music recording is a record of the musicM, then there exist another music recording, the cognitive agentRTIST and the musicUSIC such that the other music recording is a recording of the music and the cognitive agentRTIST is the performer in the other music recording and the cognitive agent is not equal to the cognitive agentRTIST and the other music recording is a record of the musicUSIC and the time of existence of the musicUSIC happens before the time of existence of the musicM
No TPTP formula. May not be expressible in strict first order.	Hotel.kif 663-674	If one must check out before a time point at a cognitive agent and another cognitive agent is a guest at the cognitive agent, then the cognitive agent expects there exist an entity and another entity such that the entity is an instance of the time point and the other cognitive agent is a patient of the other entity and the other entity is an instance of check-out service and the cognitive agent is an agent of the other entity and the beginning of the time of existence of the other entity happens before the entity will be true
( ! [V__TELEX,V__M,V__MSG] : (((s__destination(V__MSG,V__TELEX) & s__instance(V__MSG,s__Messaging) & s__patient(V__MSG,V__M) & s__instance(V__TELEX,s__Telex)) => (( ? [V__PROC, V__TEXT] : ((s__instance(V__PROC,s__Process) & (s__instrument(V__PROC,V__TELEX) & s__result(V__PROC,V__TEXT) & s__represents(V__TEXT,V__M) & s__instance(V__TEXT,s__Text) & s__before(s__BeginFn(s__WhenFn(V__MSG)) ,s__BeginFn(s__WhenFn(V__PROC))))))))) ) )	Communications.kif 202-214	If a process ends up at an object and the process is an instance of messaging and an entity is a patient of the process and the object is an instance of telex, then there exist another process and another entity such that the object is an instrument for the other process and the other entity is a result of the other process and the other entity expresses the entity and the other entity is an instance of text and the beginning of the time of existence of the process happens before the beginning of the time of existence of the other process
( ! [V__TEXT,V__EDITION1,V__CBO2,V__EDITION2,V__CBO1,V__INT2,V__PUB2,V__DATE1,V__INT1,V__DATE2,V__PUB1] : (((s__subclass(V__TEXT,s__ContentBearingObject) & s__subclass(V__EDITION1,s__ContentBearingObject) & s__instance(V__EDITION1,s__Class) & s__subclass(V__EDITION2,s__ContentBearingObject) & s__instance(V__EDITION2,s__Class) & s__instance(V__INT2,s__PositiveInteger) & s__instance(V__DATE1,s__Day) & s__instance(V__INT1,s__PositiveInteger) & s__instance(V__DATE2,s__Day)) => ((((s__EditionFn(V__TEXT,V__INT1) = V__EDITION1) & (s__EditionFn(V__TEXT,V__INT2) = V__EDITION2) & s__greaterThan(V__INT2,V__INT1) & s__instance(V__PUB1,s__Publication) & s__instance(V__PUB2,s__Publication) & s__instance(V__CBO1,V__EDITION1) & s__instance(V__CBO2,V__EDITION2) & s__patient(V__PUB1,V__CBO1) & s__patient(V__PUB2,V__CBO2) & s__date(V__PUB1,V__DATE1) & s__date(V__PUB2,V__DATE2)) => (s__before(s__EndFn(V__DATE1) ,s__EndFn(V__DATE2)))))) ) )	Merge.kif 14846-14863	If edition a positive integer of a kind of content bearing object is equal to another kind of content bearing object and edition another positive integer of a kind of content bearing object is equal to a third kind of content bearing object and the other positive integer is greater than the positive integer and a process is an instance of publication and another process is an instance of publication and an entity is an instance of another kind of content bearing object and another entity is an instance of a third kind of content bearing object and the entity is a patient of the process and the other entity is a patient of the other process and date of the process is a day and date of the other process is another day, then the end of the day happens before the end of the other day
( ! [V__AGENT,V__PROCESS,V__PROCESSSTART,V__AGENTEND] : (((s__instance(V__AGENT,s__Agent) & s__instance(V__PROCESS,s__Process) & s__instance(V__PROCESSSTART,s__TimePoint) & s__instance(V__AGENTEND,s__TimePoint)) => ((((V__PROCESSSTART = s__BeginFn(s__WhenFn(V__PROCESS))) & (V__AGENTEND = s__EndFn(s__WhenFn(V__AGENT))) & s__benefits(V__PROCESS,V__AGENT)) => (s__before(V__PROCESSSTART,V__AGENTEND))))) ) )	Mid-level-ontology.kif 22011-22016	If a time point is equal to the beginning of the time of existence of a process and another time point is equal to the end of the time of existence of an agent and the agent is a beneficiary of the process, then the time point happens before the other time point
( ! [V__AGENT,V__PROCESS,V__PROCESSSTART,V__AGENTEND] : (((s__instance(V__AGENT,s__Agent) & s__instance(V__PROCESS,s__Process) & s__instance(V__PROCESSSTART,s__TimePoint) & s__instance(V__AGENTEND,s__TimePoint)) => ((((V__PROCESSSTART = s__BeginFn(s__WhenFn(V__PROCESS))) & (V__AGENTEND = s__EndFn(s__WhenFn(V__AGENT))) & s__suffers(V__PROCESS,V__AGENT)) => (s__before(V__PROCESSSTART,V__AGENTEND))))) ) )	Mid-level-ontology.kif 28654-28663	If a time point is equal to the beginning of the time of existence of a process and another time point is equal to the end of the time of existence of an agent and the agent suffers from the process, then the time point happens before the other time point
( ! [V__N1,V__N2,V__Y,V__D1,V__T1,V__D2,V__T2,V__M] : (((s__instance(V__N1,s__PositiveInteger) & s__instance(V__N2,s__PositiveInteger) & s__instance(V__Y,s__Integer) & s__instance(V__D1,s__TimeInterval) & s__instance(V__T1,s__TimePoint) & s__instance(V__D2,s__TimeInterval) & s__instance(V__T2,s__TimePoint) & s__subclass(V__M,s__Month)) => (((s__instance(V__D1,s__DayFn(V__N1,s__MonthFn(V__M,s__YearFn(V__Y)))) & s__instance(V__D2,s__DayFn(V__N2,s__MonthFn(V__M,s__YearFn(V__Y)))) & (V__T1 = s__BeginFn(V__D1)) & (V__T2 = s__BeginFn(V__D2)) & s__greaterThan(V__N2,V__N1)) => (s__before(V__T1,V__T2))))) ) )	Merge.kif 8365-8372	If a time interval is an instance of the day a positive integer and another time interval is an instance of the day another positive integer and a time point is equal to the beginning of the time interval and another time point is equal to the beginning of the other time interval and the other positive integer is greater than the positive integer, then the time point happens before the other time point
( ! [V__Period,V__Loan,V__Date,V__Interest,V__Principal] : (((s__instance(V__Period,s__TimeInterval) & s__instance(V__Date,s__TimeInterval) & s__instance(V__Interest,s__Interest) & s__instance(V__Principal,s__CurrencyMeasure)) => (((s__instance(V__Loan,s__InterestOnlyLoan) & s__agreementPeriod(V__Loan,V__Period) & s__principalAmount(V__Loan,V__Principal) & s__interestEarned(V__Loan,V__Interest,V__Period)) => ((s__amountDue(V__Loan,V__Principal,s__EndFn(V__Period)) & s__amountDue(V__Loan,V__Interest,V__Date) & s__before(s__EndFn(V__Date) ,s__EndFn(V__Period))))))) ) )	FinancialOntology.kif 1570-1579	If a financial account is an instance of interest only loan and a time interval is an agreement period of the financial account and a currency measure is a principal amount of the financial account and the financial account is interest earned an interest for the time interval, then the financial account amount due the currency measure for the end of the time interval and the financial account amount due the interest for another time interval and the end of the other time interval happens before the end of the time interval
( ! [V__N1,V__M1,V__N2,V__M2,V__Y,V__T1,V__T2] : (((s__instance(V__N1,s__Class) & s__subclass(V__N1,s__Month) & s__instance(V__M1,s__TimeInterval) & s__instance(V__N2,s__Class) & s__subclass(V__N2,s__Month) & s__instance(V__M2,s__TimeInterval) & s__instance(V__Y,s__Integer) & s__instance(V__T1,s__TimePoint) & s__instance(V__T2,s__TimePoint)) => (((s__instance(V__M1,s__MonthFn(V__N1,s__YearFn(V__Y))) & s__instance(V__M2,s__MonthFn(V__N2,s__YearFn(V__Y))) & (V__T1 = s__BeginFn(V__M1)) & (V__T2 = s__BeginFn(V__M2)) & s__successorClass(V__N1,V__N2)) => (s__before(V__T1,V__T2))))) ) )	Merge.kif 8349-8356	If a time interval is an instance of the month a kind of month and another time interval is an instance of the month another kind of month and a time point is equal to the beginning of the time interval and another time point is equal to the beginning of the other time interval and %2 is the successorClass of %2., then the time point happens before the other time point
( ! [V__POINT] : (((s__instance(V__POINT,s__TimePoint) & ~((V__POINT = s__NegativeInfinity))) => (s__before(s__NegativeInfinity,V__POINT))) ) )	Merge.kif 7657-7661	If a time point is an instance of time point and the time point is not equal to negative infinity, then negative infinity happens before the time point
( ! [V__POINT] : (((s__instance(V__POINT,s__TimePoint) & ~((V__POINT = s__PositiveInfinity))) => (s__before(V__POINT,s__PositiveInfinity))) ) )	Merge.kif 7639-7643	If a time point is an instance of time point and the time point is not equal to positive infinity, then the time point happens before positive infinity
No TPTP formula. May not be expressible in strict first order.	Merge.kif 11582-11591	If a process is an instance of remembering and a formula is a patient of the process, then there exists a time interval such that the formula holds during the time interval and the time interval happens before the time of existence of the process or the time interval happens earlier than the time of existence of the process
( ! [V__PLACE,V__SHOCK] : (((s__instance(V__SHOCK,s__Aftershock) & s__eventLocated(V__SHOCK,V__PLACE)) => (( ? [V__TREMOR] : ((s__instance(V__TREMOR,s__EarthTremor) & s__eventLocated(V__TREMOR,V__PLACE) & s__before(s__WhenFn(V__TREMOR) ,s__WhenFn(V__SHOCK))))))) ) )	Geography.kif 2294-2302	If a process is an instance of aftershock and the process is located at 2, then there exists another process such that the other process is an instance of earth tremor and the other process is located at 2 and the time of existence of the other process happens before the time of existence of the process
( ! [V__AGENT,V__E,V__ITEM,V__X,V__LOC2,V__LOC1] : (((s__instance(V__AGENT,s__Agent) & s__instance(V__ITEM,s__Physical) & s__instance(V__LOC1,s__Object)) => (((s__instance(V__X,s__Buffet) & s__member(V__ITEM,V__X) & s__located(V__X,V__LOC1) & s__instance(V__E,s__Eating) & s__agent(V__E,V__AGENT) & s__eventLocated(V__E,V__LOC2) & s__patient(V__E,V__ITEM)) => ((~((V__LOC1 = V__LOC2)) & ( ? [V__G] : ((s__instance(V__G,s__Getting) & s__patient(V__G,V__ITEM) & s__origin(V__G,V__LOC1) & s__agent(V__G,V__AGENT) & s__before(s__WhenFn(V__G) ,s__WhenFn(V__E)))))))))) ) )	Dining.kif 270-287	If a collection is an instance of buffet and a physical is a member of the collection and the collection is located at an object and a process is an instance of eating and an agent is an agent of the process and the process is located at 2 and the physical is a patient of the process, then the object is not equal to an entity and there exists another process such that the other process is an instance of getting and the physical is a patient of the other process and the other process originates at the object and the agent is an agent of the other process and the time of existence of the other process happens before the time of existence of the process
No TPTP formula. May not be expressible in strict first order.	Mid-level-ontology.kif 26014-26040	If a physical is an instance of surveillance system and the physical is a member of a collection and the physical is a member of another collection and the collection is located at an object and the collection is an instance of camera and the other collection is located at another object and the object is not equal to the other object and the other collection is an instance of video display, then the physical has the purpose there exist an entity, another entity,, , a third entity and a fourth entity such that the entity is an instance of process and the entity is located at 2 and the other entity expresses the entity and camera is an instrument for the fourth entity and the other entity is a result of the fourth entity and the third entity is an instance of radiating light and the other collection is an instrument for the third entity and the other entity is a patient of the third entity and the beginning of the entity happens before the beginning of the fourth entity and the beginning of the fourth entity happens before the beginning of the third entity
( ! [V__N1,V__N2,V__Y1,V__Y2,V__T1,V__T2] : (((s__instance(V__N1,s__Integer) & s__instance(V__N2,s__Integer) & s__instance(V__Y1,s__TimeInterval) & s__instance(V__Y2,s__TimeInterval) & s__instance(V__T1,s__TimePoint) & s__instance(V__T2,s__TimePoint)) => (((s__instance(V__Y1,s__YearFn(V__N1)) & s__instance(V__Y2,s__YearFn(V__N2)) & (V__T1 = s__BeginFn(V__Y1)) & (V__T2 = s__BeginFn(V__Y2)) & s__greaterThan(V__N2,V__N1)) => (s__before(V__T1,V__T2))))) ) )	Merge.kif 8333-8340	If a time interval is an instance of the year an integer and another time interval is an instance of the year another integer and a time point is equal to the beginning of the time interval and another time point is equal to the beginning of the other time interval and the other integer is greater than the integer, then the time point happens before the other time point
No TPTP formula. May not be expressible in strict first order.	FinancialOntology.kif 2749-2761	If an agreement the attribute american style option and a cognitive agent holds the agreement and the agreement has expiration a time point, then the cognitive agent has the right to perform there exists an entity such that the entity is an instance of exercise an option and the agreement is a patient of the entity and the end of the time of existence of the entity happens before the end of the time point
( ! [V__TEXT,V__CBO2,V__CBO1,V__INT2,V__PUB2,V__DATE1,V__INT1,V__DATE2,V__VOLUME2,V__PUB1,V__VOLUME1] : (((s__subclass(V__TEXT,s__Series) & s__instance(V__TEXT,s__Class) & s__instance(V__INT2,s__PositiveInteger) & s__instance(V__DATE1,s__Day) & s__instance(V__INT1,s__PositiveInteger) & s__instance(V__DATE2,s__Day) & s__subclass(V__VOLUME2,s__Text) & s__instance(V__VOLUME2,s__Class) & s__subclass(V__VOLUME1,s__Text) & s__instance(V__VOLUME1,s__Class)) => (((s__subclass(V__TEXT,s__Periodical) & (s__SeriesVolumeFn(V__TEXT,V__INT1) = V__VOLUME1) & (s__SeriesVolumeFn(V__TEXT,V__INT2) = V__VOLUME2) & s__greaterThan(V__INT2,V__INT1) & s__instance(V__PUB1,s__Publication) & s__instance(V__PUB2,s__Publication) & s__instance(V__CBO1,V__VOLUME1) & s__instance(V__CBO2,V__VOLUME2) & s__patient(V__PUB1,V__CBO1) & s__patient(V__PUB2,V__CBO2) & s__date(V__PUB1,V__DATE1) & s__date(V__PUB2,V__DATE2)) => (s__before(s__EndFn(V__DATE1) ,s__EndFn(V__DATE2)))))) ) )	Mid-level-ontology.kif 13814-13828	If a kind of series is a subclass of periodical and volume a positive integer in the series a kind of series is equal to a kind of text and volume another positive integer in the series the kind of series is equal to another kind of text and the other positive integer is greater than the positive integer and a process is an instance of publication and another process is an instance of publication and an entity is an instance of a kind of text and another entity is an instance of another kind of text and the entity is a patient of the process and the other entity is a patient of the other process and date of the process is a day and date of the other process is another day, then the end of the day happens before the end of the other day

Display limited to 25 items. Show next 25

Display limited to 25 items. Show next 25

Show simplified definition (without tree view)
Show simplified definition (with tree view)

KB Term:			Term intersection

English Word: