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

Formal Language: 



KB Term:  Term intersection
English Word: 

  equal

Sigma KEE - equal
equal

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


No TPTP formula. May not be expressible in strict first order. Merge.kif 290-291
No TPTP formula. May not be expressible in strict first order. Merge.kif 288-289
No TPTP formula. May not be expressible in strict first order. Merge.kif 286-286
No TPTP formula. May not be expressible in strict first order. Merge.kif 287-287
No TPTP formula. May not be expressible in strict first order. Merge.kif 283-283
No TPTP formula. May not be expressible in strict first order. Merge.kif 284-284
s__instance(s__RelationExtendedToQuantities,s__SetOrClass)

Merge.kif 285-285

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


No TPTP formula. May not be expressible in strict first order. chinese_format.kif 297-297
No TPTP formula. May not be expressible in strict first order. english_format.kif 181-181
No TPTP formula. May not be expressible in strict first order. french_format.kif 171-171
No TPTP formula. May not be expressible in strict first order. relations-it.txt 96-96
No TPTP formula. May not be expressible in strict first order. portuguese_format.kif 123-123
No TPTP formula. May not be expressible in strict first order. arabic_format.kif 116-116
No TPTP formula. May not be expressible in strict first order. relations-cz.txt 179-179
No TPTP formula. May not be expressible in strict first order. relations-de.txt 387-387
No TPTP formula. May not be expressible in strict first order. relations-hindi.txt 136-136
No TPTP formula. May not be expressible in strict first order. relations-tg.txt 205-205
No TPTP formula. May not be expressible in strict first order. chinese_format.kif 298-298
No TPTP formula. May not be expressible in strict first order. domainEnglishFormat.kif 4141-4141
No TPTP formula. May not be expressible in strict first order. arabic_format.kif 566-566
No TPTP formula. May not be expressible in strict first order. relations-tg.txt 206-206

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


( ∀ [V__NUMBER1,V__NUMBER2]
   (((s__AbsoluteValueFn(V__NUMBER1)
       = V__NUMBER2)
     ∧
     s__instance(V__NUMBER1,s__RealNumber) ∧
     s__instance(V__NUMBER2,s__RealNumber))
   <⇒
   ((s__instance(V__NUMBER1,s__NonnegativeRealNumber) ∧
       (V__NUMBER1 = V__NUMBER2))
     ∨
     (s__instance(V__NUMBER1,s__NegativeRealNumber) ∧
       (V__NUMBER2 = s__SubtractionFn(0,V__NUMBER1)))))
)

Merge.kif 4911-4922
( ∀ [V__Account,V__Agent,V__Asset]
   ((s__instance(V__Account,s__FinancialAccount) ∧
       s__possesses(V__Agent,V__Asset)
     ∧
     (V__Account = s__AccountFn(V__Asset)))
<⇒
s__accountHolder(V__Account,V__Agent))
)

FinancialOntology.kif 2252-2257
( ∀ [V__UNIT,V__AMOUNT]
   ((s__instance(V__UNIT,s__UnitOfMeasure) ∧
       (V__AMOUNT = s__MeasureFn(1,s__SquareUnitFn(V__UNIT))))
<⇒
(V__AMOUNT = s__MultiplicationFn(s__MeasureFn(1,V__UNIT)
,s__MeasureFn(1,V__UNIT))))
)

Geography.kif 3748-3752
No TPTP formula. May not be expressible in strict first order. People.kif 104-117
No TPTP formula. May not be expressible in strict first order. People.kif 138-151
No TPTP formula. May not be expressible in strict first order. People.kif 253-277
No TPTP formula. May not be expressible in strict first order. People.kif 411-442
( ∀ [V__LIST,V__ITEM]
   ((s__LastFn(V__LIST)
     = V__ITEM)
   <⇒
   (∃ [V__NUMBER]
     ((s__ListLengthFn(V__LIST)
       = V__NUMBER)
     ∧
     (s__ListOrderFn(V__LIST,V__NUMBER)
     = V__ITEM))))
)

Mid-level-ontology.kif 6346-6351
No TPTP formula. May not be expressible in strict first order. People.kif 323-353
No TPTP formula. May not be expressible in strict first order. People.kif 367-398
No TPTP formula. May not be expressible in strict first order. People.kif 221-238
No TPTP formula. May not be expressible in strict first order. People.kif 174-202
No TPTP formula. May not be expressible in strict first order. People.kif 77-86
( ∀ [V__NUMBER1,V__NUMBER2,V__NUMBER]
   ((s__RemainderFn(V__NUMBER1,V__NUMBER2)
     = V__NUMBER)
   <⇒
   (s__AdditionFn(s__MultiplicationFn(s__FloorFn(s__DivisionFn(V__NUMBER1,V__NUMBER2))
,V__NUMBER2)
,V__NUMBER)
= V__NUMBER1))
)

Merge.kif 5248-5250
( ∀ [V__PERSON,V__AMOUNT]
   ((s__WealthFn(V__PERSON)
     = V__AMOUNT)
   <⇒
   s__monetaryValue(s__PropertyFn(V__PERSON)
,V__AMOUNT))
)

Merge.kif 7994-7996
No TPTP formula. May not be expressible in strict first order. Merge.kif 4357-4359
( ∀ [V__Agent,V__Activity,V__ATIncome]
   ((∃ [V__Income,V__Tax,V__TaxAmount]
       (s__incomeEarned(V__Agent,V__Income,V__Activity)
       ∧
       s__amountCharged(V__Tax,V__TaxAmount)
     ∧
     s__causes(V__Activity,V__Tax)
   ∧
   (V__ATIncome = s__SubtractionFn(V__Income,V__TaxAmount))))
<⇒
s__afterTaxIncome(V__Agent,V__ATIncome,V__Activity))
)

FinancialOntology.kif 3222-3229
( ∀ [V__Option,V__Time]
   ((∃ [V__Stock,V__StockPrice,V__StrikePrice]
       (s__instance(V__Option,s__Option) ∧
         s__underlier(V__Option,V__Stock)
       ∧
       s__price(V__Stock,V__StockPrice,V__Time)
     ∧
     s__strikePrice(V__Option,V__StrikePrice)
   ∧
   (V__StockPrice = V__StrikePrice)))
<⇒
s__atTheMoney(V__Option,V__Time))
)

FinancialOntology.kif 2948-2956
No TPTP formula. May not be expressible in strict first order. Mid-level-ontology.kif 11682-11692
( ∀ [V__REGION,V__FRACTION,V__TOTAL,V__UNIT,V__AMOUNT]
   ((s__arableLandArea(V__REGION,V__FRACTION)
     ∧
     s__greaterThanOrEqualTo(V__FRACTION,0)
   ∧
   s__totalArea(V__REGION,s__MeasureFn(V__TOTAL,V__UNIT))

s__instance(V__UNIT,s__UnitOfArea) ∧
(V__AMOUNT = s__MeasureFn(s__MultiplicationFn(V__FRACTION,V__TOTAL)
,V__UNIT)))

s__arableLandArea(V__REGION,V__AMOUNT))
)

Geography.kif 2028-2035
( ∀ [V__REGION,V__FRACTION,V__TOTAL,V__AMOUNT]
   ((s__arableLandArea(V__REGION,V__FRACTION)
     ∧
     s__greaterThanOrEqualTo(V__FRACTION,0)
   ∧
   s__totalArea(V__REGION,V__TOTAL)

s__instance(V__TOTAL,s__AreaMeasure) ∧
(V__AMOUNT = s__MultiplicationFn(V__FRACTION,V__TOTAL)))

s__arableLandArea(V__REGION,V__AMOUNT))
)

Geography.kif 2019-2026
No TPTP formula. May not be expressible in strict first order. ArabicCulture.kif 193-210
( ∀ [V__A3,V__CURRENCY,V__A2,V__AREA]
   ((s__codeMapping(s__ISO_4217_A,V__A3,V__CURRENCY)
     ∧
     s__codeMapping(s__ISO_3166_1_alpha_2,V__A2,V__AREA)
   ∧
   s__subclass(V__AREA,s__GeopoliticalArea) ∧
   (V__A2 = s__SubstringFn(V__A3,0,2)))

s__currencyType(V__AREA,V__CURRENCY))
)

Media.kif 2859-2865
( ∀ [V__EXPERIMENT,V__CONFIDENCE,V__EXPERIMENTING,V__FORMULA]
   ((s__confidenceInterval(V__EXPERIMENT,V__CONFIDENCE)
     ∧
     s__instance(V__EXPERIMENT,V__EXPERIMENTING)
   ∧
   s__instance(V__FORMULA,s__Formula) ∧
   s__patient(V__EXPERIMENT,V__FORMULA)

(V__CONFIDENCE = 100))

s__truth(V__FORMULA,'$false__m'))
)

UXExperimentalTerms.kif 680-687
( ∀ [V__EXPERIMENT,V__CONFIDENCE,V__EXPERIMENTING,V__FORMULA]
   ((s__confidenceInterval(V__EXPERIMENT,V__CONFIDENCE)
     ∧
     s__instance(V__EXPERIMENT,V__EXPERIMENTING)
   ∧
   s__instance(V__FORMULA,s__Formula) ∧
   s__patient(V__EXPERIMENT,V__FORMULA)

(V__CONFIDENCE = 100))

s__truth(V__FORMULA,'$true__m'))
)

UXExperimentalTerms.kif 671-678

Display limited to 25 items. Show next 25

Display limited to 25 items. Show next 25

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


( ∀ [V__NUMBER1,V__NUMBER2]
   (((s__AbsoluteValueFn(V__NUMBER1)
       = V__NUMBER2)
     ∧
     s__instance(V__NUMBER1,s__RealNumber) ∧
     s__instance(V__NUMBER2,s__RealNumber))
   <⇒
   ((s__instance(V__NUMBER1,s__NonnegativeRealNumber) ∧
       (V__NUMBER1 = V__NUMBER2))
     ∨
     (s__instance(V__NUMBER1,s__NegativeRealNumber) ∧
       (V__NUMBER2 = s__SubtractionFn(0,V__NUMBER1)))))
)

Merge.kif 4911-4922
( ∀ [V__ROW1]
   ((s__instance(s__duration__m,s__TotalValuedRelation) ∧
       s__instance(s__duration__m,s__Predicate))
     <⇒
     (∃ [V__VALENCE]
       (s__instance(s__duration__m,s__Relation) ∧
         s__valence(s__duration__m,V__VALENCE)
       ∧
       ((∀ [V__NUMBER,V__ELEMENT,V__CLASS]
           ((s__lessThan(V__NUMBER,V__VALENCE)
             ∧
             s__domain(s__duration__m,V__NUMBER,V__CLASS)
           ∧
           (V__ELEMENT = s__ListOrderFn(s__ListFn_1(V__ROW1)
          ,V__NUMBER)))
     ⇒
     s__instance(V__ELEMENT,V__CLASS)))

(∃ [V__ITEM]
s__duration(V__ROW1,V__ITEM))))))
)

Merge.kif 2318-2335
( ∀ [V__UNIT,V__AMOUNT]
   ((s__instance(V__UNIT,s__UnitOfMeasure) ∧
       (V__AMOUNT = s__MeasureFn(1,s__SquareUnitFn(V__UNIT))))
<⇒
(V__AMOUNT = s__MultiplicationFn(s__MeasureFn(1,V__UNIT)
,s__MeasureFn(1,V__UNIT))))
)

Geography.kif 3748-3752
( ∀ [V__MUSIC]
   (s__attribute(V__MUSIC,s__PolyphonicMusic) <⇒
     (∃ [V__PART1,V__PART2]
       (s__instance(V__MUSIC,s__MakingMusic) ∧
         s__instance(V__PART1,s__MakingMusic) ∧
         s__instance(V__PART2,s__MakingMusic) ∧
         s__subProcess(V__PART1,V__MUSIC)
       ∧
       s__subProcess(V__PART2,V__MUSIC)
     ∧
     (¬ (V__PART1 = V__PART2))
     ∧
     s__cooccur(V__PART1,V__MUSIC)
   ∧
   s__cooccur(V__PART2,V__MUSIC))))
)

Mid-level-ontology.kif 927-938
( ∀ [V__LIST1,V__AVERAGE,V__LASTPLACE]
   (s__average(V__LIST1,V__AVERAGE)
   <⇒
   (∃ [V__LIST2]
     ((s__ListLengthFn(V__LIST2)
       = s__ListLengthFn(V__LIST1))
   ∧
   (s__ListOrderFn(V__LIST2,1)
   = s__ListOrderFn(V__LIST1,1))

(∀ [V__ITEMFROM2]
(s__inList(V__ITEMFROM2,V__LIST2)

(∃ [V__POSITION,V__POSITIONMINUSONE,V__ITEMFROM1,V__PRIORFROM2]
   (s__greaterThan(V__POSITION,1)
   ∧
   s__lessThanOrEqualTo(V__POSITION,s__ListLengthFn(V__LIST2))

(s__ListOrderFn(V__LIST2,V__ITEMFROM2)
= V__POSITION)

s__inList(V__ITEMFROM1,V__LIST1)

(V__POSITION = s__ListOrderFn(V__LIST1,V__ITEMFROM1))

s__inList(V__PRIORFROM2,V__LIST2)

(V__POSITIONMINUSONE = s__SubtractionFn(V__POSITION,1))

(V__POSITIONMINUSONE = s__ListOrderFn(V__LIST2,V__PRIORFROM2))

(V__ITEMFROM2 = s__AdditionFn(V__ITEMFROM1,V__PRIORFROM2))))))

(V__LASTPLACE = s__ListLengthFn(V__LIST2))

(V__AVERAGE = s__DivisionFn(s__ListOrderFn(V__LIST2,V__LASTPLACE)
,V__LASTPLACE)))))
)

People.kif 285-306
( ∀ [V__BG,V__N,V__R,V__P,V__N1,V__P2,V__N2]
   (s__beliefGroupPercentInRegion(V__BG,V__N,V__R)
   <⇒
   (∃ [V__G1,V__G2]
     (s__located(V__P,V__R)
     ∧
     s__member(V__P,V__BG)
   ∧
   s__member(V__P,V__G1)

s__memberCount(V__G1,V__N1)

s__located(V__P2,V__R)

s__member(V__P2,V__G2)

s__memberCount(V__G2,V__N2)

(s__DivisionFn(V__N,100)
= s__DivisionFn(V__N1,V__N2)))))
)

People.kif 1526-1537
( ∀ [V__E,V__R,V__MIN,V__M,V__MAX]
   (s__compressionRatio(V__E,V__R)
   <⇒
   (s__minCylinderVolume(V__E,s__MeasureFn(V__MIN,V__M))

s__maxCylinderVolume(V__E,s__MeasureFn(V__MAX,V__M))

(V__R = s__DivisionFn(V__MIN,V__MAX))))
)

Cars.kif 1917-1922
( ∀ [V__PHYS1,V__PHYS2]
   (s__cooccur(V__PHYS1,V__PHYS2)
   <⇒
   (s__WhenFn(V__PHYS1)
   = s__WhenFn(V__PHYS2)))
)

Merge.kif 8483-8485
No TPTP formula. May not be expressible in strict first order. People.kif 104-117
No TPTP formula. May not be expressible in strict first order. People.kif 138-151
No TPTP formula. May not be expressible in strict first order. People.kif 253-277
No TPTP formula. May not be expressible in strict first order. People.kif 411-442
( ∀ [V__LIST,V__ITEM]
   ((s__LastFn(V__LIST)
     = V__ITEM)
   <⇒
   (∃ [V__NUMBER]
     ((s__ListLengthFn(V__LIST)
       = V__NUMBER)
     ∧
     (s__ListOrderFn(V__LIST,V__NUMBER)
     = V__ITEM))))
)

Mid-level-ontology.kif 6346-6351
No TPTP formula. May not be expressible in strict first order. People.kif 323-353
No TPTP formula. May not be expressible in strict first order. People.kif 367-398
No TPTP formula. May not be expressible in strict first order. People.kif 221-238
No TPTP formula. May not be expressible in strict first order. People.kif 174-202
No TPTP formula. May not be expressible in strict first order. People.kif 77-86
( ∀ [V__NUMBER1,V__NUMBER2,V__NUMBER]
   ((s__RemainderFn(V__NUMBER1,V__NUMBER2)
     = V__NUMBER)
   <⇒
   (s__AdditionFn(s__MultiplicationFn(s__FloorFn(s__DivisionFn(V__NUMBER1,V__NUMBER2))
,V__NUMBER2)
,V__NUMBER)
= V__NUMBER1))
)

Merge.kif 5248-5250
( ∀ [V__BG,V__N,V__R,V__P,V__N1,V__P2,V__N2]
   (s__ethnicityPercentInRegion(V__BG,V__N,V__R)
   <⇒
   (∃ [V__G1,V__G2]
     (s__located(V__P,V__R)
     ∧
     s__member(V__P,V__BG)
   ∧
   s__member(V__P,V__G1)

s__memberCount(V__G1,V__N1)

s__located(V__P2,V__R)

s__member(V__P2,V__G2)

s__memberCount(V__G2,V__N2)

(s__DivisionFn(V__N,100)
= s__DivisionFn(V__N1,V__N2)))))
)

People.kif 1545-1556
( ∀ [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__NUMBER1,V__NUMBER2]
   (s__greaterThanOrEqualTo(V__NUMBER1,V__NUMBER2)
   <⇒
   ((V__NUMBER1 = V__NUMBER2)
     ∨
     s__greaterThan(V__NUMBER1,V__NUMBER2)))
)

Merge.kif 1940-1944
No TPTP formula. May not be expressible in strict first order. Mid-level-ontology.kif 28294-28305
( ∀ [V__COMPOUND]
   (s__instance(V__COMPOUND,s__CompoundSubstance) <⇒
     (∃ [V__ELEMENT1,V__ELEMENT2,V__PROCESS]
       (s__instance(V__ELEMENT1,s__ElementalSubstance) ∧
         s__instance(V__ELEMENT2,s__ElementalSubstance) ∧
         (¬ (V__ELEMENT1 = V__ELEMENT2))
         ∧
         s__instance(V__PROCESS,s__ChemicalSynthesis) ∧
         s__resource(V__PROCESS,V__ELEMENT1)
       ∧
       s__resource(V__PROCESS,V__ELEMENT2)
     ∧
     s__result(V__PROCESS,V__COMPOUND))))
)

Merge.kif 12391-12401
( ∀ [V__CONTINENT]
   (s__instance(V__CONTINENT,s__Continent) <⇒
     ((s__Africa = V__CONTINENT)
       ∨
       (s__NorthAmerica = V__CONTINENT)
       ∨
       (s__SouthAmerica = V__CONTINENT)
       ∨
       (s__Antarctica = V__CONTINENT)
       ∨
       (s__Europe = V__CONTINENT)
       ∨
       (s__Asia = V__CONTINENT)
       ∨
       (s__Oceania = V__CONTINENT)))
   )

Geography.kif 3350-3359

Display limited to 25 items. Show next 25

Display limited to 25 items. Show next 25

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


No TPTP formula. May not be expressible in strict first order. Military.kif 928-941
(∀ [V__NUMBER]
   (s__MeasureFn(V__NUMBER,s__OunceMass) = s__MeasureFn(s__DivisionFn(V__NUMBER,16)
  ,s__PoundMass)))

Mid-level-ontology.kif 10946-10949
(∀ [V__NUMBER]
   (s__PredecessorFn(V__NUMBER)
   = s__SubtractionFn(V__NUMBER,1)))

Merge.kif 4874-4875
(∀ [V__NUMBER]
   (s__SuccessorFn(V__NUMBER)
   = s__AdditionFn(V__NUMBER,1)))

Merge.kif 4854-4855
No TPTP formula. May not be expressible in strict first order. Merge.kif 3224-3227
No TPTP formula. May not be expressible in strict first order. Merge.kif 3229-3233
(¬ (s__BigSix = s__GroupOf6))

Government.kif 2852-2852

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


No TPTP formula. May not be expressible in strict first order. Military.kif 867-876
(s__BeginFn(s__BeforeCommonEra) = s__NegativeInfinity)

Mid-level-ontology.kif 7589-7589
(s__CardinalityFn(s__Continent) = 7)

Merge.kif 14144-14144
(s__CardinalityFn(s__NativityMagi) = 3)

Media.kif 2005-2005
No TPTP formula. May not be expressible in strict first order. People.kif 462-472
(s__EndFn(s__CommonEra) = s__PositiveInfinity)

Mid-level-ontology.kif 7597-7597
No TPTP formula. May not be expressible in strict first order. Military.kif 890-901
(s__MeasureFn(0.0,s__AngularDegree) = s__MeasureFn(360.0,s__AngularDegree))

Merge.kif 7644-7644
(s__MeasureFn(1,s__AngularDegree) = s__MeasureFn(60,s__ArcMinute))

Geography.kif 382-382
(s__MeasureFn(1,s__ArcMinute) = s__MeasureFn(60,s__ArcSecond))

Geography.kif 401-401
(s__MeasureFn(1,s__CubicFoot) = s__MultiplicationFn(s__MeasureFn(1,s__FootLength),s__MultiplicationFn(s__MeasureFn(1,s__FootLength),s__MeasureFn(1,s__FootLength))))

Mid-level-ontology.kif 11223-11229
(s__MeasureFn(1,s__Fathom) = s__MeasureFn(6,s__FootLength))

Geography.kif 3664-3664
(s__MeasureFn(1,s__KilowattHour) = s__MeasureFn(3.6,s__MegaFn(s__Joule)))

Economy.kif 2012-2012
(s__MeasureFn(1,s__KilowattHour) = s__MeasureFn(3600000,s__Joule))

Economy.kif 2013-2013
(s__MeasureFn(1,s__MetricTon) = s__MeasureFn(2205,s__PoundMass))

Mid-level-ontology.kif 11195-11197
(s__MeasureFn(1,s__NauticalMile) = s__MeasureFn(1852,s__Meter))

Geography.kif 3684-3684
(s__MeasureFn(1,s__NauticalMile) = s__MeasureFn(6076.1,s__FootLength))

Geography.kif 3683-3683
(s__MeasureFn(1,s__SquareKilometer) = s__MultiplicationFn(s__MeasureFn(1,s__KiloFn(s__Meter))
,s__MeasureFn(1,s__KiloFn(s__Meter))))

Geography.kif 621-622
(s__MeasureFn(1,s__SquareMeter) = s__MultiplicationFn(s__MeasureFn(1,s__Meter),s__MeasureFn(1,s__Meter)))

Geography.kif 3736-3737
(s__MeasureFn(1,s__SquareMile) = s__PerFn(s__MeasureFn(1,s__Mile),s__MeasureFn(1,s__Mile)))

Mid-level-ontology.kif 11279-11283
(s__MeasureFn(1,s__SquareYard) = s__PerFn(s__MeasureFn(1,s__YardLength),s__MeasureFn(1,s__YardLength)))

Mid-level-ontology.kif 11289-11293
( ∀ [V__DEG]
   (s__MeasureFn(V__DEG,s__ArcMinute) = s__MeasureFn(s__MultiplicationFn(60,V__DEG)
  ,s__ArcSecond))
)

Geography.kif 402-402
( ∀ [V__MUMBER,V__NUMBER]
   (s__MeasureFn(V__MUMBER,s__Micrometer) = s__MeasureFn(s__MultiplicationFn(V__NUMBER,0.0000001)
  ,s__Meter))
)

Geography.kif 6450-6453
( ∀ [V__NUM]
   (s__MeasureFn(V__NUM,s__AngularDegree) = s__MeasureFn(s__MultiplicationFn(60,V__NUM)
  ,s__ArcMinute))
)

Geography.kif 383-383
( ∀ [V__NUMBER]
   (s__MeasureFn(V__NUMBER,s__Amu) = s__MeasureFn(s__MultiplicationFn(V__NUMBER,1.6605402E-24)
  ,s__Gram))
)

Merge.kif 7404-7406

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