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

Formal Language: 



KB Term:  Term intersection
English Word: 

  Cerium

Sigma KEE - before
before

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


s__documentation(s__before__m,s__ChineseLanguage,'(before ?POINT1 ?POINT2)的意思是 ?POINT1 在通用时 间轴上比 ?POINT2 先开始。')

Merge.kif 8280-8281
s__documentation(s__before__m,s__EnglishLanguage,'(before ?POINT1 ?POINT2) means that ?POINT1 precedes ?POINT2 on the universal timeline.')

Merge.kif 8278-8279
s__domain(s__before__m,1,s__TimePoint)

Merge.kif 8276-8276
s__domain(s__before__m,2,s__TimePoint)

Merge.kif 8277-8277
s__instance(s__IrreflexiveRelation,s__SetOrClass)

Merge.kif 8272-8272
s__instance(s__TemporalRelation,s__SetOrClass)

Merge.kif 8271-8271
s__instance(s__TransitiveRelation,s__SetOrClass)

Merge.kif 8273-8273
s__relatedInternalConcept(s__before__m,s__earlier__m)

Merge.kif 8275-8275
s__subrelation(s__before__m,s__beforeOrEqual__m)

Merge.kif 8274-8274

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 256-256
s__format(s__FrenchLanguage,s__before__m,'%1 %n{ne} se produit %n{pas} avant %2')

french_format.kif 246-246
s__format(s__ItalianLanguage,s__before__m,'%1 %n{non} succede%{s} prima di %2')

relations-it.txt 32-32
s__format(s__PortugueseLanguage,s__before__m,'%1 %n{nao} comeca %n antes de %2')

portuguese_format.kif 198-198
s__format(s__ar__m,s__before__m,'%1 %n{لا} يَحْدُث قَبْلَ %2')

arabic_format.kif 180-180
s__format(s__cb__m,s__before__m,'%1 %n{dili} nahimo una sa %2')

relations-cb.txt 66-66
s__format(s__cz__m,s__before__m,'%1 %n{doesnt} happen%p{s} before %2')

relations-cz.txt 251-251
s__format(s__de__m,s__before__m,'%1 geschieht vor %2 %n{nicht}')

relations-de.txt 550-550
s__format(s__hi__m,s__before__m,'%1 %2 ke pahale %n{nahiin} ghaTita hotaa hai')

relations-hindi.txt 76-76
s__format(s__tg__m,s__before__m,'%1 %n{hindi} nagaanap bago sa %2')

relations-tg.txt 80-80
s__termFormat(s__ChineseLanguage,s__before__m,'之前')

chinese_format.kif 424-424
s__termFormat(s__EnglishLanguage,s__before__m,'before')

domainEnglishFormat.kif 2180-2180
s__termFormat(s__ar__m,s__before__m,'«يَحْدُث قَبْلَ»')

arabic_format.kif 630-630
s__termFormat(s__tg__m,s__before__m,'nagaanap bago')

relations-tg.txt 81-81

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


No TPTP formula. May not be expressible in strict first order. ArabicCulture.kif 57-75
( ∀ [V__A,V__S1,V__S2,V__S1_START,V__S2_START]
   ((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__S1_START = s__BeginFn(s__WhenFn(V__S1)))

(V__S2_START = s__BeginFn(s__WhenFn(V__S2)))

(¬ (s__before(V__S1_START,V__S2_START)

s__before(V__S2_START,V__S1_START))))

(V__S1 = V__S2))
)

Mid-level-ontology.kif 676-689
( ∀ [V__CD,V__MaturityDate,V__Withdrawal,V__DateOfWithdrawal]
   ((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 1032-1044
( ∀ [V__PROCESS,V__PROCESS_CLASS,V__ACCESSING,V__AGENT,V__TIMETOFIRST]
   ((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,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
No TPTP formula. May not be expressible in strict first order. FinancialOntology.kif 2590-2606
No TPTP formula. May not be expressible in strict first order. FinancialOntology.kif 2546-2562
No TPTP formula. May not be expressible in strict first order. FinancialOntology.kif 2608-2624
No TPTP formula. May not be expressible in strict first order. FinancialOntology.kif 2564-2580
( ∀ [V__Payment,V__Amount,V__Date,V__Account,V__AmountDue,V__DueDate]
   ((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__AmountDue,V__DueDate)

s__before(s__EndFn(V__Date)
,s__BeginFn(V__DueDate)))

s__instance(V__Payment,s__Prepayment))
)

FinancialOntology.kif 779-787

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


( ∀ [V__INTERVAL1,V__INTERVAL2]
   (s__earlier(V__INTERVAL1,V__INTERVAL2)
   <⇒
   s__before(s__EndFn(V__INTERVAL1)
,s__BeginFn(V__INTERVAL2)))
)

Merge.kif 8465-8467
( ∀ [V__INTERVAL1,V__INTERVAL2]
   (s__finishes(V__INTERVAL1,V__INTERVAL2)
   <⇒
   (s__before(s__BeginFn(V__INTERVAL2)
  ,s__BeginFn(V__INTERVAL1))

(s__EndFn(V__INTERVAL2)
= s__EndFn(V__INTERVAL1))))
)

Merge.kif 8261-8269
( ∀ [V__INTERVAL1,V__INTERVAL2]
   (s__starts(V__INTERVAL1,V__INTERVAL2)
   <⇒
   ((s__BeginFn(V__INTERVAL1)
     = s__BeginFn(V__INTERVAL2))

s__before(s__EndFn(V__INTERVAL1)
,s__EndFn(V__INTERVAL2))))
)

Merge.kif 8237-8245
( ∀ [V__POINT1,V__POINT2,V__POINT3]
   (s__temporallyBetween(V__POINT1,V__POINT2,V__POINT3)
   <⇒
   (s__before(V__POINT1,V__POINT2)
   ∧
   s__before(V__POINT2,V__POINT3)))
)

Merge.kif 8343-8347
( ∀ [V__A,V__T]
   (s__albumRelease(V__A,V__T)
   ⇒
   ((∃ [V__R1,V__DS1]
       s__releaseForSale(s__AlbumCopiesFn(V__A,V__DS1)
    ,V__R1,V__T))

(¬ (∃ [V__B,V__R2,V__DS2]
     (s__before(V__B,V__T)
     ∧
     s__releaseForSale(s__AlbumCopiesFn(V__A,V__DS2)
  ,V__R2,V__B))))))
)

Music.kif 255-264
No TPTP formula. May not be expressible in strict first order. ArabicCulture.kif 57-75
( ∀ [V__MR,V__A,V__M,V__MM]
   ((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__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 460-473
No TPTP formula. May not be expressible in strict first order. Hotel.kif 653-664
( ∀ [V__MSG,V__TELEX,V__M]
   ((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__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
( ∀ [V__TEXT,V__INT1,V__EDITION1,V__INT2,V__EDITION2,V__PUB1,V__PUB2,V__CBO1,V__CBO2,V__DATE1,V__DATE2]
   (((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 15574-15591
( ∀ [V__PROCESS_START,V__PROCESS,V__AGENT_END,V__AGENT]
   (((V__PROCESS_START = s__BeginFn(s__WhenFn(V__PROCESS)))
   ∧
   (V__AGENT_END = s__EndFn(s__WhenFn(V__AGENT)))

s__benefits(V__PROCESS,V__AGENT))

s__before(V__PROCESS_START,V__AGENT_END))
)

Mid-level-ontology.kif 20772-20777
( ∀ [V__PROCESS_START,V__PROCESS,V__AGENT_END,V__AGENT]
   (((V__PROCESS_START = s__BeginFn(s__WhenFn(V__PROCESS)))
   ∧
   (V__AGENT_END = s__EndFn(s__WhenFn(V__AGENT)))

s__suffers(V__PROCESS,V__AGENT))

s__before(V__PROCESS_START,V__AGENT_END))
)

Mid-level-ontology.kif 27684-27693
( ∀ [V__T1,V__N1,V__M,V__Y,V__T2,V__N2]
   (((V__T1 = s__BeginFn(s__DayFn(V__N1,s__MonthFn(V__M,s__YearFn(V__Y)))))

(V__T2 = s__BeginFn(s__DayFn(V__N2,s__MonthFn(V__M,s__YearFn(V__Y)))))

s__greaterThan(V__N2,V__N1))

s__before(V__T1,V__T2))
)

Merge.kif 8838-8843
( ∀ [V__T1,V__N1,V__Y,V__T2,V__N2]
   (((V__T1 = s__BeginFn(s__MonthFn(V__N1,s__YearFn(V__Y))))

(V__T2 = s__BeginFn(s__MonthFn(V__N2,s__YearFn(V__Y))))

s__greaterThan(V__N2,V__N1))

s__before(V__T1,V__T2))
)

Merge.kif 8824-8829
( ∀ [V__T1,V__N1,V__T2,V__N2]
   (((V__T1 = s__BeginFn(s__YearFn(V__N1)))
   ∧
   (V__T2 = s__BeginFn(s__YearFn(V__N2)))

s__greaterThan(V__N2,V__N1))

s__before(V__T1,V__T2))
)

Merge.kif 8810-8815
( ∀ [V__Loan,V__Period,V__Principal,V__Interest,V__Date]
   ((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 1559-1568
( ∀ [V__POINT]
   ((s__instance(V__POINT,s__TimePoint) ∧
       (¬ (V__POINT = s__NegativeInfinity)))
       ⇒
       s__before(s__NegativeInfinity,V__POINT))
   )

Merge.kif 8080-8084
( ∀ [V__POINT]
   ((s__instance(V__POINT,s__TimePoint) ∧
       (¬ (V__POINT = s__PositiveInfinity)))
       ⇒
       s__before(V__POINT,s__PositiveInfinity))
     )

Merge.kif 8061-8065
No TPTP formula. May not be expressible in strict first order. Merge.kif 12027-12036
( ∀ [V__SHOCK,V__PLACE]
   ((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 2261-2269
( ∀ [V__X,V__ITEM,V__LOC1,V__E,V__AGENT,V__LOC2]
   ((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 277-294
No TPTP formula. May not be expressible in strict first order. Mid-level-ontology.kif 25089-25115
No TPTP formula. May not be expressible in strict first order. FinancialOntology.kif 2708-2720
( ∀ [V__TEXT,V__INT1,V__VOLUME1,V__INT2,V__VOLUME2,V__PUB1,V__PUB2,V__CBO1,V__CBO2,V__DATE1,V__DATE2]
   ((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 12368-12382
( ∀ [V__POINT1,V__POINT2]
   (s__beforeOrEqual(V__POINT1,V__POINT2)
   ⇒
   (s__before(V__POINT1,V__POINT2)
   ∨
   (V__POINT1 = V__POINT2)))
)

Merge.kif 8322-8326

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)

Show without tree


Sigma web home      Suggested Upper Merged Ontology (SUMO) web home
Sigma version 2.99c (>= 2017/11/20) is open source software produced by Articulate Software and its partners